// RUN: %clang -emit-llvm -c -g %s -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t.bc "initial" // RUN: test -f %t.klee-out/test000001.ktest // RUN: not test -f %t.klee-out/test000002.ktest // RUN: rm -rf %t.klee-out-2 // RUN: %klee --output-dir=%t.klee-out-2 --only-replay-seeds --named-seed-matching --seed-file %t.klee-out/test000001.ktest %t.bc > %t.log // RUN: grep -q "a==3" %t.log // RUN: grep -q "b==4" %t.log // RUN: grep -q "c==5" %t.log // RUN: grep -q "x==6" %t.log #include "klee/klee.h" #include #include int main(int argc, char **argv) { int a, b, c, x; if (argc==2 && strcmp(argv[1], "initial") == 0) { klee_make_symbolic(&a, sizeof a, "a"); klee_make_symbolic(&b, sizeof b, "b"); klee_make_symbolic(&c, sizeof c, "c"); klee_make_symbolic(&x, sizeof x, "a"); klee_assume(a == 3); klee_assume(b == 4); klee_assume(c == 5); klee_assume(x == 6); } else { klee_make_symbolic(&a, sizeof a, "a"); klee_make_symbolic(&c, sizeof c, "c"); klee_make_symbolic(&b, sizeof b, "b"); klee_make_symbolic(&x, sizeof x, "a"); } if (a==3) printf("a==3\n"); if (b==4) printf("b==4\n"); if (c==5) printf("c==5\n"); if (x==6) printf("x==6\n"); return 0; }