From e8725d73c12742caa3997520095cae77ed2d8cf3 Mon Sep 17 00:00:00 2001
From: kroening <kroening@6afb6bc1-c8e4-404c-8f48-9ae832c5b171>
Date: Tue, 7 Jan 2014 13:42:11 +0000
Subject: [PATCH] report unreached assertions

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3366 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
---
 src/symex/path_search.cpp        |  8 +++++---
 src/symex/path_search.h          |  4 +++-
 src/symex/symex_parseoptions.cpp | 16 ++++++++--------
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 0643132866..97ad01fc1d 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -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();
       }
     }    
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index 6af871f75d..5422d0d443 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -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;
   };
diff --git a/src/symex/symex_parseoptions.cpp b/src/symex/symex_parseoptions.cpp
index 68102cdff4..b4ac8c7332 100644
--- a/src/symex/symex_parseoptions.cpp
+++ b/src/symex/symex_parseoptions.cpp
@@ -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