Rafael Sá Menezes

This PR adds the flag `--goto-ssa-promotion` which will introduce phi-nodes into the goto program for all program variables. It consists in: 1. Computing dominator information about the CFG. 2. Computing...

Realloc and memcpy issues while verifying a vector structure

3

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...

Fix Z3 API usage

11

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...

Add a "JUMP" step in SSA trace

1

In ESBMC, our counterexample is generated using the SSA trace. However, it can be challenging to track the program flow when only the assignments are available. We could make the...

ESBMC complaining with symbol not being found in a big file (wolfSSL)

1

1. Clone wolfSSL (https://github.com/wolfSSL/wolfssl) 2. Checkout version 4.0.0 3. Run `esbmc src/tls13.c --function DoPreSharedKeys -I.`, esbmc will complain about the entry point not being found. This issue happens even when...