replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

report unreached assertions 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3366 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-01-07 13:42:11 +00:00
parent bee60df9d3
commit e8725d73c1
3 changed files with 16 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/symex/path_search.cpp
View File

@ -279,8 +279,10 @@ void path_searcht::check_assertion(
irep_idt property_name=instruction.location.get_claim();
property_entryt &property_entry=property_map[property_name];
if(property_entry.status==UNSAFE)
if(property_entry.status==FAIL)
return; // already failed
else if(property_entry.status==NOT_REACHED)
property_entry.status=PASS; // well, for now!
// the assertion in SSA
exprt assertion=
@ -312,7 +314,7 @@ void path_searcht::check_assertion(
{
case decision_proceduret::D_SATISFIABLE:
build_goto_trace(state, bv_pointers, property_entry.error_trace);
property_entry.status=UNSAFE;
property_entry.status=FAIL;
number_of_failed_properties++;
break; // error
@ -362,7 +364,7 @@ void path_searcht::initialize_property_map(
irep_idt property_name=location.get_claim();
property_entryt &property_entry=property_map[property_name];
property_entry.status=SAFE;
property_entry.status=NOT_REACHED;
property_entry.description=location.get_comment();
}
}

4
src/symex/path_search.h
View File

@ -44,9 +44,11 @@ public:
absolute_timet start_time;
time_periodt sat_time;
enum statust { NOT_REACHED, PASS, FAIL };
struct property_entryt
{
resultt status;
statust status;
irep_idt description;
goto_tracet error_trace;
};

16
src/symex/symex_parseoptions.cpp
View File

@ -594,9 +594,9 @@ void symex_parseoptionst::report_properties(
switch(it->second.status)
{
case path_searcht::SAFE: status_string="OK"; break;
case path_searcht::UNSAFE: status_string="FAILURE"; break;
case path_searcht::ERROR: status_string="ERROR"; break;
case path_searcht::PASS: status_string="OK"; break;
case path_searcht::FAIL: status_string="FAILURE"; break;
case path_searcht::NOT_REACHED: status_string="OK"; break;
}
xml_result.set_attribute("status", status_string);
@ -609,15 +609,15 @@ void symex_parseoptionst::report_properties(
<< it->second.description << ": ";
switch(it->second.status)
{
case path_searcht::SAFE: status() << "OK"; break;
case path_searcht::UNSAFE: status() << "FAILED"; break;
case path_searcht::ERROR: status() << "ERROR"; break;
case path_searcht::PASS: status() << "OK"; break;
case path_searcht::FAIL: status() << "FAILED"; break;
case path_searcht::NOT_REACHED: status() << "OK (not reached)"; break;
}
status() << eom;
}
if(cmdline.isset("show-trace") &&
it->second.status==path_searcht::UNSAFE)
it->second.status==path_searcht::FAIL)
show_counterexample(it->second.error_trace);
}
@ -631,7 +631,7 @@ void symex_parseoptionst::report_properties(
it=property_map.begin();
it!=property_map.end();
it++)
if(it->second.status==path_searcht::UNSAFE)
if(it->second.status==path_searcht::FAIL)
failed++;
status() << "** " << failed