Clean up CMake files after diffblue#1321

Author: reuk

CMakeLists.txt

@@ -25,14 +25,14 @@ elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     #   config.inc doesn't seem to do that currently
 endif()
 
-add_subdirectory(src)
-
 set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
 
 set(sat_impl "minisat2" CACHE STRING
     "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
 )
 
+add_subdirectory(src)
+
 if(${enable_cbmc_tests})
     enable_testing()
 endif()

src/goto-analyzer/CMakeLists.txt

@@ -3,9 +3,6 @@ file(GLOB_RECURSE sources "*.cpp")
 file(GLOB_RECURSE headers "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/goto_analyzer_main.cpp
-
-    # This doesn't build
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_goto_function.cpp
 )
 add_library(goto-analyzer-lib ${sources} ${headers})
 

src/goto-cc/CMakeLists.txt

@@ -3,15 +3,6 @@ file(GLOB_RECURSE sources "*.cpp")
 file(GLOB_RECURSE headers "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/goto_cc_main.cpp
-
-    # These files don't build
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/read_goto_object.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_goto_function.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_goto_function_hashing.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_goto_program.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_goto_program_hashing.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_irep_hashing.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/xml_binaries/xml_symbol_hashing.cpp
 )
 add_library(goto-cc-lib ${sources} ${headers})
 

src/goto-programs/CMakeLists.txt

@@ -1,8 +1,5 @@
 file(GLOB_RECURSE sources "*.cpp")
 file(GLOB_RECURSE headers "*.h")
-list(REMOVE_ITEM sources
-    ${CMAKE_CURRENT_SOURCE_DIR}/goto_convert_new_switch_case.cpp
-)
 add_library(goto-programs ${sources} ${headers})
 
 generic_includes(goto-programs)

src/java_bytecode/CMakeLists.txt

@@ -1,8 +1,5 @@
 file(GLOB_RECURSE sources "*.cpp")
 file(GLOB_RECURSE headers "*.h")
-list(REMOVE_ITEM sources
-    ${CMAKE_CURRENT_SOURCE_DIR}/java_bytecode_vtable.cpp
-)
 add_library(java_bytecode ${sources} ${headers})
 
 generic_includes(java_bytecode)

src/solvers/CMakeLists.txt

@@ -41,6 +41,9 @@ set(booleforce_source
 set(minibdd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp
 )
+set(limmat_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
+)
 
 file(GLOB_RECURSE sources "*.cpp")
 file(GLOB_RECURSE headers "*.h")
@@ -57,26 +60,19 @@ list(REMOVE_ITEM sources
     ${lingeling_source}
     ${booleforce_source}
     ${minibdd_source}
-
-    # Some files just don't build
-    ${CMAKE_CURRENT_SOURCE_DIR}/cvc/cvc_prop.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/dplib/dplib_prop.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/dplib/dplib_conv.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/dplib/dplib_dec.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/floatbv/float_approximation.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/smt1/smt1_prop.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/smt2/smt2_prop.cpp
+    ${limmat_source}
 )
 
 add_library(solvers ${sources} ${headers})
 
-if("${sat_impl}" STREQUAL "minisat2" AND TARGET minisat2-extern)
+if("${sat_impl}" STREQUAL "minisat2")
+    message(STATUS "Building solvers with minisat2")
     target_sources(solvers PRIVATE ${minisat2_source})
     add_dependencies(solvers minisat2-extern)
     target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
     target_link_libraries(solvers minisat2-condensed)
-elseif("${sat_impl}" STREQUAL "glucose" AND TARGET glucose-extern)
+elseif("${sat_impl}" STREQUAL "glucose")
+    message(STATUS "Building solvers with glucose")
     target_sources(solvers PRIVATE ${glucose_source})
     add_dependencies(solvers glucose-extern)
     target_compile_definitions(solvers PUBLIC SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)