From ee5a905cda1af731c3994e63f140c654c5dc7c2c Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Fri, 4 Dec 2015 18:55:24 -0600
Subject: Add command line flag ``--silent-klee-assume``to suppress errors due
 to infeasible assumptions.

---
 lib/Core/SpecialFunctionHandler.cpp | 15 ++++++++++++---
 test/Feature/SilentKleeAssume.c     | 30 ++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 3 deletions(-)
 create mode 100644 test/Feature/SilentKleeAssume.c

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
-- 
cgit 1.4.1