Move symex_bmc and symex_coverage to goto-checker

These classes are language-independent.

Author: peterschrammel

src/cbmc/Makefile

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