Add CMakeLists alongside existing makefiles

.travis.yml

@@ -151,6 +151,34 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-5
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+        - CCACHE_CPP2=yes
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+
   allow_failures:
     - <<: *linter-stage
 

CMakeLists.txt

@@ -0,0 +1,40 @@
+cmake_minimum_required(VERSION 3.2)
+
+find_program(CCACHE_PROGRAM ccache)
+if(CCACHE_PROGRAM)
+    set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+ endif()
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+
+include(GNUInstallDirs)
+
+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)
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+)
+    #   Ensure NDEBUG is not set for release builds
+    set(CMAKE_CXX_FLAGS_RELEASE "-O2")
+    #   Enable lots of warnings
+    set(CMAKE_CXX_FLAGS "-Wall -Wpedantic -Werror")
+elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    #   This would be the place to enable warnings for Windows builds, although
+    #   config.inc doesn't seem to do that currently
+endif()
+
+set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+
+set(sat_impl "minisat2" CACHE STRING
+    "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
+)
+
+add_subdirectory(src)
+
+if(${enable_cbmc_tests})
+    enable_testing()
+endif()
+add_subdirectory(unit)
+add_subdirectory(regression)

COMPILING

@@ -171,7 +171,7 @@ Follow these instructions:
    BUILD_ENV = MSVC
 
    Open the Visual Studio Command prompt, and then bash.exe -login from
-   Cygwin from in there. 
+   Cygwin from in there.
 
 3) Type cd src; make - that should do it.
 
@@ -183,6 +183,53 @@ can be used for building with MSBuild.  Note that you still need to run
 flex/bison using "make generated_files" before opening the project.
 
 
+WORKING WITH CMAKE (EXPERIMENTAL)
+---------------------------------
+
+There is an experimental build based on CMake instead of hand-written
+makefiles. It should work on a wider variety of systems than the standard
+makefile build, and can integrate better with IDEs and static-analysis tools.
+
+0) Run `cmake --version`. If you get a command-not-found error, or the installed
+   version is lower than 3.2, go and install a new version. Most Linux
+   distributions have a package for CMake, and Mac users can get it through
+   Homebrew.  Windows users should download it manually from cmake.org.
+
+1) Create a directory to store your build:
+   `mkdir build`
+   Run this from the *top level* folder of the project. This is different from
+   the other builds, which require you to `cd src` first.
+
+2) Generate build files with CMake:
+   `cmake -H. -Bbuild`
+   This command tells CMake to use the configuration in the current directory,
+   and to generate build files into the `build` directory.
+   This is the point to specify custom build settings, such as compilers and
+   build back-ends. You can use clang (for example) by adding the argument
+   `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
+   CMake to generate IDE projects by supplying the `-G` flag.
+   Run `cmake -G` for a comprehensive list of supported back-ends.
+
+   Generally it is not necessary to manually specify individual compiler or
+   linker flags, as CMake defines a number of "build modes" including Debug
+   and Release modes. To build in a particular mode, add the flag
+   `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation.
+
+   If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
+   `-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
+   sanitizers.
+
+   Finally, to enable building universal binaries on macOS, you can pass the
+   flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
+   the build will just be for the architecture of your machine.
+
+3) Run the build:
+   `cmake --build build`
+   This command tells CMake to invoke the correct tool to run the build in the
+   `build` directory. You can also use the build back-end directly by invoking
+   `make`, `ninja`, or opening the generated IDE project as appropriate.
+
+
 WORKING WITH ECLIPSE
 --------------------
 

appveyor.yml

@@ -60,19 +60,6 @@ build_script:
 test_script:
 - cmd: |
     cd regression
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" ansi-c/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" cpp/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument/chain.sh
-    sed -i "15s/.*/$goto_cc $name.c/" goto-instrument/chain.sh
-    sed -i "16i mv $name.exe $name.gb" goto-instrument/chain.sh
-    sed -i "23s/.*/  $goto_cc ${name}-mod.c/" goto-instrument/chain.sh
-    sed -i "24i   mv ${name}-mod.exe $name-mod.gb" goto-instrument/chain.sh
-    cat goto-instrument/chain.sh
-
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument-typedef/chain.sh || true
-    sed -i "12s/.*/$GC $NAME.c --function fun/" goto-instrument-typedef/chain.sh || true
-    sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
-    cat goto-instrument-typedef/chain.sh || true
 
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad

regression/CMakeLists.txt

@@ -0,0 +1,36 @@
+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)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -c ${cmdline} ${flag}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile}"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests name cmdline)
+    add_test_pl_profile("${name}" "${cmdline}" -C CORE)
+    add_test_pl_profile("${name}" "${cmdline}" -T THOROUGH)
+    add_test_pl_profile("${name}" "${cmdline}" -F FUTURE)
+    add_test_pl_profile("${name}" "${cmdline}" -K KNOWNBUG)
+endmacro(add_test_pl_tests)
+
+add_subdirectory(ansi-c)
+add_subdirectory(cbmc)
+add_subdirectory(cbmc-java)
+add_subdirectory(cbmc-java-inheritance)
+add_subdirectory(cpp)
+add_subdirectory(goto-analyzer)
+add_subdirectory(goto-diff)
+add_subdirectory(goto-instrument)
+add_subdirectory(goto-instrument-typedef)
+add_subdirectory(invariants)
+add_subdirectory(strings)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(test-script)

regression/ansi-c/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "ansi-c"
+    "$<TARGET_FILE:goto-cc>"
+)

regression/ansi-c/Makefile

@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi

regression/cbmc-java-inheritance/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc-java-inheritance"
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-java/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc-java"
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc"
+    "$<TARGET_FILE:cbmc>"
+)

regression/cpp/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cpp"
+    "$<TARGET_FILE:goto-cc>"
+)

regression/cpp/Makefile

@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi

regression/goto-analyzer/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "goto-analyzer"
+    "$<TARGET_FILE:goto-analyzer>"
+)

regression/goto-diff/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "goto-diff"
+    "$<TARGET_FILE:goto-diff>"
+)

regression/goto-instrument-typedef/CMakeLists.txt

@@ -0,0 +1,10 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "goto-instrument-typedef"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)

regression/goto-instrument-typedef/Makefile

@@ -1,14 +1,24 @@
-
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows="true"
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows="false"
+endif
+
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
 
 tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi

regression/goto-instrument-typedef/chain.sh

@@ -1,14 +1,21 @@
 #!/bin/bash
 
-SRC=../../../src
+GC=$1
+GI=$2
+is_windows=$3
 
-GC=$SRC/goto-cc/goto-cc
-GI=$SRC/goto-instrument/goto-instrument
+name=${*:$#}
+name=${name%.c}
 
-OPTS=$1
-NAME=${2%.c}
+args=${*:4:$#-4}
 
-rm $NAME.gb
-$GC $NAME.c --function fun -o $NAME.gb
-echo $GI $OPTS $NAME.gb
-$GI $OPTS $NAME.gb
+rm "${name}.gb"
+if [[ "${is_windows}" == "true" ]]; then
+  "$GC" "${name}.c" --function fun
+  mv "${name}.exe" "${name}.gb"
+else
+  "$GC" "${name}.c" --function fun -o "${name}.gb"
+fi
+
+echo "$GI" ${args} "${name}.gb"
+"$GI" ${args} "${name}.gb"

regression/goto-instrument/CMakeLists.txt

@@ -0,0 +1,10 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "goto-instrument"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/goto-instrument/Makefile

@@ -1,14 +1,24 @@
-
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows="true"
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows="false"
+endif
+
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
 
 tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi