diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/Feature/Alias.c | 9 | ||||
| -rw-r--r-- | test/Feature/LargeReturnTypes.cpp | 3 | ||||
| -rw-r--r-- | test/Runtime/POSIX/FD_Fail.c | 2 | ||||
| -rw-r--r-- | test/lit.cfg | 8 | ||||
| -rw-r--r-- | test/regression/2016-11-24-bitcast-weak-alias.c | 1 | ||||
| -rw-r--r-- | test/regression/2017-03-23-early-exit-log-stats.c | 22 |
7 files changed, 38 insertions, 9 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index a2a46e2a..4b6a63f6 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -96,7 +96,7 @@ if (DOWNLOAD_NOT_SOURCE) target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) - target_link_libraries("not" PRIVATE ${FILECHECK_NEEDED_LIBS}) + target_link_libraries("not" PRIVATE ${NOT_NEEDED_LIBS}) endif() ############################################################################### diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c index 381bcc2a..09abb3e0 100644 --- a/test/Feature/Alias.c +++ b/test/Feature/Alias.c @@ -1,10 +1,9 @@ +// Darwin does not have strong aliases. +// REQUIRES: not-darwin // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -// Darwin does not have strong aliases. -// XFAIL: darwin - #include <assert.h> // alias for global @@ -17,10 +16,10 @@ extern int foo() __attribute__((alias("__foo"))); int *c = &a; -int main() { +int main() { assert(a == 52); assert(foo() == 52); assert(*c == 52); - + return 0; } diff --git a/test/Feature/LargeReturnTypes.cpp b/test/Feature/LargeReturnTypes.cpp index 937b0758..84119624 100644 --- a/test/Feature/LargeReturnTypes.cpp +++ b/test/Feature/LargeReturnTypes.cpp @@ -1,3 +1,4 @@ +// REQUIRES: not-darwin // RUN: %llvmgxx -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log @@ -9,8 +10,6 @@ // This test currently doesn't work on darwin because this isn't how things work // in libc++. This test should be rewritten to not depend on an external // dependency. -// -// XFAIL: darwin #include <fstream> diff --git a/test/Runtime/POSIX/FD_Fail.c b/test/Runtime/POSIX/FD_Fail.c index 186ada51..2ee1a1a2 100644 --- a/test/Runtime/POSIX/FD_Fail.c +++ b/test/Runtime/POSIX/FD_Fail.c @@ -11,7 +11,7 @@ int main(int argc, char** argv) { char buf[1024]; - FILE* f = fopen("/etc/fstab", "r"); + FILE* f = fopen("/etc/mtab", "r"); assert(f); int r = fread(buf, 1, 100, f); diff --git a/test/lit.cfg b/test/lit.cfg index 31552882..dd2fbc13 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -151,3 +151,11 @@ else: # POSIX runtime feature if config.enable_posix_runtime: config.available_features.add('posix-runtime') + +# Target operating system features +supported_targets = ['linux', 'darwin'] +for target in supported_targets: + if config.target_triple.find(target) != -1: + config.available_features.add(target) + else: + config.available_features.add('not-{}'.format(target)) diff --git a/test/regression/2016-11-24-bitcast-weak-alias.c b/test/regression/2016-11-24-bitcast-weak-alias.c index f115731b..3e4ebe64 100644 --- a/test/regression/2016-11-24-bitcast-weak-alias.c +++ b/test/regression/2016-11-24-bitcast-weak-alias.c @@ -1,3 +1,4 @@ +// REQUIRES: not-darwin // RUN: %llvmgcc %s -Wall -emit-llvm -g -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: klee --output-dir=%t.klee-out -exit-on-error -search=nurs:covnew %t.bc DUMMY_ARG >%t1.log 2>&1 diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c new file mode 100644 index 00000000..96d3c30f --- /dev/null +++ b/test/regression/2017-03-23-early-exit-log-stats.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// Delay writing instructions so that we ensure on exit that flush happens +// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 %t.bc 2> %t.log +// RUN: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s +#include "klee/klee.h" +#include <stdlib.h> +int main(){ + int a; + klee_make_symbolic (&a, sizeof(int), "a"); + if (a) { + // CHECK-KLEE: EXITING ON ERROR + // CHECK-KLEE-NEXT: Error: abort failure + abort(); + } + return 0; +} +// First check we find a line with the expected format +// CHECK-STATS:{{^\('Instructions'}} +// Now check that we eventually get a line where a non zero amount of instructions were executed +// CHECK-STATS:{{^\([ ]*([1-9]|([1-9]+)[0-9])}} |
