ESBMC Cpp Support - esbmc/esbmc GitHub Wiki

Supported features:

ESBMC v7 supports the following C++ features:

  • Class

  • new and delete operators

  • constructors and destructors

  • lvalue reference

  • rvalue reference

  • Move semantics: Move constructor, Move assignment operator.

  • template

  • inheritance and polymorphism:

    • single-level polymorhism
    • multi-level polymorhism
    • pure virtual method
    • virtual inheritance (the diamond problem)
    • correct order of ctors/dtors:
      • tracked by the umbrella issue issue 940, affected features are listed below:
        • Virtual destructor
        • Base initialization for the most-derivied class
        • Order of destruction in case of object composition (part-whole relationship)
  • (TODO) Exception handling:

    • try-catch, throw

Features WIP:

Backlog:

Issues are listed from high to low priority in each subsection:

Development Tracking:

The new clang-based frontend is under development. We are currently working to pass the benchmark regression/esbmc-cpp/cpp which contains 370 test cases. Please see benchmark stats in each subsection.

The stats are generated by applying the following commands in the benchmark logs from Github workflow "Run a Benchmark":

To generate stats about error signatures:

egrep "Assertion|ERROR" * -rn | egrep -v "//" | cut -d':' -f3- | sort | uniq -c

To generate stats about passes:

egrep "VERIFICATION FAILED|VERIFICATION SUCCESSFUL" * -rn | rev | cut -d ':' -f 1 | rev | sort | uniq -c

Summary of Pass Rate in Each Test Suite:

Test Suite Pass Rate Date Remarks
cpp 281/374, 75.13% 19/02/2024 Last run: result link
inheritance_bringup 14/15, 93.3% 19/03/2023 Skipped as the last TC is not passable even by the old esbmc-v2.1
polymorphism_bringup 39/45, 86.7% 19/03/2023 1x TC failure is caused by issue 938. 2x TC failures are caused by issue 940. The remaining failures are skipped as they are not passable even by the old esbmc-v2.1
cbmc 119/120, 99% 11/07/2023 This suite contains 'Template_XXX' TCs only. Last run: result link The failed TC is covered by https://github.com/esbmc/esbmc/issues/940
gcc-template-tests 104/113, 92% 13/06/2023 Last run: result link - apart from arg6, const1, spec26, union1 and vtable1, the remaining failed TCs are not passable by v2.1
template 93/107, 87% 11/07/2023 Last run: result link - the remaining failed TCs are either OM dependent or not passable by v2.1
stream 22/66, 33% 03/08/2023 Last run: result link
string 194/234, 82.91% 19/02/2024 Last run: result link
algorithm 0/144, 0% 03/08/2023 Last run: result link
deque 0/43, 0% 03/08/2023 Last run: result link
list 0/72, 0% 03/08/2023 Last run: result link
map 0/47, 0% 03/08/2023 Last run: result link
multimap 0/47, 0% 03/08/2023 Last run: result link
multiset 0/43, 0% 03/08/2023 Last run: result link
priority_queue 0/15, 0% 03/08/2023 Last run: result link
set 0/48, 0% 03/08/2023 Last run: result link
stack 0/14, 0% 03/08/2023 Last run: result link
vector 0/143, 0% 03/08/2023 Last run: result link
try_catch 0/81, 0% 03/08/2023 Last run: result link

The following lines are used to fix the TCs, and added here for future reference: The commands below are for future reference: Fix the include path for Linux CIs:

egrep "\-I ~/libraries" . -rl | xargs sed -i 's/-I \~\/libraries/-I \/__w\/esbmc\/esbmc\/src\/cpp\/library/g'

Add tag for each TC in a test suite:

from pathlib import Path
for path in Path('./').rglob('test.desc'):
    print(path)
    f = open(path,'r')
    lines = f.readlines()[:-1]
    lines.append("<item_10_mode>KNOWNBUG</item_10_mode>" + "\n")
    lines.append("</test-case>")
    f.close()
    f = open(path,'w')
    f.writelines(lines)

Tracking Error Signatures for esbmc-cpp/cpp test suite:

Since we've added the support for most of the key features, most, if not all, errors are of the type PARSE ERRORS in our OMs for STL test suites. There's no need to track parse errors for those test suites. See section Summary of Pass Rate in Each Test Suite for the most up-to-date pass rate.

Build LLVM from source:

Using a debug build of clang greatly helps debugging the clang-based C++ converter in ESBMC. See Rafael's guide in https://github.com/esbmc/esbmc/wiki/Windows-Build#llvm

⚠️ **GitHub.com Fallback** ⚠️