Bug #7279
open
Added by Sepideh Asadi over 6 years ago.
Updated over 6 years ago.
Description
File is:.../cprover/regression/funfrog/VTT/P2P_Joints_TG3_e.c
File is:.../cprover/regression/funfrog/VTT/VTT1.c
File: /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e_BUG.c
File /cprover/regression/funfrog/VTT/VTT.c
File /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e.c
Claim number # 1 is SAFE
Caught exception: identifier tag-#anon#ST[S32'a1'|S32'a2'|S32'v'|S32't1'|S32't2'|S32't3'|S32'delta'|S32'initPos'|S32'initVel'] not found
time 108.58
Sometimes we can skip this bug when using --no-error-trace option
The problem is in the end when we are reporting results about the assertion.
The exception is thrown in CProver method from_expr() in this piece of code:
res.status() << "Claim number # " << claim_number << " is " << (safe ? "SAFE" : "UNSAFE") << res.eom;
res.status()
<<" File: " << assertion->source_location.get_file()
<<" \n Function: " << assertion->source_location.get_function()
<<" \n Line: " << assertion->source_location.get_line()
<< "\n " << ((assertion->is_assert()) ? "Guard: " : "Code") <<"( "
<< from_expr(assertion->guard) <<" ) \n";
From my point of view this is inability of CProver to convert its inner representation back to source code representation.
- Status changed from New to Resolved
Fixed by letting the from_expr function know about the current symbol table. See git commit 1603c58a.
Also available in: Atom
PDF