Lucas C. Cordeiro

[WiP] Refactor string copy functions

6

I have created this PR just to clarify one question raised by @vanderson-rocha when implementing the string solver in ESBMC. In this simple C program, ESBMC produces: $ `esbmc file.c...

[Concurrency] Segmentation fault

7

ESBMC crashes in this example: ```C a; *d, *e; b() { if (a) ; } c() { do ; while (a == 0); } main() { pthread_create(&d, 0, b, 0);...

noreturn attribute

3

Check whether we support the noreturn attribute in ESBMC.

Undefined behaviour for 43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

15

@marek-trtik and I have investigate this issue. This benchmark `43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c` contains an execution trace leading to an undefined behaviour related to overlap of strings passed to `strncpy` (this is a...

@marek-trtik and I have analyzed this benchmark. Our conclusions are: each execution trace (starting in the `main` function) reaches the line 6847, where is called a function `ldv_initialize`. Two things...

[Concurrency] Experimental results

4

I will run some experiments with different context-bounds and report the results here to keep the history. * **Context-bound 2 and --no-por:** the current master (https://github.com/esbmc/esbmc/commit/0e707f7b6b53956ee3c95525d9c93ba69108cbe3) produced the following results...

An idea to speedup our multi-property verification

10

We could introduce literals to indicate which assertions have been checked by the SMT solver to reduce the computational burden in our multi-property verification. For example, consider the following C...