Kunjian Song

[cpp] Fixed operational model for string

15

Fixed loads of errors and warnings, such as: - comparison between `char` and `NULL` - arithmetic on void* pointers - overloading binary operators as member functions. But the overloaded binary...

CPP old-frontend uses a different name for c size `sizeof-type` rather than `#c_sizeof_type`: **Fixed the error message below:** ``` esbmc: ../src/cpp/cpp_typecheck_type.cpp:18: virtual void cpp_typecheckt::typecheck_type(typet&): Assertion `type.is_not_nil()' failed. Program received signal...

### Benchmark to be used: `regression/esbmc-cpp/string` ### Current status: Commit: f51f498930be039c932ee45e574892f77d649976 (ESBMC main) Cmd line: ./esbmc string_length_3/main.cpp -I ../library/ --unwind 25 --no-unwinding-assertions --memlimit 14000000 --timeout 900 Error: ``` fatal error:...

Previously discussed in https://github.com/esbmc/esbmc/pull/815#issuecomment-1196741044 Standardize all the dynamic alloc call to deal with malloc/new and free/delete in symex.

ESBMC crashes when printing SSA for struct bitfield regression test

4

### Test case: `regression/esbmc/struct_bitfields_16` ### Error: ``` ~/ESBMC_Project/release/bin$ ./esbmc struct_bitfields_16/main.c --ssa-trace ESBMC version 6.9.0 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmc libc file struct_bitfields_16/main.c: Parsing Converting Generating GOTO...

[clang-cpp] class inheritance

9

Add support for inheritance and polymorphism:

ESBMC-CHERI failed to build

7

ESBMC-CHERI failed to build due to parsing error when generating libc model. ### Error log: Please see file attached below: [error_log.txt](https://github.com/esbmc/esbmc/files/14000716/error_log.txt) ### CHERI build command used: ``` python cheribuild.py cheribsd-riscv64-purecap...

./esbmc gcc-template-tests/vtable1/main.cpp --compact-trace Error: ``` [Counterexample] State 1 file main.cpp line 7 thread 0 ---------------------------------------------------- r = 0 (00000000 00000000 00000000 00000000) State 2 file main.cpp line 11 thread 0...

./esbmc-new gcc-template-tests/union1/main.cpp ``` ERROR: Declaration has an empty name: CXXConstructorDecl 0x8773568 col:5 implicit used 'void () throw()' inline default trivial `-CompoundStmt 0x8773850 Aborted (core dumped) ``` version https://github.com/esbmc/esbmc/commit/db4d28d4bfdbb8a80f118c15ba6fa4f5f70ad0ea

TC const1: failed to generate VCC due to unrecognized address_of operand

1

./esbmc gcc-template-tests/const1/main.cpp ``` Encoding remaining VCC(s) using bit-vector/floating-point arithmetic ERROR: Unrecognized address_of operand: address_of * pointer_obj : address_of * pointer_obj : symbol * name : c:@F@bar# * renamelev : Level...