Felipe R. Monteiro

ESBMC doesn't find standard C libraries on macOS

13

I tried to verify the following program on macOS Monterey 12.3.1. I installed ESBMC using the [latest Darwin script](https://github.com/esbmc/esbmc/releases/tag/v6.10). ```c #include void unescape(char *p) { unsigned v; while (*p) {...

Replace `PROOF_SOURCES` with `ABSTRACTIONS` when using stubs in CBMC proofs.

Since we have a stub for this function and use it in proofs, we need a proof harness.

CBMC proofs for `aws_hash_iter_delete` and `aws_hash_table_remove` use a stub for the `s_remove_entry`static function in order to cope with complexity. Improve CBMC performance and remove the stub.

In some proofs we use `ASSUME_VALID_MEMORY_COUNT` to properly allocate a valid memory in proof harnesses. It's nice to have a new macro that does the malloc + the nullness etc....

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Many CBMC proofs use stubs for standard C functions (e.g., `memcpy`) that are no longer necessary. By removing these stubs, many proofs could go from bounded to unbounded (e.g., proofs...

Signed-off-by: Felipe R. Monteiro

Better error message for missing dependencies

1

One user reporter the following error while trying to run the `run-cbmc-proofs.py` script. ```shell ./run-cbmc-proofs.py --proofs aws_byte_buf_append_and_update For your convenience, the output of this run will be symbolically linked to...