Kunjian Song

@lucasccordeiro sure, thanks

> We could relax our constraints here. > > GCC and Clang do not abort or give a warning message because `The virtual method isn't pure virtual and hasn't a...

@brcfarias for C++ verification we usually use "-I /library" so that we can use the ESBMC's C++ OMs instead of the original libraries

Preliminary analysis: This is another issue essentially caused by the order of dtor as in https://github.com/esbmc/esbmc/issues/940 Clang AST doesn't have enough information of the order of destructors in case of...

This issue is covered by the umbrella issue https://github.com/esbmc/esbmc/issues/940. based on the analysis in 940, this is a feature that also failed in CBMC and the old ESBMC not a...

OMs that need some attention: - string (`src/cpp/library/cstring` vs. `src/c2goto/library/string.c`) - cstdlib (`src/cpp/library/cstdlib` vs. `src/c2goto/library/stdlib.c`)

> @kunjsong01 @mikhailramalho What is left to do here? The only .h files remaining on the top-level are non-standard: > > ``` > $ ls cpp/library/*.h > cpp/library/OM_compiler_defs.h cpp/library/definitions.h cpp/library/systemc.h...

Since D is the most derived class, Clang is clever enough to generate the AST for D's non-trivial constructor `D(int x) : B(x), C(x) {}`: ```cpp | |-CXXConstructorDecl 0x55def76d5d30 col:5...

Hi @mikhailramalho, thanks a lot for the prompt reply. > Also, how do we handle virtual inheritance? Is A marked somehow? Do we inherit its member variables more than once...

>I can't get esbmc to verify it with the ToT ooops my mistake of copying the wrong example. I've corrected it and updated the example.