about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2020-09-03 20:06:31 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-10-06 15:22:51 +0100
commit69d9d269c770404a9ab2cb7965efd87b273a75e5 (patch)
tree95a150cd58737a4e95462eb018a35642399e02a0 /test
parentf83eac1f001e11c3464fcf088eb4e433abad04a9 (diff)
downloadklee-69d9d269c770404a9ab2cb7965efd87b273a75e5.tar.gz
Added support for klee_open_merge and klee_close_merge in replay, together with a test case.
Diffstat (limited to 'test')
-rw-r--r--test/Replay/libkleeruntest/replay_merge.c49
1 files changed, 49 insertions, 0 deletions
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;
+}