about summary refs log tree commit diff homepage
path: root/test/Feature/SetForking.c
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature/SetForking.c')
-rw-r--r--test/Feature/SetForking.c28
1 files changed, 28 insertions, 0 deletions
diff --git a/test/Feature/SetForking.c b/test/Feature/SetForking.c
new file mode 100644
index 00000000..8620110d
--- /dev/null
+++ b/test/Feature/SetForking.c
@@ -0,0 +1,28 @@
+// RUN: %llvmgcc -g -c %s -o %t.bc
+// RUN: %klee %t.bc > %t.log
+// RUN: sort %t.log | uniq -c > %t.uniq.log
+// RUN: grep "1 A" %t.uniq.log
+// RUN: grep "1 B" %t.uniq.log
+// RUN: grep "1 C" %t.uniq.log
+
+#include <stdio.h>
+
+int main() {
+  klee_set_forking(0);
+  
+  if (klee_range(0, 2, "range")) {
+    printf("A\n");
+  } else {
+    printf("A\n");
+  }
+
+  klee_set_forking(1);
+
+  if (klee_range(0, 2, "range")) {
+    printf("B\n");
+  } else {
+    printf("C\n");
+  }
+
+  return 0;
+}