diff options
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 15 | ||||
| -rw-r--r-- | test/Feature/SilentKleeAssume.c | 30 |
2 files changed, 42 insertions, 3 deletions
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 52abff5f..8befe8f6 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -42,6 +42,11 @@ namespace { cl::init(false), cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. " "Note: option is expensive when creating lots of tests (default=false)")); + + cl::opt<bool> + SilentKleeAssume("silent-klee-assume", + cl::init(false), + cl::desc("Do not treat infeasible assumption as error.")); } @@ -391,9 +396,13 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { - executor.terminateStateOnError(state, - "invalid klee_assume call (provably false)", - "user.err"); + if (SilentKleeAssume) { + executor.terminateState(state); + } else { + executor.terminateStateOnError(state, + "invalid klee_assume call (provably false)", + "user.err"); + } } else { executor.addConstraint(state, e); } 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 |