Chenfeng Wei

closed via #1647

In the latest debug version - `esbmc --unwind 1 --overflow-check --no-unwinding-assertions --multi-property` ```shell Solving claim 'arithmetic overflow on add' with solver Boolector 3.2.2 Runtime decision procedure: 0.000s Slicing for Claim...

Sorry, this is because we have changed the command to run the ESBMC-Solidity. So the flags we are now using are: - `--sol`: to provide the smart contract source file...

> @ChenfengWei0: can I ask you to update our documentation at https://ssvlab.github.io/esbmc/documentation.html? Yes

The cause might be that, whatever value we set to the key, the return `val` in ESBMC will always be `NULL` (`assert(val == NULL)` always hold).

> You can use the option `--force-malloc-success` to ensure that malloc always succeeds. Thanks for the suggestions. I tried `--k-induction --force-malloc-success` and `--unwind 9 --no-unwinding-assertions --force-malloc-success --no-pointer-check` and still get...

```c++ typedef struct { int *a; } b; typedef struct { b base; } c; c e; d(b *i) { b f = *i; while (f.a) ; } g(b *i)...

I further simplified it a little bit ```c++ #include #include typedef struct { int *a; } b; typedef struct { b base; } c; c e; void g(b *i) {...

> What is the verdict for this issue here? My view: CBMC defaults to --force-malloc-success (which for us should imply realloc() success as well, I believe), therefore without that flag...

This issue can be avoided, to some extent, by using `--k-step = num`. `esbmc file.c --k-induction` ```sh Checking inductive step, k = 2 Starting Bounded Model Checking Unwinding loop 3...