Lucas C. Cordeiro

[k-induction] Shall our inductive step report VERIFICATION SUCCESSFUL?

6

If we run this program as esbmc file.c --k-induction, our inductive step reports "VERIFICATION SUCCESSFUL". ````C int main() { int y = __VERIFIER_nondet_int(); __ESBMC_assume(y >= 0 && y = 0...

[k-induction] disable partial loops for the k-induction proof rule.

7

**Summary** This commit updates several test description files and a source file in ESBMC. The changes are mainly related to the regression tests for k-induction and its parallel variant. Additionally,...

Hi guys, Do you see some benefit from mapping the property violations found by ESBMC to the Common Weaknesses Enumeration? As an example, we have two papers that we perform...

[Python] ERROR: PARSING ERROR

3

Bug report from a ESBMC-Python user: ```` I’ve tried on a simple python file as esbmc.exe cpufreqs_catcher.py This is the return ESBMC version 7.6.1 64-bit x86_64 windows Target: 64-bit little-endian...

[Concurrency] Is this benchmark safe?

2

I think this benchmark is incorrectly labelled in SV-COMP. SV-COMP says that this benchmark is safe, but I think it is unsafe given the description of `pthread_cond_wait`: ``` The pthread_cond_wait()...

[SMT backend] ESBMC is not printing the SMT formula with Z3

5

For some reason, ESBMC is not printing the SMT formula with Z3 when we use the options: `--smt-formula-only` and `--smt-formula-too`.

[pointer analysis] Assertion `is_struct_type(type) || is_union_type(type)' failed.

1

$esbmc alglin1.c --function det2 --incremental-bmc ```` esbmc: /home/lucas/ESBMC_Project/esbmc/src/pointer-analysis/value_set.cpp:1439: expr2tc value_sett::make_member(const expr2tc&, const irep_idt&): Assertion `is_struct_type(type) || is_union_type(type)' failed. Aborted ```` [test.zip](https://github.com/esbmc/esbmc/files/11028002/test.zip)

Incorrect instrumentation for data-races check. If we disable the data-races check, ESBMC can verify this program: $ time esbmc main.c --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check...

ESBMC crashes for this C++ code using the following command: $ esbmc pol_assert.cpp --incremental-bmc ````CPP #include #include #include #include using namespace std; // Base class class Animal { public: //...