From ee5a905cda1af731c3994e63f140c654c5dc7c2c Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 4 Dec 2015 18:55:24 -0600 Subject: Add command line flag ``--silent-klee-assume``to suppress errors due to infeasible assumptions. --- test/Feature/SilentKleeAssume.c | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test/Feature/SilentKleeAssume.c (limited to 'test') diff --git a/test/Feature/SilentKleeAssume.c b/test/Feature/SilentKleeAssume.c new file mode 100644 index 00000000..e444b6b9 --- /dev/null +++ b/test/Feature/SilentKleeAssume.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --silent-klee-assume %t.bc > %t.silent-klee-assume.log 2>&1 +// RUN: FileCheck -input-file=%t.silent-klee-assume.log -check-prefix=CHECK-SILENT-KLEE-ASSUME %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --silent-klee-assume=0 %t.bc > %t.default-klee-assume.log 2>&1 +// RUN: FileCheck -input-file=%t.default-klee-assume.log -check-prefix=CHECK-DEFAULT-KLEE-ASSUME %s + +#include +#include + +int main() { + int x = klee_int("x"); + int y = klee_int("y"); + klee_assume(x > 10); + if (y < 42) { + // CHECK-DEFAULT-KLEE-ASSUME: KLEE: ERROR: {{.*SilentKleeAssume.c:18}}: invalid klee_assume call (provably false) + klee_assume(x < 10); + // CHECK-DEFAULT-KLEE-ASSUME: KLEE: NOTE: now ignoring this error at this location + // CHECK-DEFAULT-KLEE-ASSUME: EXITING ON ERROR: + // CHECK-DEFAULT-KLEE-ASSUME: Error: invalid klee_assume call (provably false) + assert(0); + } + return 0; +} + +// CHECK-SILENT-KLEE-ASSUME: KLEE: output directory is "{{.+}}" +// CHECK-SILENT-KLEE-ASSUME: KLEE: done: total instructions = {{[0-9]+}} +// CHECK-SILENT-KLEE-ASSUME: KLEE: done: completed paths = 2 +// CHECK-SILENT-KLEE-ASSUME: KLEE: done: generated tests = 1 -- cgit 1.4.1