about summary refs log tree commit diff homepage
path: root/test/Feature/CopyOnWrite.c
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature/CopyOnWrite.c')
-rw-r--r--test/Feature/CopyOnWrite.c26
1 files changed, 26 insertions, 0 deletions
diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c
new file mode 100644
index 00000000..ee3ea15e
--- /dev/null
+++ b/test/Feature/CopyOnWrite.c
@@ -0,0 +1,26 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --use-random-search --exit-on-error %t1.bc
+
+#include <assert.h>
+
+#define N 5
+
+unsigned branches = 0;
+
+void explode(int *ap, int i, int *result) {
+  if (i<N) {
+    (*result)++;
+    if (ap[i]) // just cause a fork
+      branches++; 
+    return explode(ap, i+1, result);
+  }
+}
+
+int main() {
+  int result = 0;
+  int a[N];
+  klee_make_symbolic(a, sizeof a);
+  explode(a,0,&result);
+  assert(result==N);
+  return 0;
+}