about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2021-02-24 20:19:48 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2021-05-04 14:58:19 +0100
commit95f7f447432807efd70c8abac598d0d88ba1e9b1 (patch)
treee0aa368b069db5cbb6be99b6474db00f03cc1ca3 /test
parent43321064287cca6af7c15f173bbcefc351960cc0 (diff)
downloadklee-95f7f447432807efd70c8abac598d0d88ba1e9b1.tar.gz
test: count paths with -dump-states-on-halt=false
Diffstat (limited to 'test')
-rw-r--r--test/regression/2020-02-24-count-paths-nodump.c14
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regression/2020-02-24-count-paths-nodump.c b/test/regression/2020-02-24-count-paths-nodump.c
new file mode 100644
index 00000000..c066886c
--- /dev/null
+++ b/test/regression/2020-02-24-count-paths-nodump.c
@@ -0,0 +1,14 @@
+// ASAN fails because KLEE does not cleanup states with -dump-states-on-halt=false
+// REQUIRES: not-asan
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -dump-states-on-halt=false -max-instructions=1 -output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+
+int main(int argc, char **argv) {
+  // just do something
+  int i = 42;
+  ++i;
+}
+
+// CHECK: KLEE: done: completed paths = 0
+// CHECK: KLEE: done: partially completed paths = 1
\ No newline at end of file