Enable running tests from CMake

CMakeLists.txt

@@ -1,10 +1,19 @@
 cmake_minimum_required(VERSION 3.2)
 
+set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+
 include(GNUInstallDirs)
 
-set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+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)
 
 add_subdirectory(src)
 
-enable_testing()
+set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+
+if(${enable_cbmc_tests})
+    enable_testing()
+endif()
 add_subdirectory(unit)
+add_subdirectory(regression)

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

regression/goto-instrument/chain.sh

@@ -2,26 +2,37 @@
 
 set -e
 
-src=../../../src
-goto_cc=$src/goto-cc/goto-cc
-goto_instrument=$src/goto-instrument/goto-instrument
-cbmc=$src/cbmc/cbmc
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
 
-name=${@:$#}
+name=${*:$#}
 name=${name%.c}
 
-args=${@:1:$#-1}
-
-$goto_cc -o $name.gb $name.c
-# $goto_instrument --show-goto-functions $name.gb
-$goto_instrument $args $name.gb ${name}-mod.gb
-if [ ! -e ${name}-mod.gb ] ; then
-  cp $name.gb ${name}-mod.gb
-elif echo "$args" | grep -q -- "--dump-c" ; then
-  mv ${name}-mod.gb ${name}-mod.c
-  $goto_cc ${name}-mod.c -o ${name}-mod.gb
-  rm ${name}-mod.c
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
 fi
-$goto_instrument --show-goto-functions ${name}-mod.gb
-$cbmc ${name}-mod.gb
 
+$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+if [ ! -e "${name}-mod.gb" ] ; then
+  cp "$name.gb" "${name}-mod.gb"
+elif echo $args | grep -q -- "--dump-c" ; then
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c"
+    mv "${name}-mod.exe" "${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$goto_instrument --show-goto-functions "${name}-mod.gb"
+$cbmc "${name}-mod.gb"

regression/invariants/CMakeLists.txt

@@ -0,0 +1,7 @@
+add_executable(driver driver.cpp)
+target_link_libraries(driver big-int util)
+
+add_test_pl_tests(
+    "invariants"
+    "$<TARGET_FILE:driver>"
+)

regression/strings-smoke-tests/CMakeLists.txt

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

regression/strings/CMakeLists.txt

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

regression/test-script/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "test-script"
+    "${CMAKE_CURRENT_SOURCE_DIR}/program_runner.sh" 
+)

src/ansi-c/CMakeLists.txt

@@ -20,6 +20,31 @@ function(make_inc name)
     )
 endfunction(make_inc)
 
+################################################################################
+
+if(MINGW)
+    set(platform_unavail
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/java.io.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/err.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/threads.c
+    )
+else()
+    set(platform_unavail
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/java.io.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/threads.c
+    )
+endif()
+
+file(GLOB library_check_sources "library/*.c")
+list(REMOVE_ITEM library_check_sources ${platform_unavail})
+
+add_custom_target(library_check
+    ${CMAKE_CURRENT_SOURCE_DIR}/check_library.sh ${library_check_sources}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
+################################################################################
+
 make_inc(arm_builtin_headers)
 make_inc(clang_builtin_headers)
 make_inc(cw_builtin_headers)

src/ansi-c/check_library.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+for var in "$@"; do
+    cp "${var}" __libcheck.c
+    sed -i 's/__builtin_[^v]/s&/' __libcheck.c
+    sed -i 's/__sync_/s&/' __libcheck.c
+    sed -i 's/__noop/s&/' __libcheck.c
+    cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+    cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label -Wno-uninitialized
+
+    ec="$?"
+    rm __libcheck.s __libcheck.i __libcheck.c
+    [ "${ec}" -eq 0 ] || exit "${ec}"
+done

src/goto-cc/CMakeLists.txt

@@ -35,3 +35,7 @@ add_if_library(goto-cc-lib jsil)
 # Executable
 add_executable(goto-cc goto_cc_main.cpp)
 target_link_libraries(goto-cc goto-cc-lib)
+
+if(WIN32)
+  set_target_properties(goto-cc PROPERTIES OUTPUT_NAME goto-cl)
+endif()