Tidy up CMakeLists

CMakeLists.txt

@@ -41,3 +41,49 @@ if(${enable_cbmc_tests})
 endif()
 add_subdirectory(unit)
 add_subdirectory(regression)
+
+set_target_properties(
+    analyses
+    ansi-c
+    assembler
+    big-int
+    cbmc
+    cbmc-lib
+    clobber
+    clobber-lib
+    cpp
+    driver
+    goto-analyzer
+    goto-analyzer-lib
+    goto-cc
+    goto-cc-lib
+    goto-diff
+    goto-diff-lib
+    goto-instrument
+    goto-instrument-lib
+    goto-programs
+    goto-symex
+    java_bytecode
+    jbmc
+    jbmc-lib
+    jsil
+    json
+    langapi
+    linking
+    miniBDD
+    miniz
+    mmcc
+    pointer-analysis
+    solvers
+    string_utils
+    test-bigint
+    testing-utils
+    unit
+    util
+    xml
+
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)

regression/CMakeLists.txt

@@ -1,6 +1,3 @@
-set(CMAKE_CXX_STANDARD 11)
-set(CMAKE_CXX_STANDARD_REQUIRED true)
-
 set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
 
 macro(add_test_pl_profile name cmdline flag profile)

scripts/glucose_CMakeLists.txt

@@ -6,6 +6,14 @@ add_library(glucose-condensed
     core/Solver.cc
 )
 
+set_target_properties(
+    glucose-condensed
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)
+
 target_include_directories(glucose-condensed
     PUBLIC
     ${CMAKE_CURRENT_SOURCE_DIR}

scripts/minisat2_CMakeLists.txt

@@ -6,6 +6,14 @@ add_library(minisat2-condensed
     minisat/core/Solver.cc
 )
 
+set_target_properties(
+    minisat2-condensed
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)
+
 target_include_directories(minisat2-condensed
     PUBLIC
     ${CMAKE_CURRENT_SOURCE_DIR}

src/CMakeLists.txt

@@ -1,25 +1,8 @@
-cmake_minimum_required(VERSION 3.2)
-
-#   TODO
-#   -[ ] Install profiles.
-#   -[ ] Specify one of many different solver libraries.
-
 project(CBMC)
 
-set(CMAKE_CXX_STANDARD 11)
-set(CMAKE_CXX_STANDARD_REQUIRED true)
-
-set(CMAKE_EXPORT_COMPILE_COMMANDS true)
-
 find_package(BISON)
 find_package(FLEX)
 
-set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
-set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
-set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
-
-include(CPack)
-
 find_package(Doxygen)
 if(DOXYGEN_FOUND)
     add_custom_target(doc
@@ -97,13 +80,6 @@ macro(add_if_library target name)
     endif()
 endmacro(add_if_library)
 
-#   Override add_executable to automatically sign the target on OSX.
-function(add_executable name)
-    _add_executable(${name} ${ARGN})
-    set_target_properties(${name} PROPERTIES XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
-        "Developer ID Application: Daniel Kroening")
-endfunction(add_executable)
-
 add_subdirectory(analyses)
 add_subdirectory(ansi-c)
 add_subdirectory(assembler)

src/analyses/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(analyses ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(analyses ${sources})
 
 generic_includes(analyses)
 

src/ansi-c/CMakeLists.txt

@@ -96,8 +96,7 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
 )
 
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 
 list(REMOVE_ITEM sources
     "${CMAKE_CURRENT_SOURCE_DIR}/library/converter.cpp"
@@ -106,7 +105,6 @@ list(REMOVE_ITEM sources
 
 add_library(ansi-c
     ${sources}
-    ${headers}
     ${BISON_parser_OUTPUTS}
     ${FLEX_scanner_OUTPUTS}
 )

src/assembler/CMakeLists.txt

@@ -1,10 +1,8 @@
 generic_flex(assembler)
 
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_library(assembler
     ${sources}
-    ${headers}
     ${FLEX_scanner_OUTPUTS}
 )
 

src/cbmc/CMakeLists.txt

@@ -1,10 +1,9 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/cbmc_main.cpp
 )
-add_library(cbmc-lib ${sources} ${headers})
+add_library(cbmc-lib ${sources})
 
 generic_includes(cbmc-lib)
 

src/clobber/CMakeLists.txt

@@ -1,10 +1,9 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/clobber_main.cpp
 )
-add_library(clobber-lib ${sources} ${headers})
+add_library(clobber-lib ${sources})
 
 generic_includes(clobber-lib)
 

src/cpp/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(cpp ${sources} ${headers}) 
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(cpp ${sources})
 
 generic_includes(cpp)
 

src/goto-analyzer/CMakeLists.txt

@@ -1,10 +1,9 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/goto_analyzer_main.cpp
 )
-add_library(goto-analyzer-lib ${sources} ${headers})
+add_library(goto-analyzer-lib ${sources})
 
 generic_includes(goto-analyzer-lib)
 

src/goto-cc/CMakeLists.txt

@@ -1,10 +1,9 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/goto_cc_main.cpp
 )
-add_library(goto-cc-lib ${sources} ${headers})
+add_library(goto-cc-lib ${sources})
 
 generic_includes(goto-cc-lib)
 

src/goto-diff/CMakeLists.txt

@@ -1,10 +1,9 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/goto_diff_main.cpp
 )
-add_library(goto-diff-lib ${sources} ${headers})
+add_library(goto-diff-lib ${sources})
 
 generic_includes(goto-diff-lib)
 

src/goto-instrument/CMakeLists.txt

@@ -1,13 +1,12 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/goto_instrument_main.cpp
 
     # This doesn't build
     ${CMAKE_CURRENT_SOURCE_DIR}/accelerate/linearize.cpp
 )
-add_library(goto-instrument-lib ${sources} ${headers})
+add_library(goto-instrument-lib ${sources})
 
 generic_includes(goto-instrument-lib)
 

src/goto-programs/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(goto-programs ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(goto-programs ${sources})
 
 generic_includes(goto-programs)
 

src/goto-symex/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(goto-symex ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(goto-symex ${sources})
 
 generic_includes(goto-symex)
 

src/java_bytecode/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(java_bytecode ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(java_bytecode ${sources})
 
 generic_includes(java_bytecode)
 

src/jbmc/CMakeLists.txt

@@ -1,10 +1,9 @@
 # Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/jbmc_main.cpp
 )
-add_library(jbmc-lib ${sources} ${headers})
+add_library(jbmc-lib ${sources})
 
 generic_includes(jbmc-lib)
 

src/jsil/CMakeLists.txt

@@ -1,11 +1,9 @@
 generic_bison(jsil)
 generic_flex(jsil)
 
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_library(jsil
     ${sources}
-    ${headers}
     ${BISON_parser_OUTPUTS}
     ${FLEX_scanner_OUTPUTS}
 )

src/json/CMakeLists.txt

@@ -1,11 +1,9 @@
 generic_bison(json)
 generic_flex(json)
 
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(json 
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(json
     ${sources}
-    ${headers}
     ${BISON_parser_OUTPUTS}
     ${FLEX_scanner_OUTPUTS}
 )

src/langapi/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(langapi ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(langapi ${sources})
 
 generic_includes(langapi)
 

src/linking/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(linking ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(linking ${sources})
 
 generic_includes(linking)
 

src/memory-models/CMakeLists.txt

@@ -1,11 +1,9 @@
 generic_bison(mm)
 generic_flex(mm)
 
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_library(mmcc
     ${sources}
-    ${headers}
     ${BISON_parser_OUTPUTS}
     ${FLEX_scanner_OUTPUTS}
 )

src/miniz/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(miniz ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(miniz ${sources})
 
 generic_includes(miniz)
 

src/pointer-analysis/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(pointer-analysis ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(pointer-analysis ${sources})
 
 generic_includes(pointer-analysis)
 

src/solvers/CMakeLists.txt

@@ -45,8 +45,7 @@ set(limmat_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
 )
 
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
+file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${chaff_source}
     ${minisat_source}
@@ -63,7 +62,7 @@ list(REMOVE_ITEM sources
     ${limmat_source}
 )
 
-add_library(solvers ${sources} ${headers})
+add_library(solvers ${sources})
 
 include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
 

src/util/CMakeLists.txt

@@ -1,6 +1,5 @@
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-add_library(util ${sources} ${headers})
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(util ${sources})
 
 generic_includes(util)