Move symex_bmc and symex_coverage to goto-checker

These classes are language-independent.

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -44,8 +44,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
       # Empty last line
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src

jbmc/unit/Makefile

@@ -90,8 +90,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \

src/cbmc/Makefile

@@ -7,8 +7,6 @@ SRC = all_properties.cpp \
       cbmc_parse_options.cpp \
       counterexample_beautification.cpp \
       fault_localization.cpp \
-      symex_bmc.cpp \
-      symex_coverage.cpp \
       xml_interface.cpp \
       # Empty last line
 

src/cbmc/bmc.h

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/decision_procedure.h>
 
+#include <goto-checker/symex_bmc.h>
+
 #include <goto-programs/goto_trace.h>
 
 #include <goto-symex/symex_target_equation.h>
@@ -29,7 +31,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
-#include "symex_bmc.h"
 
 class cbmc_solverst;
 

src/goto-checker/Makefile

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

src/goto-checker/bmc_util.cpp

@@ -14,8 +14,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <fstream>
 #include <iostream>
 
-#include <cbmc/symex_bmc.h>
-
 #include <goto-programs/graphml_witness.h>
 #include <goto-programs/json_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
@@ -33,6 +31,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/make_unique.h>
 #include <util/ui_message.h>
 
+#include "symex_bmc.h"
+
 void build_error_trace(
   goto_tracet &goto_trace,
   const namespacet &ns,

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

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Bounded Model Checking for ANSI-C
 
-#ifndef CPROVER_CBMC_SYMEX_BMC_H
-#define CPROVER_CBMC_SYMEX_BMC_H
+#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H
+#define CPROVER_GOTO_CHECKER_SYMEX_BMC_H
 
 #include <util/message.h>
 #include <util/threeval.h>
@@ -115,4 +115,4 @@ class symex_bmct: public goto_symext
   symex_coveraget symex_coverage;
 };
 
-#endif // CPROVER_CBMC_SYMEX_BMC_H
+#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_H

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

@@ -94,8 +94,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \
           ../src/cbmc/counterexample_beautification$(OBJEXT) \
           ../src/cbmc/fault_localization$(OBJEXT) \
-          ../src/cbmc/symex_bmc$(OBJEXT) \
-          ../src/cbmc/symex_coverage$(OBJEXT) \
           ../src/cbmc/xml_interface$(OBJEXT) \
           ../src/goto-instrument/cover$(OBJEXT) \
           ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \