Skip to content

Commit 3ede81b

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #1293 from reuk/cmake-develop
Add CMakeLists alongside existing makefiles
2 parents 69d05a9 + 4dde3c5 commit 3ede81b

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

61 files changed

+1292
-76
lines changed

‎.travis.yml

+28
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,34 @@ jobs:
137137
- EXTRA_CXXFLAGS="-DDEBUG"
138138
script: echo "Not running any tests for a debug build."
139139

140+
- stage: Test different OS/CXX/Flags
141+
os: linux
142+
cache: ccache
143+
env:
144+
- BUILD_SYSTEM=cmake
145+
addons:
146+
apt:
147+
sources:
148+
- ubuntu-toolchain-r-test
149+
packages:
150+
- g++-5
151+
install:
152+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
153+
- cmake --build build -- -j4
154+
script: (cd build; ctest -V -L CORE)
155+
156+
- stage: Test different OS/CXX/Flags
157+
os: osx
158+
cache: ccache
159+
env:
160+
- BUILD_SYSTEM=cmake
161+
- CCACHE_CPP2=yes
162+
install:
163+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
164+
- cmake --build build -- -j4
165+
script: (cd build; ctest -V -L CORE)
166+
167+
140168
allow_failures:
141169
- <<: *linter-stage
142170

‎CMakeLists.txt

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
cmake_minimum_required(VERSION 3.2)
2+
3+
find_program(CCACHE_PROGRAM ccache)
4+
if(CCACHE_PROGRAM)
5+
set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
6+
endif()
7+
8+
set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
9+
10+
include(GNUInstallDirs)
11+
12+
set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
13+
set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
14+
set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
15+
16+
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
17+
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
18+
)
19+
# Ensure NDEBUG is not set for release builds
20+
set(CMAKE_CXX_FLAGS_RELEASE "-O2")
21+
# Enable lots of warnings
22+
set(CMAKE_CXX_FLAGS "-Wall -Wpedantic -Werror")
23+
elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
24+
# This would be the place to enable warnings for Windows builds, although
25+
# config.inc doesn't seem to do that currently
26+
endif()
27+
28+
set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
29+
30+
set(sat_impl "minisat2" CACHE STRING
31+
"This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
32+
)
33+
34+
add_subdirectory(src)
35+
36+
if(${enable_cbmc_tests})
37+
enable_testing()
38+
endif()
39+
add_subdirectory(unit)
40+
add_subdirectory(regression)

‎COMPILING

+48-1
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ Follow these instructions:
171171
BUILD_ENV = MSVC
172172

173173
Open the Visual Studio Command prompt, and then bash.exe -login from
174-
Cygwin from in there.
174+
Cygwin from in there.
175175

176176
3) Type cd src; make - that should do it.
177177

@@ -183,6 +183,53 @@ can be used for building with MSBuild. Note that you still need to run
183183
flex/bison using "make generated_files" before opening the project.
184184

185185

186+
WORKING WITH CMAKE (EXPERIMENTAL)
187+
---------------------------------
188+
189+
There is an experimental build based on CMake instead of hand-written
190+
makefiles. It should work on a wider variety of systems than the standard
191+
makefile build, and can integrate better with IDEs and static-analysis tools.
192+
193+
0) Run `cmake --version`. If you get a command-not-found error, or the installed
194+
version is lower than 3.2, go and install a new version. Most Linux
195+
distributions have a package for CMake, and Mac users can get it through
196+
Homebrew. Windows users should download it manually from cmake.org.
197+
198+
1) Create a directory to store your build:
199+
`mkdir build`
200+
Run this from the *top level* folder of the project. This is different from
201+
the other builds, which require you to `cd src` first.
202+
203+
2) Generate build files with CMake:
204+
`cmake -H. -Bbuild`
205+
This command tells CMake to use the configuration in the current directory,
206+
and to generate build files into the `build` directory.
207+
This is the point to specify custom build settings, such as compilers and
208+
build back-ends. You can use clang (for example) by adding the argument
209+
`-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
210+
CMake to generate IDE projects by supplying the `-G` flag.
211+
Run `cmake -G` for a comprehensive list of supported back-ends.
212+
213+
Generally it is not necessary to manually specify individual compiler or
214+
linker flags, as CMake defines a number of "build modes" including Debug
215+
and Release modes. To build in a particular mode, add the flag
216+
`-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation.
217+
218+
If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
219+
`-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
220+
sanitizers.
221+
222+
Finally, to enable building universal binaries on macOS, you can pass the
223+
flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
224+
the build will just be for the architecture of your machine.
225+
226+
3) Run the build:
227+
`cmake --build build`
228+
This command tells CMake to invoke the correct tool to run the build in the
229+
`build` directory. You can also use the build back-end directly by invoking
230+
`make`, `ninja`, or opening the generated IDE project as appropriate.
231+
232+
186233
WORKING WITH ECLIPSE
187234
--------------------
188235

‎appveyor.yml

-13
Original file line numberDiff line numberDiff line change
@@ -60,19 +60,6 @@ build_script:
6060
test_script:
6161
- cmd: |
6262
cd regression
63-
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" ansi-c/Makefile
64-
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" cpp/Makefile
65-
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument/chain.sh
66-
sed -i "15s/.*/$goto_cc $name.c/" goto-instrument/chain.sh
67-
sed -i "16i mv $name.exe $name.gb" goto-instrument/chain.sh
68-
sed -i "23s/.*/ $goto_cc ${name}-mod.c/" goto-instrument/chain.sh
69-
sed -i "24i mv ${name}-mod.exe $name-mod.gb" goto-instrument/chain.sh
70-
cat goto-instrument/chain.sh
71-
72-
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument-typedef/chain.sh || true
73-
sed -i "12s/.*/$GC $NAME.c --function fun/" goto-instrument-typedef/chain.sh || true
74-
sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
75-
cat goto-instrument-typedef/chain.sh || true
7663
7764
rem HACK disable failing tests
7865
rmdir /s /q ansi-c\arch_flags_mcpu_bad

‎regression/CMakeLists.txt

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
set(CMAKE_CXX_STANDARD 11)
2+
set(CMAKE_CXX_STANDARD_REQUIRED true)
3+
4+
set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
5+
6+
macro(add_test_pl_profile name cmdline flag profile)
7+
add_test(
8+
NAME "${name}-${profile}"
9+
COMMAND ${test_pl_path} -c ${cmdline} ${flag}
10+
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
11+
)
12+
set_tests_properties("${name}-${profile}" PROPERTIES
13+
LABELS "${profile}"
14+
)
15+
endmacro(add_test_pl_profile)
16+
17+
macro(add_test_pl_tests name cmdline)
18+
add_test_pl_profile("${name}" "${cmdline}" -C CORE)
19+
add_test_pl_profile("${name}" "${cmdline}" -T THOROUGH)
20+
add_test_pl_profile("${name}" "${cmdline}" -F FUTURE)
21+
add_test_pl_profile("${name}" "${cmdline}" -K KNOWNBUG)
22+
endmacro(add_test_pl_tests)
23+
24+
add_subdirectory(ansi-c)
25+
add_subdirectory(cbmc)
26+
add_subdirectory(cbmc-java)
27+
add_subdirectory(cbmc-java-inheritance)
28+
add_subdirectory(cpp)
29+
add_subdirectory(goto-analyzer)
30+
add_subdirectory(goto-diff)
31+
add_subdirectory(goto-instrument)
32+
add_subdirectory(goto-instrument-typedef)
33+
add_subdirectory(invariants)
34+
add_subdirectory(strings)
35+
add_subdirectory(strings-smoke-tests)
36+
add_subdirectory(test-script)

‎regression/ansi-c/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"ansi-c"
3+
"$<TARGET_FILE:goto-cc>"
4+
)

‎regression/ansi-c/Makefile

+11-2
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,22 @@
11
default: tests.log
22

3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
else
9+
exe=../../../src/goto-cc/goto-cc
10+
endif
11+
312
test:
4-
@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
13+
@if ! ../test.pl -c $(exe) ; then \
514
../failed-tests-printer.pl ; \
615
exit 1 ; \
716
fi
817

918
tests.log: ../test.pl
10-
@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
19+
@if ! ../test.pl -c $(exe) ; then \
1120
../failed-tests-printer.pl ; \
1221
exit 1 ; \
1322
fi

‎regression/cbmc-java-inheritance/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"cbmc-java-inheritance"
3+
"$<TARGET_FILE:cbmc>"
4+
)

‎regression/cbmc-java/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"cbmc-java"
3+
"$<TARGET_FILE:cbmc>"
4+
)

‎regression/cbmc/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"cbmc"
3+
"$<TARGET_FILE:cbmc>"
4+
)

‎regression/cpp/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"cpp"
3+
"$<TARGET_FILE:goto-cc>"
4+
)

‎regression/cpp/Makefile

+11-2
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,22 @@
11
default: tests.log
22

3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
else
9+
exe=../../../src/goto-cc/goto-cc
10+
endif
11+
312
test:
4-
@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
13+
@if ! ../test.pl -c $(exe) ; then \
514
../failed-tests-printer.pl ; \
615
exit 1 ; \
716
fi
817

918
tests.log: ../test.pl
10-
@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
19+
@if ! ../test.pl -c $(exe) ; then \
1120
../failed-tests-printer.pl ; \
1221
exit 1 ; \
1322
fi

‎regression/goto-analyzer/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"goto-analyzer"
3+
"$<TARGET_FILE:goto-analyzer>"
4+
)

‎regression/goto-diff/CMakeLists.txt

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
add_test_pl_tests(
2+
"goto-diff"
3+
"$<TARGET_FILE:goto-diff>"
4+
)

‎regression/goto-instrument-typedef/CMakeLists.txt

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
add_test_pl_tests(
8+
"goto-instrument-typedef"
9+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
10+
)

‎regression/goto-instrument-typedef/Makefile

+13-3
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,24 @@
1-
21
default: tests.log
32

3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows="true"
9+
else
10+
exe=../../../src/goto-cc/goto-cc
11+
is_windows="false"
12+
endif
13+
414
test:
5-
@if ! ../test.pl -c ../chain.sh ; then \
15+
@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
616
../failed-tests-printer.pl ; \
717
exit 1; \
818
fi
919

1020
tests.log:
11-
@if ! ../test.pl -c ../chain.sh ; then \
21+
@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
1222
../failed-tests-printer.pl ; \
1323
exit 1; \
1424
fi

‎regression/goto-instrument-typedef/chain.sh

+16-9
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,21 @@
11
#!/bin/bash
22

3-
SRC=../../../src
3+
GC=$1
4+
GI=$2
5+
is_windows=$3
46

5-
GC=$SRC/goto-cc/goto-cc
6-
GI=$SRC/goto-instrument/goto-instrument
7+
name=${*:$#}
8+
name=${name%.c}
79

8-
OPTS=$1
9-
NAME=${2%.c}
10+
args=${*:4:$#-4}
1011

11-
rm $NAME.gb
12-
$GC $NAME.c --function fun -o $NAME.gb
13-
echo $GI $OPTS $NAME.gb
14-
$GI $OPTS $NAME.gb
12+
rm "${name}.gb"
13+
if [[ "${is_windows}" == "true" ]]; then
14+
"$GC" "${name}.c" --function fun
15+
mv "${name}.exe" "${name}.gb"
16+
else
17+
"$GC" "${name}.c" --function fun -o "${name}.gb"
18+
fi
19+
20+
echo "$GI" ${args} "${name}.gb"
21+
"$GI" ${args} "${name}.gb"

‎regression/goto-instrument/CMakeLists.txt

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
add_test_pl_tests(
8+
"goto-instrument"
9+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
10+
)

‎regression/goto-instrument/Makefile

+13-3
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,24 @@
1-
21
default: tests.log
32

3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows="true"
9+
else
10+
exe=../../../src/goto-cc/goto-cc
11+
is_windows="false"
12+
endif
13+
414
test:
5-
@if ! ../test.pl -c ../chain.sh ; then \
15+
@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
616
../failed-tests-printer.pl ; \
717
exit 1; \
818
fi
919

1020
tests.log:
11-
@if ! ../test.pl -c ../chain.sh ; then \
21+
@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
1222
../failed-tests-printer.pl ; \
1323
exit 1; \
1424
fi

0 commit comments

Comments
 (0)