Lucas C. Cordeiro

[C++ frontend] Consider handling the C++ standard while parsing the C++ libraries

2

There are subtle differences in the C++ libraries between the different standards. See our discussion at https://github.com/esbmc/esbmc/pull/1675. We should consider handling the C++ standard while parsing the C++ libraries.

[clang-cpp frontend] fail to parse <iostream> with --no-library

3

$esbmc hello.cpp --no-library --cppstd 17 ````CPP #include int main() { std::cout

Update the ESBMC-solidity documentation

1

To address this issue, we must update the ESBMC-solidity documentation at https://ssvlab.github.io/esbmc/documentation.html.

Segmentation fault (core dumped)

4

ESBMC crashes in this particular C++ example: ``` [lucascordeiro@localhost src]$ esbmc binary-tree.cpp -I ~/esbmc-cpp-linux-64-static/libraries/ ESBMC version 3.0.0 64-bit x86_64 linux file binary-tree.cpp: Parsing Converting Type-checking binary-tree.cpp Segmentation fault (core dumped)...

```` ./esbmc-wrapper.py -p ../../sv-benchmarks/c/properties/valid-memsafety.prp -s kinduction --arch 32 ../../sv-benchmarks/c/weaver/popl20-prod-cons-eq.wvr.c -------------------------------------------------------------------------------- Verifying with ESBMC Command: ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check ../../sv-benchmarks/c/weaver/popl20-prod-cons-eq.wvr.c --32 --witness-output witness.graphml --memory-leak-check...

```` ./esbmc-wrapper.py -p ../../sv-benchmarks/c/properties/valid-memsafety.prp -s kinduction --arch 32 ../../sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i -------------------------------------------------------------------------------- Verifying with ESBMC Command: ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check ../../sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i --32 --witness-output witness.graphml --memory-leak-check...

```` ./esbmc-wrapper.py -p ../../sv-benchmarks/c/properties/unreach-call.prp -s kinduction --arch 32 ../../sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c -------------------------------------------------------------------------------- Verifying with ESBMC Command: ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check ../../sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c --32 --no-por --context-bound 2...

[Python] Shall we really invoke the SMT solver for this simple Python program?

2

I would expect our constant propagation algorithm to solve this case easily without calling the SMT solver. ````Python class MyClass: def __init__(self, value: int): self.data:int = value obj1 = MyClass(5)...

We should add something like: "If you cite ESBMC >= 7.0 please cite us as below." https://github.com/esbmc/esbmc/blob/master/CITATION.cff Here is our .bib file: ```` ​ Lucas Cordeiro ​ @InProceedings{esbmc2024, author =...