esbmc
esbmc copied to clipboard
esbmc
The efficient SMT-based context-bounded model checker (ESBMC)
I was trying to use esbmc to verify the following code: ```c typedef struct vector vector; #define VECTOR_INIT_LENGTH 10 #define VECTOR_FACTOR 2 struct vector { char *_buf; size_t length; size_t...
### built-in-functions : Let us take a look at few examples below from #1963 ``` def foo() -> None: a = int(2.121212121212) assert a == 2 foo() x = int(1)...
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...
```cpp #include int main() { int src = 1; int dest = 2; __builtin_memcpy(&dest, &src, sizeof(int)); assert(dest == 1); } ``` fails with: ``` ESBMC version 7.6.1 64-bit x86_64 linux...
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()...
Following the issue: https://github.com/Z3Prover/z3/issues/6479#issuecomment-1337364769 Running ESBMC with the following program: ```c extern void abort(void); #include void reach_error() { assert(0); } #include int *a, *b; int n; extern int __VERIFIER_nondet_int(void); void...
For some reason, ESBMC is not printing the SMT formula with Z3 when we use the options: `--smt-formula-only` and `--smt-formula-too`.
$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)
The ill-typed expressions happens to arrive at smt-conv on the sv-comp benchmark [c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--wireless--iwlegacy--iwl3945.ko-entry_point.cil.out.i](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--wireless--iwlegacy--iwl3945.ko-entry_point.cil.out.i) causing ESBMC to abort with ``` src/solvers/boolector/boolector_conv.cpp:287: virtual const smt_ast* boolector_convt::mk_bvor(smt_astt, smt_astt): Assertion `a->sort->get_data_width() == b->sort->get_data_width()' failed....
