search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
830 stars 262 forks source link

c++ program with single inheritance, Bounds check Aborted #3551

Closed venkyjntu-git closed 5 years ago

venkyjntu-git commented 5 years ago

The following c++ program with single inheritance. Giving error the error described below, please let me know the reason OS is :Ubuntu 14.04.5 LTS

//#include //using namespace std; class Base { int a[10]; public: void show() { //cout<<"In base class"<<endl; a[11]=20; } }; class Derived:public Base { int b[5]; public: void show() { //cout<<"In derived class"<<endl; } };

int main() { Base bo1; Derived do1; bo1.show(); do1.show();

return 0; }

./cbmc --bounds-check tests/buff_over_wop.cpp

CBMC version 5.10 (cbmc-5.10) 64-bit x86_64 linux Parsing tests/buff_over_wop.cpp Converting Type-checking buff_over_wop Generating GOTO Program Adding CPROVER library (x86_64) Removal of function pointers and virtual functions Generic Property Instrumentation Running with 8 object bits, 56 offset bits (default) Starting Bounded Model Checking --- begin invariant violation report --- Invariant check failed File: goto_symex_state.cpp:55 function: operator() Condition: found_l0 Reason: level0: failed to find this Backtrace: [0x53c2bd] [0x53c8ff] [0x4a9aa4] [0x8128c6] [0x812a02] [0x81687a] [0x816753] [0x8165cb] [0x814efa] [0x814eb4] [0x7ed173] [0x7e602e] [0x7fd650] [0x5c0e19] [0x7fcd9e] [0x7fdad3] [0x7fed94] [0x596942] [0x59ab1e] [0x59bcb6] [0x5b09c4] [0x49cc81] [0xa13019] [0x49f73a]

--- end invariant violation report --- Aborted (core dumped)

venkyjntu-git commented 5 years ago

Any one , Please help me to resolve the issue