about summary refs log tree commit diff homepage
path: root/test/regression
diff options
context:
space:
mode:
Diffstat (limited to 'test/regression')
-rw-r--r--test/regression/2016-11-24-bitcast-weak-alias.c1
-rw-r--r--test/regression/2017-02-21-pathOS-id.c19
-rw-r--r--test/regression/2017-03-23-early-exit-log-stats.c22
3 files changed, 42 insertions, 0 deletions
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-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c
new file mode 100644
index 00000000..d3bffbe0
--- /dev/null
+++ b/test/regression/2017-02-21-pathOS-id.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log
+// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1
+int main(){
+	int a, b;
+	klee_make_symbolic (&a, sizeof(int), "a");
+	klee_make_symbolic (&b, sizeof(int), "b");
+	klee_assume(a<2);
+	klee_assume(a>=0);
+	malloc(a);
+	if(b){
+		b++;//do something
+	}
+	return b;
+}
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])}}