Bug #7279: crash in VTT (2) - hifrog - USI & SUPSI Source Code Management (SCM)

Actions

Copy link

Bug #7279

open

crash in VTT (2)

Added by Sepideh Asadi about 6 years ago. Updated about 6 years ago.

Status:

Resolved

Priority:

Normal

Assignee:

Start date:

07/05/2018

Due date:

% Done:

Estimated time:

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

Actions

Copy link

Updated by Karine Even Mendoza about 6 years ago

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

Actions

Copy link

Updated by Martin Blicha about 6 years 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.

Actions

Copy link