replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Enable running tests from CMake

This commit is contained in:
reuk 2017-08-30 17:17:38 +01:00
parent e609bbb51a
commit f6e49683c9
25 changed files with 263 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
CMakeLists.txt
View File

@ -1,10 +1,19 @@
cmake_minimum_required(VERSION 3.2)
include(GNUInstallDirs)
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)
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)

36
regression/CMakeLists.txt Normal file
View File

@ -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)

4
regression/ansi-c/CMakeLists.txt Normal file
View File

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

13
regression/ansi-c/Makefile
View File

@ -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

4
regression/cbmc-java-inheritance/CMakeLists.txt Normal file
View File

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

4
regression/cbmc-java/CMakeLists.txt Normal file
View File

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

4
regression/cbmc/CMakeLists.txt Normal file
View File

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

4
regression/cpp/CMakeLists.txt Normal file
View File

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

13
regression/cpp/Makefile
View File

@ -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

4
regression/goto-analyzer/CMakeLists.txt Normal file
View File

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

4
regression/goto-diff/CMakeLists.txt Normal file
View File

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

10
regression/goto-instrument-typedef/CMakeLists.txt Normal file
View File

@ -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}"
)

16
regression/goto-instrument-typedef/Makefile
View File

@ -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

25
regression/goto-instrument-typedef/chain.sh
View File

@ -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"

10
regression/goto-instrument/CMakeLists.txt Normal file
View File

@ -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}"
)

16
regression/goto-instrument/Makefile
View File

@ -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

45
regression/goto-instrument/chain.sh
View File

@ -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}
args=${*:5:$#-5}
$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
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"

7
regression/invariants/CMakeLists.txt Normal file
View File

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

4
regression/strings-smoke-tests/CMakeLists.txt Normal file
View File

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

4
regression/strings/CMakeLists.txt Normal file
View File

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

4
regression/test-script/CMakeLists.txt Normal file
View File

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

25
src/ansi-c/CMakeLists.txt
View File

@ -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)

14
src/ansi-c/check_library.sh Executable file
View File

@ -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

4
src/goto-cc/CMakeLists.txt
View File

@ -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()

19
unit/CMakeLists.txt
View File

@ -31,7 +31,12 @@ target_include_directories(unit
${CMAKE_CURRENT_SOURCE_DIR}
)
target_link_libraries(unit ansi-c solvers java_bytecode)
add_test(NAME unit COMMAND unit WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
add_test(
NAME unit
COMMAND $<TARGET_FILE:unit>
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
)
set_tests_properties(unit PROPERTIES LABELS CORE)
add_executable(miniBDD miniBDD.cpp)
target_include_directories(miniBDD
@ -41,7 +46,8 @@ target_include_directories(miniBDD
${CMAKE_CURRENT_SOURCE_DIR}
)
target_link_libraries(miniBDD solvers ansi-c)
add_test(miniBDD miniBDD)
add_test(NAME miniBDD COMMAND $<TARGET_FILE:miniBDD>)
set_tests_properties(miniBDD PROPERTIES LABELS CORE)
add_executable(string_utils string_utils.cpp)
target_include_directories(string_utils
@ -51,7 +57,8 @@ target_include_directories(string_utils
${CMAKE_CURRENT_SOURCE_DIR}
)
target_link_libraries(string_utils solvers ansi-c)
add_test(string_utils string_utils)
add_test(NAME string_utils COMMAND $<TARGET_FILE:string_utils>)
set_tests_properties(string_utils PROPERTIES LABELS CORE)
add_executable(sharing_node sharing_node.cpp)
target_include_directories(sharing_node
@ -60,6 +67,6 @@ target_include_directories(sharing_node
${CBMC_SOURCE_DIR}
${CMAKE_CURRENT_SOURCE_DIR}
)
add_test(sharing_node sharing_node)
install(TARGETS unit miniBDD string_utils sharing_node DESTINATION bin)
target_link_libraries(sharing_node util)
add_test(NAME sharing_node COMMAND $<TARGET_FILE:sharing_node>)
set_tests_properties(sharing_node PROPERTIES LABELS CORE)