Move bmct and all_properties to jbmc/

These aren't used by CBMC anymore, but only
for the symex-driven lazy-loading mode of JBMC.

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -1,4 +1,6 @@
-SRC = jbmc_main.cpp \
+SRC = all_properties.cpp \
+      bmc.cpp \
+      jbmc_main.cpp \
       jbmc_parse_options.cpp \
       # Empty last line
 
@@ -39,8 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \
       ../miniz/miniz$(OBJEXT) \
       ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       # Empty last line
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src

src/cbmc/all_properties.cpp renamed to jbmc/src/jbmc/all_properties.cpp

@@ -61,7 +61,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
-#include <cbmc/bmc.h> // will go away
+#include "bmc.h" // will go away
 
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>

src/cbmc/all_properties_class.h renamed to jbmc/src/jbmc/all_properties_class.h

@@ -1,6 +1,5 @@
 analyses
 ansi-c # should go away
-cbmc # bmc.h - will go away
 goto-checker
 goto-instrument
 goto-programs
@@ -11,5 +10,7 @@ langapi # should go away
 linking
 pointer-analysis
 solvers/refinement
+solvers/prop
+solvers/sat
 solvers/strings
 util

src/cbmc/bmc.cpp renamed to jbmc/src/jbmc/bmc.cpp

@@ -1,6 +1,4 @@
-SRC = all_properties.cpp \
-      bmc.cpp \
-      c_test_input_generator.cpp \
+SRC = c_test_input_generator.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \

src/cbmc/bmc.h renamed to jbmc/src/jbmc/bmc.h

@@ -31,7 +31,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/strings/string_refinement.h>
 
-#include "bmc.h"
 #include "xml_interface.h"
 
 class goto_functionst;

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -98,9 +98,7 @@ testing-utils-clean:
 	$(MAKE) $(MAKEARGS) -C testing-utils clean
 
 # We need to link bmc.o to the unit test, so here's everything it depends on...
-BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
-          ../src/cbmc/bmc$(OBJEXT) \
-          ../src/cbmc/c_test_input_generator$(OBJEXT) \
+BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \
           ../src/cbmc/xml_interface$(OBJEXT) \