Merge pull request #4223 from peterschrammel/get-only-failed-properties

Get_all_property_ids should only return failed properties

Author: peterschrammel

regression/cbmc-cover/branch-loop1/main.c

@@ -0,0 +1,11 @@
+int main(int argc, char **argv)
+{
+  for(int i = 0; i < 4; i++)
+  {
+    char c;
+    __CPROVER_input("c", c);
+    if(c == 42)
+      return 0;
+  }
+  return 1;
+}

regression/cbmc-cover/branch-loop1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--xml-ui --cover branch
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+</inputs>\n\s*<goal id="main\.coverage\.1"/>\n\s*<goal id="main\.coverage\.2"/>\n\s*<goal id="main\.coverage\.3"/>\n\s*<goal id="main\.coverage\.5"/>\n\s*</test>
+--
+^warning: ignoring
+--
+Expect each goal only occur once per test.

src/cbmc/c_test_input_generator.cpp

@@ -71,7 +71,7 @@ json_objectt test_inputst::to_json(
   }
 
   json_arrayt goal_refs;
-  for(const auto &goal_id : goto_trace.get_all_property_ids())
+  for(const auto &goal_id : goto_trace.get_failed_property_ids())
   {
     goal_refs.push_back(json_stringt(goal_id));
   }
@@ -112,7 +112,7 @@ xmlt test_inputst::to_xml(
     }
   }
 
-  for(const auto &goal_id : goto_trace.get_all_property_ids())
+  for(const auto &goal_id : goto_trace.get_failed_property_ids())
   {
     xmlt &xml_goal = xml_result.new_element("goal");
     xml_goal.set_attribute("id", id2string(goal_id));

src/goto-checker/goto_trace_storage.cpp

@@ -33,7 +33,7 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
 const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
 {
   traces.push_back(std::move(trace));
-  const auto &all_property_ids = traces.back().get_all_property_ids();
+  const auto &all_property_ids = traces.back().get_failed_property_ids();
   DATA_INVARIANT(
     !all_property_ids.empty(), "a trace must violate at least one assertion");
   for(const auto &property_id : all_property_ids)

src/goto-programs/goto_trace.cpp

@@ -773,13 +773,13 @@ void show_goto_trace(
 
 const trace_optionst trace_optionst::default_options = trace_optionst();
 
-std::vector<irep_idt> goto_tracet::get_all_property_ids() const
+std::set<irep_idt> goto_tracet::get_failed_property_ids() const
 {
-  std::vector<irep_idt> property_ids;
+  std::set<irep_idt> property_ids;
   for(const auto &step : steps)
   {
-    if(step.is_assert())
-      property_ids.push_back(step.property_id);
+    if(step.is_assert() && !step.cond_value)
+      property_ids.insert(step.property_id);
   }
   return property_ids;
 }

src/goto-programs/goto_trace.h

@@ -206,8 +206,8 @@ class goto_tracet
     return steps.back();
   }
 
-  /// Returns the property IDs of all assertions in the trace
-  std::vector<irep_idt> get_all_property_ids() const;
+  /// Returns the property IDs of all failed assertions in the trace
+  std::set<irep_idt> get_failed_property_ids() const;
 };
 
 /// Options for printing the trace using show_goto_trace