Factor out bmct building blocks int bmc_util

This is an intermediate step in order to reuse
the building blocks in the new implementation of bmct.
The old implementation is functional until it can
be replaced by the new one.

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -40,6 +40,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \

jbmc/unit/Makefile

@@ -84,6 +84,7 @@ java-testing-utils-clean:
 BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \

src/cbmc/Makefile

@@ -1,6 +1,7 @@
 SRC = all_properties.cpp \
       bmc.cpp \
       bmc_cover.cpp \
+      bmc_util.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \

src/cbmc/all_properties.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <chrono>
 
+#include <cbmc/bmc_util.h>
+
 #include <util/xml.h>
 #include <util/json.h>
 
@@ -55,7 +57,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   auto solver_start=std::chrono::steady_clock::now();
 
-  bmc.do_conversion();
+  convert_symex_target_equation(
+    bmc.equation, bmc.prop_conv, get_message_handler());
+  bmc.freeze_program_variables();
 
   // Collect _all_ goals in `goal_map'.
   // This maps property IDs to 'goalt'
@@ -144,9 +148,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   bool safe=(cover_goals.number_covered()==0);
 
   if(safe)
-    bmc.report_success(); // legacy, might go away
+    report_success(bmc.ui_message_handler); // legacy, might go away
   else
-    bmc.report_failure(); // legacy, might go away
+    report_failure(bmc.ui_message_handler); // legacy, might go away
 
   return safe?safety_checkert::resultt::SAFE:safety_checkert::resultt::UNSAFE;
 }