Mikhail R. Gadelha

Atexit support

5

This PR implements atexit support, as shipped in the last SV-COMP. It also adds some small changes so it works with --memcleanup-check.

Enable memory leak check when doing memcleanup and disable it otherwise

1

Signed-off-by: Mikhail R. Gadelha

Add error label target despite disabling user assertions

5

It should fix issue #475

[WIP] Camada support

4

Work-in-progress support for camada (https://github.com/mikhailramalho/camada). Should massively simplify ESBMC's backend.

Add support for __ESBMC_array_of(foo) to the frontend

4

As discussed in issue esbmc/esbmc#131, we can avoid the loop by using a new reserved function __ESBMC_array_of(foo). This can be easily done on both frontends (the C++ frontends won't need...

Infinite loop (?) on symbolic execution

6

OBS: the new llvm frontend is required in order to reproduce this error. The program in [1] causes esbmc to hang during symbolic execution. Maybe an infinite loop. Symex trace...

Score schema for the SoftwareSystems category

8

Hi all, I'm running some tests now and just saw the distribution for the SoftwareSystems category: Systems_BusyBox_MemSafety: 52 benchmarks Systems_BusyBox_Overflows: 52 benchmarks Systems_DeviceDriversLinux64_ReachSafety: 2796 benchmarks Given our meta category score...

Add type assertions when creating irep2s

7

We are currently generating a number of `irep`/`irep2` expr's where the operands have different types. The SMT solvers don't like it, and even the C standard tries to avoid it...

[JSC][32bit] Enable concurrency

6

#### df50b57bbbf11f79296ed7298983d930bf787496 [JSC][32bit] Enable concurrency https://bugs.webkit.org/show_bug.cgi?id=239821 Reviewed by NOBODY (OOPS!). This enables concurrency on 32bit systems but it's disabled by default. The solution is using the isLiveConcurrently which locks, checks...

[libc][riscv] Fatal error: glibc detected an invalid stdio handle

1

I started to get the following error when testing the latest ToT libc in a VisionFive 2 board: ```console $ valgrind ./libc.test.src.stdio.ungetc_test.__build__ ==51691== Memcheck, a memory error detector ==51691== Copyright...