From 95f7f447432807efd70c8abac598d0d88ba1e9b1 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Wed, 24 Feb 2021 20:19:48 +0000 Subject: test: count paths with -dump-states-on-halt=false --- test/regression/2020-02-24-count-paths-nodump.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 test/regression/2020-02-24-count-paths-nodump.c (limited to 'test') 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 -- cgit 1.4.1