Kunjian Song

It appears that `--smt-formula-only/too` works for Z3, mathsat and CVC solvers, but still broken for boolector and bitwuzla.

@mikhailramalho I'm currently researching the best way to implement vtable but not sure if we should follow approach in old frontend (cpp_typecheck_virtual_table.cpp). Here's what I found in clang: Clang appears...

> @kunjsong01: Can I ask you whether you could add some regression tests or unit tests? Done. Enabled two test cases in commit d10f6d13f60ea3f437bfbbd0b8837b6049e3a948 including pass and fail scenarios.

>Using clang to generate the vtable seems like a better way forward and should play nice with our "convert then adjust" method, however, I can't help you with that as...

> @kunjsong01 Do I understand correctly that you want to implement the same approach taken by compilers to model virtual methods? I.e. each non-abstract class gets a `vptr` member which...

A note for future clang vtable approach: https://clang.llvm.org/doxygen/VTableBuilder_8h.html https://clang.llvm.org/doxygen/CXXInheritance_8h.html `clang/AST/CXXInheritance.h` and `clang/AST/VTableBuilder.h` might be a good starting point. (For the time being, I'm not seeing the APIs to generate/use any...

TODOs to pass test case `paper_inheritance_example/main.cpp`: 1. Match symbols for Vechicle class (WIP) 2. Match symbols for Car class (TODO) 3. Match symbols for Motorcycle class (TODO) ```cpp // Vehicle...

Closed and replaced by https://github.com/esbmc/esbmc/pull/854 due to too many experiment stuff.

### Preliminary analysis and trials: Based on our current AST for C++, I spent a day trying to figure out a generic way to traverse the directed acyclic graph that...

Simply upgrading to "--std==c++14" doesn't resolve this problem - no ordering information is provided by Clang AST.