about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/CMakeLists.txt2
-rw-r--r--test/Feature/Alias.c9
-rw-r--r--test/Feature/LargeReturnTypes.cpp3
-rw-r--r--test/Runtime/POSIX/FD_Fail.c2
-rw-r--r--test/lit.cfg8
-rw-r--r--test/regression/2016-11-24-bitcast-weak-alias.c1
-rw-r--r--test/regression/2017-03-23-early-exit-log-stats.c22
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])}}