diff options
| author | Frank Busse <bb0xfb@gmail.com> | 2021-02-24 20:19:48 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2021-05-04 14:58:19 +0100 |
| commit | 95f7f447432807efd70c8abac598d0d88ba1e9b1 (patch) | |
| tree | e0aa368b069db5cbb6be99b6474db00f03cc1ca3 /test/regression | |
| parent | 43321064287cca6af7c15f173bbcefc351960cc0 (diff) | |
| download | klee-95f7f447432807efd70c8abac598d0d88ba1e9b1.tar.gz | |
test: count paths with -dump-states-on-halt=false
Diffstat (limited to 'test/regression')
| -rw-r--r-- | test/regression/2020-02-24-count-paths-nodump.c | 14 |
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 |