test/regression/2007-10-12-failed-make-symbolic-after-copy.c


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %klee %t1.bc
// RUN: test -f %T/klee-last/test000001.ktest

int main() {
  unsigned x, y[4];

  klee_make_symbolic(&x, sizeof x, "x");
  if (x>=4) klee_silent_exit(0);
  
  y[x] = 0;

  if (x) { // force branch so y is copied
    klee_make_symbolic(&y, sizeof y, "y");
    if (y[x]==0) klee_silent_exit(0);
    return 0; // should be reachable
  } else {
    // force read here in case we try to optimize copies smartly later
    if (y[x]==0) klee_silent_exit(0);
    return 0; // not reachable
  }
}