Move property_checker and safety_checker into goto-checker dir

These will be transformed in subsequent PRs to form the basic
interfaces for any algorithms that can check assertions
so that they can be used interchangeably in driver programs.

Author: peterschrammel

CMakeLists.txt

@@ -58,6 +58,7 @@ set_target_properties(
     goto-analyzer-lib
     goto-cc
     goto-cc-lib
+    goto-checker
     goto-diff
     goto-diff-lib
     goto-instrument

jbmc/src/jbmc/CMakeLists.txt

@@ -12,6 +12,7 @@ target_link_libraries(jbmc-lib
     ansi-c
     big-int
     cbmc-lib
+    goto-checker
     goto-instrument-lib
     goto-programs
     goto-symex

jbmc/src/jbmc/Makefile

@@ -6,6 +6,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../java_bytecode/java_bytecode$(LIBEXT) \
       ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
       ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
       ../$(CPROVER_DIR)/src/pointer-analysis/value_set$(OBJEXT) \

jbmc/unit/CMakeLists.txt

@@ -23,6 +23,7 @@ target_link_libraries(java-unit
         testing-utils
         ansi-c
         solvers
+        goto-checker
         goto-programs
         goto-instrument-lib
         cbmc-lib

jbmc/unit/Makefile

@@ -92,6 +92,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
               $(CPROVER_DIR)/src/util/util$(LIBEXT) \
               $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+              $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/goto-instrument$(LIBEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \

src/CMakeLists.txt

@@ -85,6 +85,7 @@ add_subdirectory(ansi-c)
 add_subdirectory(assembler)
 add_subdirectory(big-int)
 add_subdirectory(cpp)
+add_subdirectory(goto-checker)
 add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
 add_subdirectory(jsil)

src/Makefile

@@ -6,6 +6,7 @@ DIRS = analyses \
        cpp \
        goto-analyzer \
        goto-cc \
+       goto-checker \
        goto-diff \
        goto-instrument \
        goto-programs \
@@ -49,9 +50,11 @@ goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir \
                      json.dir
 
+goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir
+
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
-          goto-instrument.dir
+          goto-instrument.dir goto-checker.dir
 
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir

src/cbmc/CMakeLists.txt

@@ -13,6 +13,7 @@ target_link_libraries(cbmc-lib
     assembler
     big-int
     cpp
+    goto-checker
     goto-instrument-lib
     goto-programs
     goto-symex

src/cbmc/Makefile

@@ -19,6 +19,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
+      ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../goto-symex/goto-symex$(LIBEXT) \
       ../pointer-analysis/value_set$(OBJEXT) \

src/cbmc/bmc.h

@@ -25,8 +25,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-symex/symex_target_equation.h>
 #include <goto-symex/path_storage.h>
 
+#include <goto-checker/safety_checker.h>
 #include <goto-programs/goto_model.h>
-#include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
 #include "symex_bmc.h"

src/cbmc/module_dependencies.txt

@@ -1,6 +1,7 @@
 analyses
 ansi-c
 cpp
+goto-checker
 goto-instrument
 goto-programs
 goto-symex

src/goto-checker/CMakeLists.txt

@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(goto-checker ${sources})
+
+generic_includes(goto-checker)
+
+target_link_libraries(goto-checker goto-programs goto-symex solvers util)

src/goto-checker/Makefile

@@ -0,0 +1,17 @@
+SRC = property_checker.cpp \
+      safety_checker.cpp \
+      # Empty last line
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = goto-checker$(LIBEXT)
+
+all: goto-checker$(LIBEXT)
+
+###############################################################################
+
+goto-checker$(LIBEXT): $(OBJ)
+	$(LINKLIB)

src/goto-checker/module_dependencies.txt

@@ -0,0 +1,5 @@
+goto-checker
+goto-programs
+goto-symex
+solvers
+util

src/goto-programs/property_checker.cpp renamed to src/goto-checker/property_checker.cpp

@@ -9,15 +9,15 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Property Checker Interface
 
-#ifndef CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
-#define CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
+#ifndef CPROVER_GOTO_CHECKER_PROPERTY_CHECKER_H
+#define CPROVER_GOTO_CHECKER_PROPERTY_CHECKER_H
 
 // this is just an interface -- it won't actually do any checking!
 
 #include <util/message.h>
 
-#include "goto_trace.h"
-#include "goto_model.h"
+#include <goto-programs/goto_model.h>
+#include <goto-programs/goto_trace.h>
 
 class property_checkert:public messaget
 {
@@ -52,4 +52,4 @@ class property_checkert:public messaget
   void initialize_property_map(const goto_functionst &);
 };
 
-#endif // CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
+#endif // CPROVER_GOTO_CHECKER_PROPERTY_CHECKER_H

src/goto-programs/property_checker.h renamed to src/goto-checker/property_checker.h

@@ -9,16 +9,16 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Safety Checker Interface
 
-#ifndef CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
-#define CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
+#ifndef CPROVER_GOTO_CHECKER_SAFETY_CHECKER_H
+#define CPROVER_GOTO_CHECKER_SAFETY_CHECKER_H
 
 // this is just an interface -- it won't actually do any checking!
 
 #include <util/invariant.h>
 #include <util/message.h>
 
-#include "goto_trace.h"
-#include "goto_functions.h"
+#include <goto-programs/goto_model.h>
+#include <goto-programs/goto_trace.h>
 
 class safety_checkert:public messaget
 {
@@ -123,4 +123,4 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
   }
   UNREACHABLE;
 }
-#endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
+#endif // CPROVER_GOTO_CHECKER_SAFETY_CHECKER_H

src/goto-programs/safety_checker.cpp renamed to src/goto-checker/safety_checker.cpp

@@ -36,7 +36,6 @@ SRC = adjust_float_expressions.cpp \
       parameter_assignments.cpp \
       pointer_arithmetic.cpp \
       printf_formatter.cpp \
-      property_checker.cpp \
       read_bin_goto_object.cpp \
       read_goto_binary.cpp \
       rebuild_goto_start_function.cpp \
@@ -53,7 +52,6 @@ SRC = adjust_float_expressions.cpp \
       remove_virtual_functions.cpp \
       replace_calls.cpp \
       resolve_inherited_component.cpp \
-      safety_checker.cpp \
       set_properties.cpp \
       show_goto_functions.cpp \
       show_goto_functions_json.cpp \

src/goto-programs/safety_checker.h renamed to src/goto-checker/safety_checker.h

@@ -37,6 +37,7 @@ target_link_libraries(
         testing-utils
         ansi-c
         solvers
+        goto-checker
         goto-programs
         goto-instrument-lib
         cbmc-lib

src/goto-programs/Makefile

@@ -84,6 +84,7 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \
               ../src/linking/linking$(LIBEXT) \
               ../src/util/util$(LIBEXT) \
               ../src/big-int/big-int$(LIBEXT) \
+              ../src/goto-checker/goto-checker$(LIBEXT) \
               ../src/goto-programs/goto-programs$(LIBEXT) \
               ../src/goto-instrument/goto-instrument$(LIBEXT) \
               ../src/pointer-analysis/pointer-analysis$(LIBEXT) \

unit/CMakeLists.txt

@@ -1,6 +1,7 @@
 ansi-c
 cbmc
 cpp
+goto-checker
 goto-programs
 goto-symex
 json

unit/Makefile

@@ -5,8 +5,9 @@
 #ifndef CPROVER_PATH_STRATEGIES_H
 #define CPROVER_PATH_STRATEGIES_H
 
+#include <goto-checker/safety_checker.h>
+
 #include <goto-programs/goto_model.h>
-#include <goto-programs/safety_checker.h>
 
 #include <goto-symex/goto_symex_state.h>