Merge pull request #3241 from diffblue/cbmc-goal-ordering

all-properties now shows results in an ordering

Author: Daniel Kroening

regression/cbmc/Multiple_Properties1/test.desc

@@ -1,10 +1,10 @@
 CORE
 main.c
 --property main.assertion.1 --property main.assertion.3
+activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION FAILED
-^.*main.assertion.1.*SUCCESS
-^.*main.assertion.3.*FAILURE
+^VERIFICATION FAILED$
+^main.c function main\n\[main\.assertion\.1\] .* SUCCESS\n\[main\.assertion\.3\] .* FAILURE$
 --
 ^warning: ignoring

src/cbmc/all_properties.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "all_properties_class.h"
 
+#include <algorithm>
 #include <chrono>
 
 #include <util/xml.h>
@@ -158,17 +159,63 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
     {
       result() << "\n** Results:" << eom;
 
-      for(const auto &goal_pair : goal_map)
+      // collect goals in a vector
+      std::vector<goal_mapt::const_iterator> goals;
+
+      for(auto g_it = goal_map.begin(); g_it != goal_map.end(); g_it++)
+        goals.push_back(g_it);
+
+      // now determine an ordering for those goals:
+      // 1. alphabetical ordering of file name
+      // 2. numerical ordering of line number
+      // 3. alphabetical ordering of goal ID
+      std::sort(
+        goals.begin(),
+        goals.end(),
+        [](goal_mapt::const_iterator git1, goal_mapt::const_iterator git2) {
+          const auto &g1 = git1->second.source_location;
+          const auto &g2 = git2->second.source_location;
+          if(g1.get_file() != g2.get_file())
+            return id2string(g1.get_file()) < id2string(g2.get_file());
+          else if(!g1.get_line().empty() && !g2.get_line().empty())
+            return std::stoul(id2string(g1.get_line())) <
+                   std::stoul(id2string(g2.get_line()));
+          else
+            return id2string(git1->first) < id2string(git2->first);
+        });
+
+      // now show in the order we have determined
+
+      irep_idt previous_function;
+      for(const auto &g : goals)
       {
-        result() << "[" << goal_pair.first << "] "
-                 << goal_pair.second.description << ": ";
+        const auto &l = g->second.source_location;
 
-        if(goal_pair.second.status == goalt::statust::SUCCESS)
+        if(l.get_function() != previous_function)
+        {
+          if(!previous_function.empty())
+            result() << '\n';
+          previous_function = l.get_function();
+          if(!previous_function.empty())
+          {
+            if(!l.get_file().empty())
+              result() << l.get_file() << ' ';
+            if(!l.get_function().empty())
+              result() << "function " << l.get_function();
+            result() << eom;
+          }
+        }
+
+        result() << faint << '[' << g->first << "] " << reset;
+
+        result() << g->second.description << ": ";
+
+        if(g->second.status == goalt::statust::SUCCESS)
           result() << green;
         else
           result() << red;
 
-        result() << goal_pair.second.status_string() << reset << eom;
+        result() << g->second.status_string() << reset << eom;
       }
 
       if(bmc.options.get_bool_option("trace"))

src/cbmc/all_properties_class.h

@@ -40,6 +40,7 @@ class bmc_all_propertiest:
       instancest;
     instancest instances;
     std::string description;
+    source_locationt source_location;
 
     // if failed, we compute a goto_trace for the first failing instance
     enum statust { UNKNOWN, FAILURE, SUCCESS, ERROR } status;
@@ -64,6 +65,7 @@ class bmc_all_propertiest:
       const goto_programt::instructiont &instruction):
       status(statust::UNKNOWN)
     {
+      source_location = instruction.source_location;
       description=id2string(instruction.source_location.get_comment());
     }