diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 2a64acc4df0..e2ccc772f4f 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/jbmc/regression/CMakeLists.txt @@ -1,4 +1,4 @@ -set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl") +set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl") # For the best possible utilisation of multiple cores when # running tests in parallel, it is important that these directories are diff --git a/jbmc/src/CMakeLists.txt b/jbmc/src/CMakeLists.txt index a2058e084ac..ceb67b10b6c 100644 --- a/jbmc/src/CMakeLists.txt +++ b/jbmc/src/CMakeLists.txt @@ -7,7 +7,7 @@ macro(generic_includes name) ${JBMC_BINARY_DIR} ${JBMC_SOURCE_DIR} ${CBMC_BINARY_DIR} - ${CBMC_SOURCE_DIR} + ${CBMC_SOURCE_DIR}/src ${CMAKE_CURRENT_BINARY_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ${CUDD_INCLUDE} diff --git a/jbmc/unit/CMakeLists.txt b/jbmc/unit/CMakeLists.txt index 781e39b66ac..510ceacd69a 100644 --- a/jbmc/unit/CMakeLists.txt +++ b/jbmc/unit/CMakeLists.txt @@ -1,5 +1,5 @@ file(GLOB_RECURSE sources "*.cpp" "*.h") -list(APPEND sources ${CBMC_SOURCE_DIR}/../unit/unit_tests.cpp) +list(APPEND sources ${CBMC_SOURCE_DIR}/unit/unit_tests.cpp) file(GLOB_RECURSE java-testing_utils "java-testing-utils/*.cpp" "java-testing-utils/*.h") @@ -14,8 +14,8 @@ add_executable(java-unit ${sources}) target_include_directories(java-unit PUBLIC ${CBMC_BINARY_DIR} - ${CBMC_SOURCE_DIR} - ${CBMC_SOURCE_DIR}/../unit + ${CBMC_SOURCE_DIR}/src + ${CBMC_SOURCE_DIR}/unit ${CMAKE_CURRENT_SOURCE_DIR} ) target_link_libraries(java-unit diff --git a/jbmc/unit/java-testing-utils/CMakeLists.txt b/jbmc/unit/java-testing-utils/CMakeLists.txt index 0dcba22e1a1..127b99a7407 100644 --- a/jbmc/unit/java-testing-utils/CMakeLists.txt +++ b/jbmc/unit/java-testing-utils/CMakeLists.txt @@ -7,5 +7,5 @@ target_link_libraries(java-testing-utils target_include_directories(java-testing-utils PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}/.. - ${CBMC_SOURCE_DIR}/../unit + ${CBMC_SOURCE_DIR}/unit ) diff --git a/regression/libcprover-cpp/CMakeLists.txt b/regression/libcprover-cpp/CMakeLists.txt index f7a6b864f7f..0c57cb71d46 100644 --- a/regression/libcprover-cpp/CMakeLists.txt +++ b/regression/libcprover-cpp/CMakeLists.txt @@ -4,13 +4,13 @@ cprover_default_properties(api-binary-driver) target_include_directories(api-binary-driver PUBLIC ${CBMC_BINARY_DIR} - ${CBMC_SOURCE_DIR} + ${CBMC_SOURCE_DIR}/src # TODO: Should be fixed for the proper include form. ${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/) target_link_libraries(api-binary-driver goto-programs util langapi ansi-c cprover-api-cpp) # Enable test running -set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl") +set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl") macro(add_test_pl_profile name cmdline flag profile) add_test( diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c7fb54d4e46..7583d0ce6d1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,5 +1,3 @@ -project(CBMC VERSION ${CBMC_VERSION}) - find_package(BISON REQUIRED) find_package(FLEX REQUIRED) @@ -66,8 +64,8 @@ endmacro(generic_flex) macro(generic_includes name) target_include_directories(${name} PUBLIC - ${CBMC_BINARY_DIR} - ${CBMC_SOURCE_DIR} + ${CBMC_BINARY_DIR}/src + ${CBMC_SOURCE_DIR}/src ${CMAKE_CURRENT_BINARY_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 003a0d957b1..ab8d11117b1 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -59,7 +59,7 @@ list(REMOVE_ITEM sources add_library(solvers ${sources}) -include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake") +include("${CBMC_SOURCE_DIR}/cmake/DownloadProject.cmake") foreach(SOLVER ${sat_impl}) if("${SOLVER}" STREQUAL "minisat2") @@ -70,8 +70,8 @@ foreach(SOLVER ${sat_impl}) # to 2 times) download_project(PROJ minisat2 URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/minisat-2.2.1-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/minisat2_CMakeLists.txt CMakeLists.txt URL_MD5 27faa19ee0508660bd6fb7f894646d42 ) @@ -103,8 +103,8 @@ foreach(SOLVER ${sat_impl}) download_project(PROJ glucose URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt URL_MD5 7c539c62c248b74210aef7414787323a ) @@ -122,8 +122,8 @@ foreach(SOLVER ${sat_impl}) download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt COMMAND ./configure URL_MD5 9fc2a66196b86adceb822a583318cc35 ) @@ -145,7 +145,7 @@ foreach(SOLVER ${sat_impl}) download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch COMMAND ./configure URL_MD5 9fc2a66196b86adceb822a583318cc35 ) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 6d693238a2a..8d6da3d0771 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -5,7 +5,7 @@ find_package(Git) if(GIT_FOUND) file(WRITE ${CMAKE_BINARY_DIR}/version.cmake " - file(STRINGS \${CBMC_SOURCE_DIR}/config.inc + file(STRINGS \${SRC}/src/config.inc config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\") string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v}) execute_process( @@ -20,7 +20,7 @@ if(GIT_FOUND) else() file(WRITE ${CMAKE_BINARY_DIR}/version.cmake " - file(STRINGS \${CBMC_SOURCE_DIR}/config.inc + file(STRINGS \${SRC}/src/config.inc config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\") string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v}) set(GIT_INFO \"n/a\") @@ -35,7 +35,7 @@ add_custom_target( generate_version_cpp BYPRODUCTS version.cpp COMMAND ${CMAKE_COMMAND} - -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR} + -D SRC=${CBMC_SOURCE_DIR} -D CUR=${CMAKE_CURRENT_BINARY_DIR} -P ${CMAKE_BINARY_DIR}/version.cmake ) diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 9e9985a9b61..6435787eec3 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -75,7 +75,7 @@ add_executable(unit ${sources}) target_include_directories(unit PUBLIC ${CBMC_BINARY_DIR} - ${CBMC_SOURCE_DIR} + ${CBMC_SOURCE_DIR}/src ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR} ${CUDD_INCLUDE} diff --git a/unit/libcprover-cpp/CMakeLists.txt b/unit/libcprover-cpp/CMakeLists.txt index 6cd12d3d793..6eafaf1d580 100644 --- a/unit/libcprover-cpp/CMakeLists.txt +++ b/unit/libcprover-cpp/CMakeLists.txt @@ -4,7 +4,7 @@ file(GLOB_RECURSE sources "*.cpp" "*.h") add_executable(lib-unit ${sources}) target_include_directories(lib-unit PUBLIC - ${CBMC_SOURCE_DIR}/libcprover-cpp + ${CBMC_SOURCE_DIR}/src/libcprover-cpp ) target_link_libraries(lib-unit cprover-api-cpp