diff options
| author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-04 18:55:24 -0600 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-11 14:20:06 +0000 |
| commit | ee5a905cda1af731c3994e63f140c654c5dc7c2c (patch) | |
| tree | 4dfb45d70502dda9d0ffacc0613f0d494708108a /test | |
| parent | 1d099af31d3415c89dfbb56c8fdc1a3bcf1309c7 (diff) | |
| download | klee-ee5a905cda1af731c3994e63f140c654c5dc7c2c.tar.gz | |
Add command line flag ``--silent-klee-assume``to suppress errors due to
infeasible assumptions.
Diffstat (limited to 'test')
| -rw-r--r-- | test/Feature/SilentKleeAssume.c | 30 |
1 files changed, 30 insertions, 0 deletions
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 <stdio.h> +#include <assert.h> + +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 |