esbmc
esbmc copied to clipboard
esbmc
The efficient SMT-based context-bounded model checker (ESBMC)
What if instead of generating SSA, symex could generate SMT directly instead? In practice, that would be done by replacing the code in `symex_target_equationt::*` with calls to smt_conv. PROS: *...
Is there a reason why ESBMC does not report errors, specifically overflow and underflow on addition and subtraction that i tested for solidity contracts. If the data types are smaller...
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...
ESBMC 7.3.0 crashes in the following C program: command: `esbmc DATASET/FormAI_212.c` C program: ```c #include #include #include #include #define NUM_THREADS 4 // Structure to hold the coordinates of a point...
Testing the existing CHERI TCs in the latest release had the following issues: ```c #include #include char *buffer = "hello"; int main(int argc, char **argv) { char *__capability cap_ptr =...
HTML output
This PR adds support to generate html bug trace by using the flag `--generate-html-report`
Follow suggestion in https://github.com/esbmc/esbmc/pull/2008#issuecomment-2318404541
We now count all the conditions, instead of only the guard of the if-expr. This includes the condition within `ASSERT`, `ASSUME`, `ASSIGN`, `GOTO`, `RETURN`, `FUNCTION_CALL` and `OTHER`. E.g. ```c++ int...
This PR adds config file support to ESBMC. Now the arguments can be specified in a ini/toml style syntax in a file, and ESBMC will load those values when running....
ESBMC does not detect misaligned accesses to buffers returned by malloc, but does successfully detect misaligned accesses to global and stack memory. Minimal reproducer: ``` #include int main(void) { float...
