about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2015-10-21 16:18:17 +0100
committerDan Liew <daniel.liew@imperial.ac.uk>2015-10-21 16:19:53 +0100
commit40d9c1d6296211f8127b34036509b225b491d4b8 (patch)
treef6fb976f9dcd20a526f2d961bc37427724f8ed71
parent65ba2c937a8534a43b27a0c0bb7e22849d6aae02 (diff)
downloadklee-40d9c1d6296211f8127b34036509b225b491d4b8.tar.gz
Change implementation of __VERIFIER_assume() so that if it's isn't svcomp
satisfiable KLEE doesn't exit with an error.
-rw-r--r--runtime/svcomp64/functions.c9
1 files changed, 8 insertions, 1 deletions
diff --git a/runtime/svcomp64/functions.c b/runtime/svcomp64/functions.c
index 0fdae3bd..f8957e66 100644
--- a/runtime/svcomp64/functions.c
+++ b/runtime/svcomp64/functions.c
@@ -52,7 +52,14 @@ float __VERIFIER_nondet_float() {
 }
 
 void __VERIFIER_assume(int condition) {
-  klee_assume(condition);
+  // Guard the condition we assume so that if it is not
+  // satisfiable we don't flag up an error. Instead we'll
+  // just silently terminate this state.
+  if (condition) {
+    klee_assume(condition);
+  } else {
+    klee_silent_exit(0);
+  }
 }
 
 void __VERIFIER_assert(int cond) {