Project

General

Profile

Bug #7279

crash in VTT (2)

Added by Sepideh Asadi 10 months ago. Updated 8 months ago.

Status:
Resolved
Priority:
Normal
Assignee:
-
Start date:
07/05/2018
Due date:
% Done:

0%


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


History

#1 Updated by Karine Even Mendoza 9 months ago

Sometimes we can skip this bug when using --no-error-trace option

#2 Updated by Martin Blicha 8 months ago

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.

#3 Updated by Martin Blicha 8 months ago

  • 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