Rafael Sá Menezes
Rafael Sá Menezes
Right now, our regression suite looks like: ``` ``` From my understanding: - Mode: CORE (less than 30s tests that don't need any specific solver or arch), KNOWNBUG (tests that...
The following benchmarks are giving Incorrect true: - c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--megaraid--megaraid_mm.ko-entry_point.cil.out.yml - c/ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--scsi--megaraid--megaraid_mm.ko-entry_point.cil.out.yml - c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml All of them have the message `no body for function __builtin_object_size`. So it might be just a...
In interval analysis, we have support for adding Invariants based on the current abstract state of the statement. For example: ``` int a = * ? 0 : 10; //>...
The Jimple frontend models Assertion failures as throws. Since they are not catched, it results in a error. This behaviour is similar to what Java and Kotlin do (as the...
Currently, the abstract interpretation and the k-induction algorithm of ESBMC do not work properly for concurrency. This can lead to all sorts of confusion from users (and developers!) that are...
The following program: ```c float a; main() { for (;;) { memset(&a, 0, sizeof(a)); reach_error(); for (;;) ; } } ``` Gives an incorrect veredict when using k-induction
We can't parse the following program: ```c struct a { long b }; struct c d; struct c { short e; struct a f[] } main() { d.f->b; } ```
When trying to compile ESBMC with recent versions of llvm: ``` /Users/user/Repos/esbmc/src/clang-c-frontend/AST/build_ast.cpp:17:10: fatal error: 'llvm/Support/Host.h' file not found #include ``` And checking on my environment: ``` $ ls llvm@16/include/llvm/Support |...
As discussed in the local meetings, we could start checking other types of encoding that could be used. But first we should check how many benchmarks could be affected by...
This allow us to check whether the SMTLIB output is producing valid formulas by checking the produced formulas against Z3. I also removed the --array-flattener flag from the default flags...