diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-14 17:55:07 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-14 21:37:19 +0000 |
| commit | 3c8cb4600392675a34f2505f630523a494844d3d (patch) | |
| tree | bbe0cf8b9d2e369175ad03020d7bdb47e9e11aa9 /test/CMakeLists.txt | |
| parent | 23e656156e4790a06a295d48932db53f2a582227 (diff) | |
| download | klee-3c8cb4600392675a34f2505f630523a494844d3d.tar.gz | |
Write tests to test `libkleeRuntest`. The `replay_posix_runtime.c`
test is marked XFAIL because there is a bug in the implementation of `libkleeRuntest`. Quite a few changes had to be made to the lit configuration in order to support these tests. To run the tests I had to fix #480 for the autoconf/Makefile build system otherwise the `libkleeRuntest` library would not be found by the system linker at runtime.
Diffstat (limited to 'test/CMakeLists.txt')
| -rw-r--r-- | test/CMakeLists.txt | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 6d3ec926..0ae78faf 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -13,6 +13,8 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") # is shared by both build systems. set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") +set(NATIVE_CC "${CMAKE_C_COMPILER} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_CXX "${CMAKE_CXX_COMPILER} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") if (ENABLE_KLEE_UCLIBC) set(ENABLE_UCLIBC 1) @@ -105,6 +107,20 @@ add_subdirectory(Concrete) ############################################################################### # Configure lit test suite ############################################################################### + +# Find path to libkleeRuntest target for `lit.site.cfg`. +# FIXME: This is not the right way to get the location of the target we have to +# set CMP0026 to old. +# This will likely break if using a multi-configuration generator. +if (POLICY CMP0026) + # HACK: Allow reading `LOCATION` property. + cmake_policy(SET CMP0026 OLD) +endif() +get_property(LIB_KLEE_RUN_TEST_PATH + TARGET kleeRuntest + PROPERTY LOCATION +) + configure_file(lit.site.cfg.in ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg @ONLY @@ -112,7 +128,7 @@ configure_file(lit.site.cfg.in add_custom_target(integrationtests COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" - DEPENDS klee kleaver + DEPENDS klee kleaver kleeRuntest COMMENT "Running integration tests" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) |