Skip to content

Commit 22c2ab9

Browse files
reukreuk
committed
Add CMakeLists
1 parent b846858 commit 22c2ab9

31 files changed

+852
-0
lines changed

‎CMakeLists.txt

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
cmake_minimum_required(VERSION 3.2)
2+
3+
include(GNUInstallDirs)
4+
5+
set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
6+
7+
add_subdirectory(src)
8+
9+
enable_testing()
10+
add_subdirectory(unit)

‎scripts/minisat2_CMakeLists.txt

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
cmake_minimum_required(VERSION 3.2)
2+
3+
# CBMC only uses part of minisat2.
4+
# This CMakeLists is designed to build just the parts that are needed.
5+
6+
set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
7+
set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
8+
set(CMAKE_BUILD_TYPE RelWithDebInfo)
9+
10+
add_library(minisat2-condensed
11+
minisat/simp/SimpSolver.cc
12+
minisat/core/Solver.cc
13+
)
14+
15+
set(CBMC_INCLUDE_DIR "" CACHE PATH "The path to CBMC util headers")
16+
17+
target_include_directories(minisat2-condensed
18+
PUBLIC
19+
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
20+
$<BUILD_INTERFACE:${CBMC_INCLUDE_DIR}>
21+
$<INSTALL_INTERFACE:include>
22+
)
23+
24+
install(TARGETS minisat2-condensed EXPORT minisat-condensed-targets
25+
LIBRARY DESTINATION lib
26+
ARCHIVE DESTINATION lib
27+
RUNTIME DESTINATION bin
28+
INCLUDES DESTINATION include
29+
)
30+
31+
install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
32+
33+
install(EXPORT minisat-condensed-targets DESTINATION lib/cmake/minisat-condensed)

‎src/CMakeLists.txt

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
cmake_minimum_required(VERSION 3.2)
2+
3+
# TODO
4+
# -[ ] Install profiles.
5+
# -[ ] Specify one of many different solver libraries.
6+
7+
project(CBMC)
8+
9+
set(CMAKE_CXX_STANDARD 11)
10+
set(CMAKE_CXX_STANDARD_REQUIRED true)
11+
12+
set(CMAKE_EXPORT_COMPILE_COMMANDS true)
13+
14+
find_package(BISON)
15+
find_package(FLEX)
16+
17+
set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
18+
set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
19+
set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
20+
21+
include(CPack)
22+
23+
find_package(Doxygen)
24+
if(DOXYGEN_FOUND)
25+
add_custom_target(doc
26+
${DOXYGEN_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/doxygen.cfg
27+
WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
28+
)
29+
endif(DOXYGEN_FOUND)
30+
31+
# Add a bison target named 'parser'.
32+
macro(generic_bison name)
33+
bison_target(
34+
parser
35+
${CMAKE_CURRENT_SOURCE_DIR}/parser.y
36+
${CMAKE_CURRENT_BINARY_DIR}/${name}_y.tab.cpp
37+
COMPILE_FLAGS -pyy${name}
38+
)
39+
set(renamed_parser_header ${CMAKE_CURRENT_BINARY_DIR}/${name}_y.tab.h)
40+
add_custom_command(OUTPUT ${renamed_parser_header}
41+
COMMAND ${CMAKE_COMMAND} -E copy ${BISON_parser_OUTPUT_HEADER} ${renamed_parser_header}
42+
MAIN_DEPENDENCY ${BISON_parser_OUTPUT_HEADER}
43+
)
44+
list(REMOVE_ITEM BISON_parser_OUTPUTS ${BISON_parser_OUTPUT_HEADER})
45+
list(APPEND BISON_parser_OUTPUTS ${renamed_parser_header})
46+
endmacro(generic_bison)
47+
48+
# Add a flex target named 'scanner'
49+
macro(generic_flex name)
50+
flex_target(
51+
scanner
52+
${CMAKE_CURRENT_SOURCE_DIR}/scanner.l
53+
${CMAKE_CURRENT_BINARY_DIR}/${name}_lex.yy.cpp
54+
COMPILE_FLAGS -Pyy${name}
55+
)
56+
endmacro(generic_flex)
57+
58+
# Set the public include locations for a target.
59+
macro(generic_includes name)
60+
target_include_directories(${name}
61+
PUBLIC
62+
${CBMC_BINARY_DIR}
63+
${CBMC_SOURCE_DIR}
64+
${CMAKE_CURRENT_BINARY_DIR}
65+
${CMAKE_CURRENT_SOURCE_DIR}
66+
)
67+
endmacro(generic_includes)
68+
69+
# Link optional modules.
70+
# Target is the name of the target with optional components.
71+
# Name is the name of the optional target.
72+
# Also adds a compile flag signalling to the preprocessor that the library is
73+
# used.
74+
macro(add_if_library target name)
75+
if(TARGET ${name})
76+
target_link_libraries(${target} ${name})
77+
78+
string(TOUPPER ${name} upper_name)
79+
string(REGEX REPLACE "-" "_" define ${upper_name})
80+
81+
target_compile_definitions(${target} PUBLIC HAVE_${define})
82+
endif()
83+
endmacro(add_if_library)
84+
85+
# EXTERNAL PROJECTS
86+
include(ExternalProject)
87+
set(extern_location ${CMAKE_CURRENT_BINARY_DIR}/extern)
88+
89+
set(extern_include_directory ${extern_location}/include)
90+
file(MAKE_DIRECTORY ${extern_include_directory})
91+
92+
set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
93+
94+
# minisat download
95+
# This downloads minisat2, then patches it.
96+
# Then, it injects a minimal CMakeLists.txt so that we can build just the bits
97+
# we actually want, without having to update the provided makefile.
98+
ExternalProject_Add(minisat2-extern
99+
PREFIX ${extern_location}
100+
URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
101+
PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
102+
COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
103+
CMAKE_ARGS -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR} -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
104+
BUILD_BYPRODUCTS ${minisat_lib}
105+
)
106+
107+
add_library(minisat2-condensed STATIC IMPORTED)
108+
set_target_properties(minisat2-condensed PROPERTIES
109+
IMPORTED_LOCATION ${minisat_lib}
110+
INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
111+
)
112+
add_dependencies(minisat2-condensed minisat2-extern)
113+
114+
# Override add_executable to automatically sign the target on OSX.
115+
function(add_executable name)
116+
_add_executable(${name} ${ARGN})
117+
set_target_properties(${name} PROPERTIES XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
118+
"Developer ID Application: Daniel Kroening")
119+
endfunction(add_executable)
120+
121+
add_subdirectory(analyses)
122+
add_subdirectory(ansi-c)
123+
add_subdirectory(assembler)
124+
add_subdirectory(big-int)
125+
add_subdirectory(cpp)
126+
add_subdirectory(goto-programs)
127+
add_subdirectory(goto-symex)
128+
add_subdirectory(jsil)
129+
add_subdirectory(json)
130+
add_subdirectory(langapi)
131+
add_subdirectory(linking)
132+
add_subdirectory(memory-models)
133+
add_subdirectory(path-symex)
134+
add_subdirectory(pointer-analysis)
135+
add_subdirectory(solvers)
136+
add_subdirectory(util)
137+
add_subdirectory(xmllang)
138+
add_subdirectory(java_bytecode)
139+
add_subdirectory(miniz)
140+
add_subdirectory(musketeer)
141+
add_subdirectory(clobber)
142+
add_subdirectory(cbmc)
143+
add_subdirectory(goto-cc)
144+
add_subdirectory(goto-instrument)
145+
add_subdirectory(symex)
146+
add_subdirectory(goto-analyzer)
147+
add_subdirectory(goto-diff)

‎src/analyses/CMakeLists.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
file(GLOB_RECURSE sources "*.cpp")
2+
file(GLOB_RECURSE headers "*.h")
3+
add_library(analyses ${sources} ${headers})
4+
5+
generic_includes(analyses)
6+
7+
target_link_libraries(analyses util pointer-analysis)

‎src/ansi-c/CMakeLists.txt

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
generic_bison(ansi_c)
2+
generic_flex(ansi_c)
3+
4+
add_executable(converter library/converter.cpp)
5+
6+
add_custom_command(OUTPUT converter_input.txt
7+
COMMAND cat ${CMAKE_CURRENT_SOURCE_DIR}/library/*.c > converter_input.txt
8+
)
9+
10+
add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
11+
COMMAND converter < converter_input.txt > ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
12+
DEPENDS converter_input.txt
13+
)
14+
15+
add_executable(file_converter file_converter.cpp)
16+
17+
function(make_inc name)
18+
add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${name}.inc
19+
COMMAND file_converter < ${CMAKE_CURRENT_SOURCE_DIR}/${name}.h > ${CMAKE_CURRENT_BINARY_DIR}/${name}.inc
20+
)
21+
endfunction(make_inc)
22+
23+
make_inc(arm_builtin_headers)
24+
make_inc(clang_builtin_headers)
25+
make_inc(cw_builtin_headers)
26+
make_inc(gcc_builtin_headers_alpha)
27+
make_inc(gcc_builtin_headers_arm)
28+
make_inc(gcc_builtin_headers_generic)
29+
make_inc(gcc_builtin_headers_ia32)
30+
make_inc(gcc_builtin_headers_ia32-2)
31+
make_inc(gcc_builtin_headers_ia32-3)
32+
make_inc(gcc_builtin_headers_ia32-4)
33+
make_inc(gcc_builtin_headers_math)
34+
make_inc(gcc_builtin_headers_mem_string)
35+
make_inc(gcc_builtin_headers_mips)
36+
make_inc(gcc_builtin_headers_omp)
37+
make_inc(gcc_builtin_headers_power)
38+
make_inc(gcc_builtin_headers_tm)
39+
make_inc(gcc_builtin_headers_ubsan)
40+
41+
file(GLOB_RECURSE sources "*.cpp")
42+
file(GLOB_RECURSE headers "*.h")
43+
add_library(ansi-c
44+
${sources}
45+
${headers}
46+
${BISON_parser_OUTPUTS}
47+
${FLEX_scanner_OUTPUTS}
48+
${CMAKE_CURRENT_BINARY_DIR}/arm_builtin_headers.inc
49+
${CMAKE_CURRENT_BINARY_DIR}/clang_builtin_headers.inc
50+
${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
51+
${CMAKE_CURRENT_BINARY_DIR}/cw_builtin_headers.inc
52+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_alpha.inc
53+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_arm.inc
54+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_generic.inc
55+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
56+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
57+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
58+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
59+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
60+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc
61+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mips.inc
62+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc
63+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc
64+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc
65+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
66+
)
67+
68+
generic_includes(ansi-c)
69+
70+
target_link_libraries(ansi-c util linking goto-programs assembler)

‎src/assembler/CMakeLists.txt

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
generic_flex(assembler)
2+
3+
file(GLOB_RECURSE sources "*.cpp")
4+
file(GLOB_RECURSE headers "*.h")
5+
add_library(assembler
6+
${sources}
7+
${headers}
8+
${FLEX_scanner_OUTPUTS}
9+
)
10+
11+
generic_includes(assembler)
12+
13+
target_link_libraries(assembler util)

‎src/big-int/CMakeLists.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
set(SRC bigint-func.cc bigint.cc)
2+
3+
add_executable(test-bigint ${SRC} bigint-test.cc)
4+
add_library(big-int ${SRC})
5+
6+
generic_includes(big-int)

‎src/cbmc/CMakeLists.txt

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# Library
2+
file(GLOB_RECURSE sources "*.cpp")
3+
file(GLOB_RECURSE headers "*.h")
4+
list(REMOVE_ITEM sources
5+
${CMAKE_CURRENT_SOURCE_DIR}/cbmc_main.cpp
6+
)
7+
add_library(cbmc-lib ${sources} ${headers})
8+
9+
generic_includes(cbmc-lib)
10+
11+
target_link_libraries(cbmc-lib
12+
ansi-c
13+
cpp
14+
linking
15+
big-int
16+
goto-programs
17+
goto-symex
18+
pointer-analysis
19+
goto-instrument-lib
20+
analyses
21+
langapi
22+
xml
23+
assembler
24+
solvers
25+
util
26+
json
27+
)
28+
29+
add_if_library(cbmc-lib bv_refinement)
30+
add_if_library(cbmc-lib java_bytecode)
31+
add_if_library(cbmc-lib jsil)
32+
add_if_library(cbmc-lib specc)
33+
add_if_library(cbmc-lib php)
34+
35+
# Executable
36+
add_executable(cbmc cbmc_main.cpp)
37+
target_link_libraries(cbmc cbmc-lib)
38+
39+
install(TARGETS cbmc DESTINATION bin)

‎src/clobber/CMakeLists.txt

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# Library
2+
file(GLOB_RECURSE sources "*.cpp")
3+
file(GLOB_RECURSE headers "*.h")
4+
list(REMOVE_ITEM sources
5+
${CMAKE_CURRENT_SOURCE_DIR}/clobber_main.cpp
6+
)
7+
add_library(clobber-lib ${sources} ${headers})
8+
9+
generic_includes(clobber-lib)
10+
11+
target_link_libraries(clobber-lib
12+
ansi-c
13+
cpp
14+
linking
15+
big-int
16+
goto-programs
17+
analyses
18+
langapi
19+
xml
20+
assembler
21+
solvers
22+
util
23+
goto-symex
24+
pointer-analysis
25+
goto-instrument-lib
26+
)
27+
28+
add_if_library(clobber-lib bv_refinement)
29+
add_if_library(clobber-lib java_bytecode)
30+
add_if_library(clobber-lib specc)
31+
add_if_library(clobber-lib php)
32+
33+
# Executable
34+
add_executable(clobber clobber_main.cpp)
35+
target_link_libraries(clobber clobber-lib)
36+

‎src/cpp/CMakeLists.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
file(GLOB_RECURSE sources "*.cpp")
2+
file(GLOB_RECURSE headers "*.h")
3+
add_library(cpp ${sources} ${headers})
4+
5+
generic_includes(cpp)
6+
7+
target_link_libraries(cpp util ansi-c)

0 commit comments

Comments
 (0)