From 9104800db9bee08c7ec70a3dc99e2ef492aa7dfb Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sun, 28 Oct 2018 19:00:52 +0000
Subject: [PATCH] all-properties now shows results by function

---
 .../cbmc/Multiple_Properties1/test.desc       |  6 +-
 src/cbmc/all_properties.cpp                   | 57 +++++++++++++++++--
 src/cbmc/all_properties_class.h               |  2 +
 3 files changed, 57 insertions(+), 8 deletions(-)

diff --git a/regression/cbmc/Multiple_Properties1/test.desc b/regression/cbmc/Multiple_Properties1/test.desc
index 1c7d5d0087c..37817de2447 100644
--- a/regression/cbmc/Multiple_Properties1/test.desc
+++ b/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
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
index c04fa8420eb..20d00cdea1c 100644
--- a/src/cbmc/all_properties.cpp
+++ b/src/cbmc/all_properties.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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"))
diff --git a/src/cbmc/all_properties_class.h b/src/cbmc/all_properties_class.h
index 42b95de39f4..215ad4d3655 100644
--- a/src/cbmc/all_properties_class.h
+++ b/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());
     }