Kunjian Song

TC Templates6: class template dtor not taking effect

2

./esbmc cbmc/Templates6/main.cpp ``` State 1 file main.cpp line 34 function main thread 0 ---------------------------------------------------- Violated property: file main.cpp line 34 function main assertion g==20 g == 20 VERIFICATION FAILED ```...

[C++ verification] Umbrella issue for the order of ctors/dtors

4

Evaluted the CBMC, ESBMC-v2.1 and our *current* Clang AST to figure out whether they are able to identify the correct execution order of constructors and destructors in some (fairly) complicated...

Feature request from our external partners.

[C++ OM] OM simplification

4

We should delete all .h from our model and make all the c header simply include the standard c headers. Evaluation: Just use the existing benchmarks. Expect a similar or...

[C++ verification] Incorrect result in case of initialization by the most derived class

17

ESBMC gave incorrect verification result for the following example: ```cpp #include class A { public: A() {} A(int x) : m_x(x) {}; int getX() { return m_x; } protected: int...