about summary refs log tree commit diff homepage
path: root/runtime/Runtest
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/Runtest')
-rw-r--r--runtime/Runtest/intrinsics.c6
1 files changed, 6 insertions, 0 deletions
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 4d785ee2..1e87d947 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -172,6 +172,12 @@ int klee_range(int begin, int end, const char* name) {
   return x;
 }
 
+void klee_prefer_cex(void *object, uintptr_t condition) { }
+
+void klee_abort() {
+  exit(1);
+}
+
 /* not sure we should even define.  is for debugging. */
 void klee_print_expr(const char *msg, ...) { }