about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2012-11-28 18:06:35 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2012-11-28 18:06:35 +0000
commit6d9be03c5f322207637c88eac881563c1f8420ac (patch)
tree6204dbbce8df099b09a5febdbc33316bbec948f2
parent4dc7dfdb7b65a9ef5db4cf7c911327a87323c5a1 (diff)
downloadklee-6d9be03c5f322207637c88eac881563c1f8420ac.tar.gz
Fixed fragile test case that depended too much on the code generated
by the compiler (this was failing with clang/llvm 3.1).


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168795 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--test/Feature/ReplayPath.c25
1 files changed, 15 insertions, 10 deletions
diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c
index 3f01fa80..f88ad6dc 100644
--- a/test/Feature/ReplayPath.c
+++ b/test/Feature/ReplayPath.c
@@ -1,22 +1,27 @@
-// RUN: echo "1" > %t1.path
-// RUN: echo "0" >> %t1.path
-// RUN: echo "1" >> %t1.path
-// RUN: echo "0" >> %t1.path
-// RUN: echo "1" >> %t1.path
+// RUN: %llvmgcc %s -emit-llvm -O0 -DCOND_EXIT -c -o %t1.bc
+// RUN: klee --write-paths %t1.bc > %t3.good
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --replay-path %t1.path %t2.bc > %t3.log
-// RUN: echo "res: 110" > %t3.good
+// RUN: %klee --replay-path klee-last/test000001.path %t2.bc >%t3.log
 // RUN: diff %t3.log %t3.good
 
+#include <unistd.h>
+#include <stdio.h>
+
+void cond_exit() {
+#ifdef COND_EXIT
+  klee_silent_exit(0);
+#endif
+}
+
 int main() {
   int res = 1;
   int x;
 
   klee_make_symbolic(&x, sizeof x);
 
-  if (x&1) res *= 2;
-  if (x&2) res *= 3;
-  if (x&4) res *= 5;
+  if (x&1) res *= 2; else cond_exit();
+  if (x&2) res *= 3; else cond_exit();
+  if (x&4) res *= 5; else cond_exit();
 
   // get forced branch coverage
   if (x&2) res *= 7;