Merge pull request #89 from ftsrg/patch-move-bmcverifier

Minor refactor: Move BMCVerifier inside gazer-bmc
ftsrg · Feb 4, 2021 · 4a68caf · 4a68caf
2 parents 8600b6f + b36cfc2
commit 4a68caf
Show file tree

Hide file tree

Showing 8 changed files with 7 additions and 6 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -10,7 +10,7 @@ if(NOT DEFINED GAZER_VERSION_MINOR)
   set(GAZER_VERSION_MINOR 4)
 endif()
 if(NOT DEFINED GAZER_VERSION_PATCH)
-  set(GAZER_VERSION_PATCH 0)
+  set(GAZER_VERSION_PATCH 1)
 endif()
 if(NOT DEFINED GAZER_VERSION_SUFFIX)
   set(GAZER_VERSION_SUFFIX "")

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -2,7 +2,6 @@ add_subdirectory(Core)
 add_subdirectory(Automaton)
 add_subdirectory(LLVM)
 add_subdirectory(Trace)
-add_subdirectory(Verifier)
 add_subdirectory(Support)
 
 # Add requested solvers

diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt
@@ -39,4 +39,4 @@ llvm_map_components_to_libnames(GAZER_LLVM_LIBS core irreader transformutils sca
 message(STATUS "Using LLVM libraries: ${GAZER_LLVM_LIBS}")
 
 add_library(GazerLLVM SHARED ${SOURCE_FILES})
-target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerZ3Solver GazerAutomaton GazerVerifier)
+target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerZ3Solver GazerAutomaton)
diff --git a/tools/gazer-bmc/CMakeLists.txt b/tools/gazer-bmc/CMakeLists.txt
@@ -1,6 +1,8 @@
+add_subdirectory(Verifier)
+
 set(SOURCE_FILES
     gazer-bmc.cpp
 )
 
 add_executable(gazer-bmc ${SOURCE_FILES})
-target_link_libraries(gazer-bmc GazerLLVM GazerZ3Solver)
+target_link_libraries(gazer-bmc GazerLLVM GazerZ3Solver GazerVerifier)
diff --git a/src/Verifier/BmcTrace.cpp → tools/gazer-bmc/Verifier/BmcTrace.cpp b/src/Verifier/BmcTrace.cpp → tools/gazer-bmc/Verifier/BmcTrace.cpp
diff --git a/src/Verifier/BoundedModelChecker.cpp → ...azer-bmc/Verifier/BoundedModelChecker.cpp b/src/Verifier/BoundedModelChecker.cpp → ...azer-bmc/Verifier/BoundedModelChecker.cpp
diff --git a/src/Verifier/BoundedModelCheckerImpl.h → ...er-bmc/Verifier/BoundedModelCheckerImpl.h b/src/Verifier/BoundedModelCheckerImpl.h → ...er-bmc/Verifier/BoundedModelCheckerImpl.h
diff --git a/src/Verifier/CMakeLists.txt → tools/gazer-bmc/Verifier/CMakeLists.txt b/src/Verifier/CMakeLists.txt → tools/gazer-bmc/Verifier/CMakeLists.txt
@@ -1,6 +1,6 @@
 set(SOURCE_FILES
-    BoundedModelChecker.cpp
-    BmcTrace.cpp
+        BoundedModelChecker.cpp
+        BmcTrace.cpp
 )
 
 add_library(GazerVerifier SHARED ${SOURCE_FILES})