From 91281e188724e3bffe8df2593a7af49f7efd2ee2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 18 Sep 2018 15:43:21 +0100
Subject: [PATCH 1/3] show-vcc now uses format()

This outputs the verification conditions in 'first order logic syntax', as
opposed to syntax used by a programming language, which may cause confusion.
---
 regression/cbmc/show-vcc/test.desc |  8 ++++----
 src/goto-symex/show_vcc.cpp        | 31 +++++++++++++-----------------
 2 files changed, 17 insertions(+), 22 deletions(-)

diff --git a/regression/cbmc/show-vcc/test.desc b/regression/cbmc/show-vcc/test.desc
index f3d287e6952..bb01b2fa853 100644
--- a/regression/cbmc/show-vcc/test.desc
+++ b/regression/cbmc/show-vcc/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^some property$
-^\{-.*\} a!0@1#1$
-^\{-.*\} b!0@1#1$
-^\{1\} c!0@1#1$
-^\{2\} d!0@1#1$
+^\{-.*\} main::1::a!0@1#1$
+^\{-.*\} main::1::b!0@1#1$
+^\{1\} main::1::c!0@1#1$
+^\{2\} main::1::d!0@1#1$
 --
diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
index 640a591ff46..e7dd87c97e8 100644
--- a/src/goto-symex/show_vcc.cpp
+++ b/src/goto-symex/show_vcc.cpp
@@ -10,16 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Output of the verification conditions (VCCs)
 
 #include "show_vcc.h"
+#include "symex_target_equation.h"
 
 #include <fstream>
 #include <iostream>
+#include <sstream>
 
 #include <goto-symex/symex_target_equation.h>
 
-#include <langapi/language_util.h>
-#include <langapi/mode.h>
-
 #include <util/exception_utils.h>
+#include <util/format_expr.h>
 #include <util/json.h>
 #include <util/json_expr.h>
 #include <util/ui_message.h>
@@ -63,14 +63,11 @@ void show_vcc_plain(
       {
         if(!p_it->ignore)
         {
-          std::string string_value =
-            from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
-          out << "{-" << count << "} " << string_value << "\n";
+          out << "{-" << count << "} " << format(p_it->cond_expr) << '\n';
 
 #if 0
-          languages.from_expr(p_it->guard_expr, string_value);
-          out << "GUARD: " << string_value << "\n";
-          out << "\n";
+          out << "GUARD: " << format(p_it->guard_expr) << '\n';
+          out << '\n';
 #endif
 
           count++;
@@ -94,9 +91,7 @@ void show_vcc_plain(
     std::size_t count = 1;
     for(const auto &disjunct : disjuncts)
     {
-      std::string string_value =
-        from_expr(ns, s_it->source.pc->function, disjunct);
-      out << "{" << count << "} " << string_value << "\n";
+      out << "{" << count << "} " << format(disjunct) << "\n";
       count++;
     }
   }
@@ -147,15 +142,15 @@ void show_vcc_json(
         (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
         !p_it->ignore)
       {
-        std::string string_value =
-          from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
-        json_constraints.push_back(json_stringt(string_value));
+        std::ostringstream string_value;
+        string_value << format(p_it->cond_expr);
+        json_constraints.push_back(json_stringt(string_value.str()));
       }
     }
 
-    std::string string_value =
-      from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
-    object["expression"] = json_stringt(string_value);
+    std::ostringstream string_value;
+    string_value << format(s_it->cond_expr);
+    object["expression"] = json_stringt(string_value.str());
   }
 
   out << ",\n" << json_result;

From 9b141a79ff2cb87c0f7a9a72fe4ca7fde4765438 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Fri, 21 Sep 2018 19:57:47 +0100
Subject: [PATCH 2/3] stream output optimization

---
 src/goto-symex/show_vcc.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
index e7dd87c97e8..7ab45aa4d5e 100644
--- a/src/goto-symex/show_vcc.cpp
+++ b/src/goto-symex/show_vcc.cpp
@@ -46,10 +46,10 @@ void show_vcc_plain(
       out << '\n';
 
     if(s_it->source.pc->source_location.is_not_nil())
-      out << s_it->source.pc->source_location << "\n";
+      out << s_it->source.pc->source_location << '\n';
 
     if(s_it->comment != "")
-      out << s_it->comment << "\n";
+      out << s_it->comment << '\n';
 
     symex_target_equationt::SSA_stepst::const_iterator p_it =
       equation.SSA_steps.begin();
@@ -91,7 +91,7 @@ void show_vcc_plain(
     std::size_t count = 1;
     for(const auto &disjunct : disjuncts)
     {
-      out << "{" << count << "} " << format(disjunct) << "\n";
+      out << '{' << count << "} " << format(disjunct) << '\n';
       count++;
     }
   }

From 857797c239e164e245b42c2062b4b927362ad22b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Fri, 21 Sep 2018 19:58:22 +0100
Subject: [PATCH 3/3] use DEBUG define for debugging output

---
 src/goto-symex/show_vcc.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
index 7ab45aa4d5e..6ee76ac77bf 100644
--- a/src/goto-symex/show_vcc.cpp
+++ b/src/goto-symex/show_vcc.cpp
@@ -65,8 +65,8 @@ void show_vcc_plain(
         {
           out << "{-" << count << "} " << format(p_it->cond_expr) << '\n';
 
-#if 0
-          out << "GUARD: " << format(p_it->guard_expr) << '\n';
+#ifdef DEBUG
+          out << "GUARD: " << format(p_it->guard) << '\n';
           out << '\n';
 #endif