Merge pull request #3817 from peterschrammel/symex-equation-property-id

Get property ID for SSA step assert

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -78,20 +78,16 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   {
     if(it->is_assert())
     {
-      irep_idt property_id;
+      irep_idt property_id = it->get_property_id();
 
-      if(it->source.pc->is_assert())
-        property_id=it->source.pc->source_location.get_property_id();
-      else if(it->source.pc->is_goto())
+      if(property_id.empty())
+        continue;
+
+      if(it->source.pc->is_goto())
       {
-        // this is likely an unwinding assertion
-        property_id=id2string(
-          it->source.pc->source_location.get_function())+".unwind."+
-          std::to_string(it->source.pc->loop_number);
-        goal_map[property_id].description=it->comment;
+        // goto may yield an unwinding assertion
+        goal_map[property_id].description = it->comment;
       }
-      else
-        continue;
 
       goal_map[property_id].instances.push_back(it);
     }

src/goto-symex/symex_target_equation.cpp

@@ -1007,3 +1007,27 @@ void symex_target_equationt::SSA_stept::validate(
     break;
   }
 }
+
+irep_idt symex_target_equationt::SSA_stept::get_property_id() const
+{
+  PRECONDITION(is_assert());
+
+  irep_idt property_id;
+
+  if(source.pc->is_assert())
+  {
+    property_id = source.pc->source_location.get_property_id();
+  }
+  else if(source.pc->is_goto())
+  {
+    // this is likely an unwinding assertion
+    property_id = id2string(source.pc->source_location.get_function()) +
+                  ".unwind." + std::to_string(source.pc->loop_number);
+  }
+  else
+  {
+    // return empty
+  }
+
+  return property_id;
+}

src/goto-symex/symex_target_equation.h

@@ -279,6 +279,9 @@ class symex_target_equationt:public symex_targett
     // NOLINTNEXTLINE(whitespace/line_length)
     bool is_atomic_end() const      { return type==goto_trace_stept::typet::ATOMIC_END; }
 
+    // return the property ID if this is an assertion step
+    irep_idt get_property_id() const;
+
     // we may choose to hide
     bool hidden=false;