File tree 30 files changed +108
-107
lines changed
30 files changed +108
-107
lines changed Original file line number Diff line number Diff line change @@ -41,3 +41,49 @@ if(${enable_cbmc_tests})
41
41
endif ()
42
42
add_subdirectory (unit)
43
43
add_subdirectory (regression)
44
+
45
+ set_target_properties (
46
+ analyses
47
+ ansi-c
48
+ assembler
49
+ big-int
50
+ cbmc
51
+ cbmc-lib
52
+ clobber
53
+ clobber-lib
54
+ cpp
55
+ driver
56
+ goto-analyzer
57
+ goto-analyzer-lib
58
+ goto-cc
59
+ goto-cc-lib
60
+ goto-diff
61
+ goto-diff-lib
62
+ goto-instrument
63
+ goto-instrument-lib
64
+ goto-programs
65
+ goto-symex
66
+ java_bytecode
67
+ jbmc
68
+ jbmc-lib
69
+ jsil
70
+ json
71
+ langapi
72
+ linking
73
+ miniBDD
74
+ miniz
75
+ mmcc
76
+ pointer-analysis
77
+ solvers
78
+ string_utils
79
+ test -bigint
80
+ testing-utils
81
+ unit
82
+ util
83
+ xml
84
+
85
+ PROPERTIES
86
+ CXX_STANDARD 11
87
+ CXX_STANDARD_REQUIRED true
88
+ XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
89
+ )
Original file line number Diff line number Diff line change 1
- set (CMAKE_CXX_STANDARD 11)
2
- set (CMAKE_CXX_STANDARD_REQUIRED true )
3
-
4
1
set (test_pl_path "${CMAKE_CURRENT_SOURCE_DIR} /test.pl" )
5
2
6
3
macro (add_test_pl_profile name cmdline flag profile)
Original file line number Diff line number Diff line change @@ -6,6 +6,14 @@ add_library(glucose-condensed
6
6
core/Solver.cc
7
7
)
8
8
9
+ set_target_properties(
10
+ glucose-condensed
11
+ PROPERTIES
12
+ CXX_STANDARD 11
13
+ CXX_STANDARD_REQUIRED true
14
+ XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
15
+ )
16
+
9
17
target_include_directories(glucose-condensed
10
18
PUBLIC
11
19
${CMAKE_CURRENT_SOURCE_DIR}
Original file line number Diff line number Diff line change @@ -6,6 +6,14 @@ add_library(minisat2-condensed
6
6
minisat/core/Solver.cc
7
7
)
8
8
9
+ set_target_properties(
10
+ minisat2-condensed
11
+ PROPERTIES
12
+ CXX_STANDARD 11
13
+ CXX_STANDARD_REQUIRED true
14
+ XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
15
+ )
16
+
9
17
target_include_directories(minisat2-condensed
10
18
PUBLIC
11
19
${CMAKE_CURRENT_SOURCE_DIR}
Original file line number Diff line number Diff line change 1
- cmake_minimum_required (VERSION 3.2)
2
-
3
- # TODO
4
- # -[ ] Install profiles.
5
- # -[ ] Specify one of many different solver libraries.
6
-
7
1
project (CBMC)
8
2
9
- set (CMAKE_CXX_STANDARD 11)
10
- set (CMAKE_CXX_STANDARD_REQUIRED true )
11
-
12
- set (CMAKE_EXPORT_COMPILE_COMMANDS true )
13
-
14
3
find_package (BISON)
15
4
find_package (FLEX)
16
5
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
6
find_package (Doxygen)
24
7
if (DOXYGEN_FOUND)
25
8
add_custom_target (doc
@@ -97,13 +80,6 @@ macro(add_if_library target name)
97
80
endif ()
98
81
endmacro (add_if_library)
99
82
100
- # Override add_executable to automatically sign the target on OSX.
101
- function (add_executable name )
102
- _add_executable(${name} ${ARGN} )
103
- set_target_properties (${name} PROPERTIES XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
104
- "Developer ID Application: Daniel Kroening" )
105
- endfunction (add_executable)
106
-
107
83
add_subdirectory (analyses)
108
84
add_subdirectory (ansi-c)
109
85
add_subdirectory (assembler)
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (analyses ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (analyses ${sources} )
4
3
5
4
generic_includes(analyses)
6
5
Original file line number Diff line number Diff line change @@ -96,8 +96,7 @@ set(extra_dependencies
96
96
${CMAKE_CURRENT_BINARY_DIR} /library-check.stamp
97
97
)
98
98
99
- file (GLOB_RECURSE sources "*.cpp" )
100
- file (GLOB_RECURSE headers "*.h" )
99
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
101
100
102
101
list (REMOVE_ITEM sources
103
102
"${CMAKE_CURRENT_SOURCE_DIR} /library/converter.cpp"
@@ -106,7 +105,6 @@ list(REMOVE_ITEM sources
106
105
107
106
add_library (ansi-c
108
107
${sources}
109
- ${headers}
110
108
${BISON_parser_OUTPUTS}
111
109
${FLEX_scanner_OUTPUTS}
112
110
)
Original file line number Diff line number Diff line change 1
1
generic_flex(assembler)
2
2
3
- file (GLOB_RECURSE sources "*.cpp" )
4
- file (GLOB_RECURSE headers "*.h" )
3
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
5
4
add_library (assembler
6
5
${sources}
7
- ${headers}
8
6
${FLEX_scanner_OUTPUTS}
9
7
)
10
8
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /cbmc_main.cpp
6
5
)
7
- add_library (cbmc-lib ${sources} ${headers} )
6
+ add_library (cbmc-lib ${sources} )
8
7
9
8
generic_includes(cbmc-lib)
10
9
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /clobber_main.cpp
6
5
)
7
- add_library (clobber-lib ${sources} ${headers} )
6
+ add_library (clobber-lib ${sources} )
8
7
9
8
generic_includes(clobber-lib)
10
9
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (cpp ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (cpp ${sources} )
4
3
5
4
generic_includes(cpp)
6
5
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /goto_analyzer_main.cpp
6
5
)
7
- add_library (goto-analyzer-lib ${sources} ${headers} )
6
+ add_library (goto-analyzer-lib ${sources} )
8
7
9
8
generic_includes(goto-analyzer-lib)
10
9
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /goto_cc_main.cpp
6
5
)
7
- add_library (goto-cc-lib ${sources} ${headers} )
6
+ add_library (goto-cc-lib ${sources} )
8
7
9
8
generic_includes(goto-cc-lib)
10
9
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /goto_diff_main.cpp
6
5
)
7
- add_library (goto-diff-lib ${sources} ${headers} )
6
+ add_library (goto-diff-lib ${sources} )
8
7
9
8
generic_includes(goto-diff-lib)
10
9
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /goto_instrument_main.cpp
6
5
7
6
# This doesn't build
8
7
${CMAKE_CURRENT_SOURCE_DIR} /accelerate/linearize.cpp
9
8
)
10
- add_library (goto-instrument-lib ${sources} ${headers} )
9
+ add_library (goto-instrument-lib ${sources} )
11
10
12
11
generic_includes(goto-instrument-lib)
13
12
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (goto-programs ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (goto-programs ${sources} )
4
3
5
4
generic_includes(goto-programs)
6
5
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (goto-symex ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (goto-symex ${sources} )
4
3
5
4
generic_includes(goto-symex)
6
5
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (java_bytecode ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (java_bytecode ${sources} )
4
3
5
4
generic_includes(java_bytecode)
6
5
Original file line number Diff line number Diff line change 1
1
# Library
2
- file (GLOB_RECURSE sources "*.cpp" )
3
- file (GLOB_RECURSE headers "*.h" )
2
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
4
3
list (REMOVE_ITEM sources
5
4
${CMAKE_CURRENT_SOURCE_DIR} /jbmc_main.cpp
6
5
)
7
- add_library (jbmc-lib ${sources} ${headers} )
6
+ add_library (jbmc-lib ${sources} )
8
7
9
8
generic_includes(jbmc-lib)
10
9
Original file line number Diff line number Diff line change 1
1
generic_bison(jsil)
2
2
generic_flex(jsil)
3
3
4
- file (GLOB_RECURSE sources "*.cpp" )
5
- file (GLOB_RECURSE headers "*.h" )
4
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
6
5
add_library (jsil
7
6
${sources}
8
- ${headers}
9
7
${BISON_parser_OUTPUTS}
10
8
${FLEX_scanner_OUTPUTS}
11
9
)
Original file line number Diff line number Diff line change 1
1
generic_bison(json)
2
2
generic_flex(json)
3
3
4
- file (GLOB_RECURSE sources "*.cpp" )
5
- file (GLOB_RECURSE headers "*.h" )
6
- add_library (json
4
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
5
+ add_library (json
7
6
${sources}
8
- ${headers}
9
7
${BISON_parser_OUTPUTS}
10
8
${FLEX_scanner_OUTPUTS}
11
9
)
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (langapi ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (langapi ${sources} )
4
3
5
4
generic_includes(langapi)
6
5
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (linking ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (linking ${sources} )
4
3
5
4
generic_includes(linking)
6
5
Original file line number Diff line number Diff line change 1
1
generic_bison(mm)
2
2
generic_flex(mm)
3
3
4
- file (GLOB_RECURSE sources "*.cpp" )
5
- file (GLOB_RECURSE headers "*.h" )
4
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
6
5
add_library (mmcc
7
6
${sources}
8
- ${headers}
9
7
${BISON_parser_OUTPUTS}
10
8
${FLEX_scanner_OUTPUTS}
11
9
)
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (miniz ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (miniz ${sources} )
4
3
5
4
generic_includes(miniz)
6
5
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (pointer-analysis ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (pointer-analysis ${sources} )
4
3
5
4
generic_includes(pointer-analysis)
6
5
Original file line number Diff line number Diff line change @@ -45,8 +45,7 @@ set(limmat_source
45
45
${CMAKE_CURRENT_SOURCE_DIR} /sat/satcheck_limmat.cpp
46
46
)
47
47
48
- file (GLOB_RECURSE sources "*.cpp" )
49
- file (GLOB_RECURSE headers "*.h" )
48
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
50
49
list (REMOVE_ITEM sources
51
50
${chaff_source}
52
51
${minisat_source}
@@ -63,7 +62,7 @@ list(REMOVE_ITEM sources
63
62
${limmat_source}
64
63
)
65
64
66
- add_library (solvers ${sources} ${headers} )
65
+ add_library (solvers ${sources} )
67
66
68
67
include ("${CBMC_SOURCE_DIR} /../cmake/DownloadProject.cmake" )
69
68
Original file line number Diff line number Diff line change 1
- file (GLOB_RECURSE sources "*.cpp" )
2
- file (GLOB_RECURSE headers "*.h" )
3
- add_library (util ${sources} ${headers} )
1
+ file (GLOB_RECURSE sources "*.cpp" "*.h" )
2
+ add_library (util ${sources} )
4
3
5
4
generic_includes(util)
6
5
You can’t perform that action at this time.
0 commit comments