Move bmc_util to goto_checker module

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -40,7 +40,6 @@ 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,7 +84,6 @@ 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,7 +1,6 @@
 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,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <chrono>
 
-#include <cbmc/bmc_util.h>
+#include <goto-checker/bmc_util.h>
 
 #include <util/xml.h>
 #include <util/json.h>

src/cbmc/bmc.cpp

@@ -24,9 +24,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/static_lifetime_init.h>
 
+#include <goto-checker/bmc_util.h>
 #include <goto-checker/solver_factory.h>
 
-#include "bmc_util.h"
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 

src/cbmc/bmc_cover.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 #include <iomanip>
 
-#include <cbmc/bmc_util.h>
+#include <goto-checker/bmc_util.h>
 
 #include <util/xml.h>
 #include <util/xml_expr.h>

src/cbmc/fault_localization.cpp

@@ -26,7 +26,8 @@ Author: Peter Schrammel
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
 
-#include "bmc_util.h"
+#include <goto-checker/bmc_util.h>
+
 #include "counterexample_beautification.h"
 
 void fault_localizationt::freeze_guards()

src/goto-checker/Makefile

@@ -1,4 +1,5 @@
-SRC = solver_factory.cpp \
+SRC = bmc_util.cpp \
+      solver_factory.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/cbmc/bmc_util.cpp renamed to src/goto-checker/bmc_util.cpp

@@ -9,8 +9,8 @@ Author: Daniel Kroening, Peter Schrammel
 /// \file
 /// Bounded Model Checking Utilities
 
-#ifndef CPROVER_CBMC_BMC_UTIL_H
-#define CPROVER_CBMC_BMC_UTIL_H
+#ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
+#define CPROVER_GOTO_CHECKER_BMC_UTIL_H
 
 #include <memory>
 
@@ -71,4 +71,4 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
-#endif // CPROVER_CBMC_BMC_UTIL_H
+#endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H

src/cbmc/bmc_util.h renamed to src/goto-checker/bmc_util.h

@@ -1,5 +1,7 @@
+cbmc # symex_bmc will be moved next
 goto-checker
 goto-programs
 goto-symex
+linking
 solvers
 util

src/goto-checker/module_dependencies.txt

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