Merge pull request #3210 from diffblue/goto-analyzer-output

Daniel Kroening · web-flow · commit 3628f2eb3528 · 2018-12-11T13:40:28.000-05:00
goto-analyzer: tweak user interface
diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: UNKNOWN$
+^\[main.assertion.1\] line 11 assertion i\s*<\s*51: UNKNOWN$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (UNKNOWN|FAILURE \(if reachable\))$
+^\[main.assertion.1\] line 12 assertion i\s*<\s*51: (UNKNOWN|FAILURE \(if reachable\))$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: SUCCESS$
+^\[main.assertion.1\] line 8 assertion eight == 8: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc
@@ -3,11 +3,11 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: FAILURE \(if reachable\)
-\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: UNKNOWN
-\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: SUCCESS
-\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: UNKNOWN
-\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: FAILURE \(if reachable\)
+\[main.assertion.1\] line 18 assertion \(1.0f / 10.0f\) - f < -0.1f: FAILURE \(if reachable\)
+\[main.assertion.2\] line 20 assertion \(1.0f / 10.0f\) - f < 0.0f: UNKNOWN
+\[main.assertion.3\] line 22 assertion \(1.0f / 10.0f\) - f <= 0.0f: SUCCESS
+\[main.assertion.4\] line 24 assertion \(1.0f / 10.0f\) - f >= 0.0f: UNKNOWN
+\[main.assertion.5\] line 26 assertion \(1.0f / 10.0f\) - f > 0.0f: FAILURE \(if reachable\)
 
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: SUCCESS
-^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: SUCCESS
+^\[main.assertion.1\] line 9 assertion rounded_up - 0.1f >= 0: SUCCESS
+^\[main.assertion.2\] line 10 assertion rounded_down - 0.1f < 0: SUCCESS
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc
@@ -1,15 +1,15 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: SUCCESS$
-^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: SUCCESS$
-^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: UNKNOWN$
-^\[main.assertion.4\] file main.c line 16 function main, assertion 0: SUCCESS$
-^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: SUCCESS$
-^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: UNKNOWN$
-^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: SUCCESS$
-^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: SUCCESS$
+^\[main.assertion.1\] line 7 assertion i\s*>=\s*10: SUCCESS$
+^\[main.assertion.2\] line 10 assertion i\s*!=\s*30: SUCCESS$
+^\[main.assertion.3\] line 13 assertion i\s*!=\s*15: UNKNOWN$
+^\[main.assertion.4\] line 16 assertion 0: SUCCESS$
+^\[main.assertion.5\] line 19 assertion j\s*>=\s*10: SUCCESS$
+^\[main.assertion.6\] line 22 assertion i\s*>=\s*j: UNKNOWN$
+^\[main.assertion.7\] line 25 assertion i\s*>=\s*11: SUCCESS$
+^\[main.assertion.8]\ line 28 assertion j\s*<\s*100: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 5 function main, assertion x > -10 \&\& x < 100: SUCCESS$
+^\[main.assertion.1\] line 5 assertion x > -10 \&\& x < 100: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 6 function main, assertion x > -10 \|\| x < 100: SUCCESS$
+^\[main.assertion.1\] line 6 assertion x > -10 \|\| x < 100: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 && i <= 2: SUCCESS$
+^\[main.assertion.1\] line 8 assertion i >= 1 && i <= 2: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \|\| i <= 2: SUCCESS$
+^\[main.assertion.1\] line 8 assertion i >= 1 \|\| i <= 2: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc
@@ -1,8 +1,8 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \|\| x > 100: FAILURE \(if reachable\)$
+^\[main.assertion.1\] line 7 assertion x < -10 \|\| x > 100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc
@@ -1,8 +1,8 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \&\& x > 100: FAILURE \(if reachable\)$
+^\[main.assertion.1\] line 7 assertion x < -10 \&\& x > 100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc
@@ -1,8 +1,8 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 \&\& x < 100: FAILURE \(if reachable\)$
+^\[main.assertion.1\] line 6 assertion x < -10 \&\& x < 100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \&\& i <= 2: SUCCESS$
+^\[main.assertion.1\] line 8 assertion i >= 1 \&\& i <= 2: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc
@@ -1,12 +1,12 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$
-^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$
-^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: FAILURE \(if reachable\)$
-^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: UNKNOWN$
-^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: FAILURE \(if reachable\)$
+^\[main.assertion.1\] line 8 assertion j<=100: SUCCESS$
+^\[main.assertion.2\] line 11 assertion j<101: SUCCESS$
+^\[main.assertion.3\] line 14 assertion j>100: FAILURE \(if reachable\)$
+^\[main.assertion.4\] line 17 assertion j<99: UNKNOWN$
+^\[main.assertion.5\] line 20 assertion j==100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc
@@ -1,9 +1,9 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: UNKNOWN$
-^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: UNKNOWN$
+^\[main.assertion.1\] line 30 assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: UNKNOWN$
+^\[main.assertion.2\] line 35 assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: UNKNOWN$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_12/test.desc b/regression/goto-analyzer/intervals_12/test.desc
@@ -1,9 +1,9 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^[main.assertion.1] file main.c line 8 function main, assertion j < 0: SUCCESS$
-^[main.assertion.2] file main.c line 11 function main, assertion j < 0: SUCCESS$
+^[main.assertion.1] line 8 assertion j < 0: SUCCESS$
+^[main.assertion.2] line 11 assertion j < 0: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc
@@ -1,15 +1,15 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: SUCCESS$
-^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: SUCCESS$
-^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: UNKNOWN$
-^\[main.assertion.4\] file main.c line 16 function main, assertion 0: SUCCESS$
-^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: SUCCESS$
-^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: UNKNOWN$
-^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: SUCCESS$
-^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: SUCCESS$
+^\[main.assertion.1\] line 7 assertion i\s*>=\s*10: SUCCESS$
+^\[main.assertion.2\] line 10 assertion i\s*!=\s*30: SUCCESS$
+^\[main.assertion.3\] line 13 assertion i\s*!=\s*15: UNKNOWN$
+^\[main.assertion.4\] line 16 assertion 0: SUCCESS$
+^\[main.assertion.5\] line 19 assertion j\s*>=\s*10: SUCCESS$
+^\[main.assertion.6\] line 22 assertion i\s*>=\s*j: UNKNOWN$
+^\[main.assertion.7\] line 25 assertion i\s*>=\s*11: SUCCESS$
+^\[main.assertion.8\] line 28 assertion j\s*<\s*100: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_14/test.desc b/regression/goto-analyzer/intervals_14/test.desc
@@ -1,10 +1,10 @@
 FUTURE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: UNKNOWN$
-^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: UNKNOWN$
-^\[main.assertion.3\] file main.c line 14 function main, assertion i<52: SUCCESS$
+^\[main.assertion.1\] line 12 assertion i<50: UNKNOWN$
+^\[main.assertion.2\] line 13 assertion i<51: UNKNOWN$
+^\[main.assertion.3\] line 14 assertion i<52: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_15/test.desc b/regression/goto-analyzer/intervals_15/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: UNKNOWN$
+^\[main.assertion.1\] line 11 assertion j\s*<\s*52: UNKNOWN$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals_16/test.desc b/regression/goto-analyzer/intervals_16/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
---intervals --verify
+--intervals
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (UNKNOWN|FAILURE \(if reachable\))$
+^\[main.assertion.1\] line 11 assertion j\s*<\s*52: (UNKNOWN|FAILURE \(if reachable\))$
 --
 ^warning: ignoring
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
@@ -157,28 +157,44 @@ static void static_verifier_text(
 static void static_verifier_console(
   const std::vector<static_verifier_resultt> &results,
   const namespacet &ns,
-  messaget &m,
-  std::ostream &out)
+  messaget &m)
 {
   irep_idt last_function_id;
+  irep_idt function_file;
 
   for(const auto &result : results)
   {
     if(last_function_id != result.function_id)
     {
       if(!last_function_id.empty())
-        out << '\n';
+        m.status() << '\n';
       last_function_id = result.function_id;
       const auto &symbol = ns.lookup(last_function_id);
-      out << "******** Function " << symbol.display_name() << '\n';
+      m.status() << messaget::underline << "Function " << symbol.display_name();
+      function_file = symbol.location.get_file();
+      if(!function_file.empty())
+        m.status() << ' ' << function_file;
+      if(!symbol.location.get_line().empty())
+        m.status() << ':' << symbol.location.get_line();
+      m.status() << messaget::reset << messaget::eom;
     }
 
-    m.result() << '[' << result.source_location.get_property_id() << ']' << ' ';
+    m.result() << messaget::faint << '['
+               << result.source_location.get_property_id() << ']'
+               << messaget::reset;
 
-    m.result() << result.source_location;
+    if(
+      !result.source_location.get_file().empty() &&
+      result.source_location.get_file() != function_file)
+    {
+      m.result() << " file " << result.source_location.get_file();
+    }
+
+    if(!result.source_location.get_line().empty())
+      m.result() << " line " << result.source_location.get_line();
 
     if(!result.source_location.get_comment().empty())
-      m.result() << ", " << result.source_location.get_comment();
+      m.result() << ' ' << result.source_location.get_comment();
 
     m.result() << ": ";
 
@@ -203,6 +219,9 @@ static void static_verifier_console(
 
     m.result() << messaget::eom;
   }
+
+  if(!results.empty())
+    m.result() << '\n';
 }
 
 /// Runs the analyzer and then prints out the domain
@@ -290,7 +309,7 @@ bool static_verifier(
   }
   else
   {
-    static_verifier_console(results, ns, m, out);
+    static_verifier_console(results, ns, m);
   }
 
   m.status() << m.bold << "Summary: "
