Factor our show_vcc

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -47,7 +47,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/show_vcc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
       # Empty last line

jbmc/unit/Makefile

@@ -67,7 +67,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/show_vcc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \

src/cbmc/Makefile

@@ -9,7 +9,6 @@ SRC = all_properties.cpp \
       cbmc_solvers.cpp \
       counterexample_beautification.cpp \
       fault_localization.cpp \
-      show_vcc.cpp \
       symex_bmc.cpp \
       symex_coverage.cpp \
       xml_interface.cpp \

src/cbmc/bmc.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
+#include <goto-checker/show_vcc.h>
+
 #include <goto-programs/graphml_witness.h>
 #include <goto-programs/json_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
@@ -376,7 +378,7 @@ safety_checkert::resultt bmct::execute(
 
     if(options.get_bool_option("show-vcc"))
     {
-      show_vcc();
+      show_vcc(options, get_message_handler(), ui, ns, equation);
       return safety_checkert::resultt::SAFE; // to indicate non-error
     }
 
@@ -502,7 +504,7 @@ void bmct::show()
 {
   if(options.get_bool_option("show-vcc"))
   {
-    show_vcc();
+    show_vcc(options, get_message_handler(), ui, ns, equation);
   }
 
   if(options.get_bool_option("program-only"))

src/cbmc/bmc.h

@@ -199,10 +199,6 @@ class bmct:public safety_checkert
 
   virtual void freeze_program_variables();
 
-  virtual void show_vcc();
-  virtual void show_vcc_plain(std::ostream &out);
-  virtual void show_vcc_json(std::ostream &out);
-
   trace_optionst trace_options()
   {
     return trace_optionst(options);

src/cbmc/show_vcc.cpp

@@ -1,5 +1,6 @@
 SRC = property_checker.cpp \
       safety_checker.cpp \
+      show_vcc.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/goto-checker/Makefile

@@ -1,5 +1,6 @@
 goto-checker
 goto-programs
 goto-symex
+langapi # will go away
 solvers
 util