Lucas C. Cordeiro
Lucas C. Cordeiro
The master branch has the option --no-por in our sv-comp wrapper. This branch removes the option --no-por. @Anthonysdu: it seems that POR makes no difference to remove the redundant interleavings....
Thanks, @Anthonysdu. @fbrausse and @Anthonysdu: shall we merge this PR to remove the `--no-por` from the SV-COMP script?
> Where is the best place for the transformation? I fear that we may get slowdowns if we do it at the goto program. So I would suggest doing it...
@Anthonysdu: This version of the `strcmp` improves ESBMC performance for a few seconds: ````C int strcmp(const char *p1, const char *p2) { __ESBMC_HIDE:; const unsigned char *s1 = (const unsigned...
Thanks, @Anthonysdu. I have submitted a PR to integrate this version of `strcmp`: https://github.com/esbmc/esbmc/pull/1718. Please let us know if other string functions need to be optimized.
@ChenfengWei0: could you check this issue?
> I understand that switching from_expr() output from e.g. C to something else might break other parts of ESBMC, but that doesn't mean we should cement this C output. Over...
@fbrausse: can I ask you to run this PR over the concurrency category of SV-COMP?
@rafaelsamenezes: could you please conclude this documentation? We must replace the malloc calls with __ESBMC_alloca because the latter does not lead to memory leaks and dangling pointers.