Lucas C. Cordeiro

icon indicating a website link https://ssvlab.github.io/lucasccordeiro/ icon indicating an email [email protected]

icon company The University of Manchester, UK icon location Manchester icon location Lucas C. Cordeiro is a Full Professor in the Department of Computer Science at the University of Manchester/UK and an Associate Professor at UFAM/Brazil.

Results 215 comments of Lucas C. Cordeiro

ESBMC intrinsic library

Hi @mikhailramalho, You're correct. `Alloc` does not solve the problem. However, `__ESBMC_alloca` has a different semantic than `alloca`. `__ESBMC_alloca` allocates a memory that is always valid. In particular, `__EBMC_alloca` was...

Intrinsic memset optimization

@rafaelsamenezes: as discussed, we should move forward with this PR :-)

Intrinsic memset optimization

Many thanks, @rafaelsamenezes. Can I ask you to fix the code style and rebase this PR with the master?

Assert with dynamic strings don't work

@rafaelsamenezes: Can I ask you whether you have news about this issue?

Memory safety: addresses of free'd objects are excluded from the address space

@fbrausse: can I ask you for the status of this issue?

Memory safety: addresses of free'd objects are excluded from the address space

@fbrausse: can I ask you for the status of this issue?

Memory safety: addresses of free'd objects are excluded from the address space

@fbrausse: let's move forward with option (a).

Support for integers bigger than 64 bits

I believe @brcfarias could work on this issue.

[WiP] Benchexec kind parallel

@ericksonalves: Does this PR still make sense?

[Concurrency] Segmentation fault

ESBMC still fails with this example: ```` esbmc: /home/lucas/ESBMC_Project/esbmc/src/goto-symex/execution_state.cpp:502: void execution_statet::preserve_last_paths(): Assertion `it != ls.top().goto_state_map.end() && "Nonexistant preserved-path target?"' failed. ```` @Anthonysdu : could you please check this issue?