Factor our show_vcc

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -45,7 +45,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

@@ -66,7 +66,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

@@ -8,7 +8,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

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-symex/build_goto_trace.h>
 #include <goto-symex/memory_model_pso.h>
 #include <goto-symex/show_program.h>
+#include <goto-symex/show_vcc.h>
 #include <goto-symex/slice.h>
 #include <goto-symex/slice_by_trace.h>
 
@@ -293,7 +294,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
     }
 
@@ -419,7 +420,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

@@ -12,6 +12,7 @@ SRC = auto_objects.cpp \
       precondition.cpp \
       rewrite_union.cpp \
       show_program.cpp \
+      show_vcc.cpp \
       slice.cpp \
       slice_by_trace.cpp \
       symex_assign.cpp \