esbmc
esbmc copied to clipboard
esbmc
The efficient SMT-based context-bounded model checker (ESBMC)
This PR is based on #819, is work-in-progress atm. and does: - add support for a new type annotation `__attribute__((annotate("__ESBMC_ODR-override")))` - add these annotations to all pthread-specific types in the...
I am opening this as a draft for more discussion. @mikhailramalho has suggested me to look into the `incomplete_array` from CBMC. It seems that they actually removed it and use...
Dear all, Shall we release a new version of ESBMC? ESBMC v6.11 or v7? The main feature of this release would be our new Jimple frontend for ESBMC. Additionally, the...
I've found this by accident: 1. We ignore malloc: https://github.com/esbmc/esbmc/blob/master/src/goto-programs/builtin_functions.cpp#L177 2. Even worse, we assert(0) in new: https://github.com/esbmc/esbmc/blob/master/src/goto-programs/builtin_functions.cpp#L270
I'm just getting two crashes with the latest master, may I ask if you can take a look? It's on `vector_gcc_literal_shufflevector_3_false` and `vector_gcc_literal_shufflevector_3_true` when running with `--no-simplify --incremental-bmc`: ``` esbmc...
Simplifications cases for : // A + -B --> A - B // (A + 1) + ~B --> A - B // (~B + A) + 1 --> A...
Note: This is an incorrect approach for this! I am opening this as a PR so I can properly fix at ucode branch. Right now the PR is adding external...
We need a shared header to be used by users. This header should contain all ESBMC instructions that one might need for verifying its programs. - Depends on #641
When running with the --smt-formula-only flag, esbmc crashes. Using the ESBMC-Linux.sh install, it dumps the core. Building from master crashes silently (No core dump but $? returns 127). Using the...
Every assert that are using dynamic strings: ```c assert(0 && oss.str().c_str()); ``` I think that we should: 1. Replace them with the default_msg.error 2. Make msg.error abort Edit: List of...