Added support for klee_open_merge and klee_close_merge in replay, together with a test case.

2 files changed, 53 insertions, 0 deletions

diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index f82bd554..e9f66ed1 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -190,3 +190,7 @@ void klee_abort() {
 void klee_print_expr(const char *msg, ...) { }
 
 void klee_set_forking(unsigned enable) { }
+
+
+void klee_open_merge() { }
+void klee_close_merge() { }
diff --git a/test/Replay/libkleeruntest/replay_merge.c b/test/Replay/libkleeruntest/replay_merge.c
new file mode 100644
index 00000000..fae480a5
--- /dev/null
+++ b/test/Replay/libkleeruntest/replay_merge.c
@@ -0,0 +1,49 @@
+// RUN: %clang -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-merge  %t.bc 2>&1 | FileCheck %s
+
+// CHECK: generated tests = 2{{$}}
+
+// Now try to replay with libkleeRuntest
+// RUN: %cc %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner
+// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner > %t.txt
+// RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner >> %t.txt
+// RUN: FileCheck --check-prefix=REPLAY --input-file %t.txt %s
+
+// REPLAY-DAG: 0
+// REPLAY-DAG: 1
+
+
+#include "klee/klee.h"
+
+#include <stdio.h>
+
+int main(int argc, char** args){
+
+  int x;
+  int a;
+  int foo = 0;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  if (a == 0){
+    klee_open_merge();
+
+    if (x == 1) {
+      foo = 5;
+    } else if (x == 2) {
+      foo = 6;
+    } else {
+      foo = 7;
+    }
+
+    klee_close_merge();
+  }
+
+  if (foo > 0)
+    foo = 1;
+  printf("foo = %d\n", foo);
+  
+  return 0;
+}