test/regression/2007-08-16-valid-write-to-freed-object.c


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

// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc

unsigned sym() {
  unsigned x;
  klee_make_symbolic(&x, sizeof x);
  return x;
}

int main() {
  unsigned x, y;

  // sym returns a symbolic object, but because it is
  // alloca'd it is freed on sym()s return. thats fine,
  // but the problem is that IVC is going to try to write
  // into the object right here.
  //
  // to support this we need to have a facility for making
  // state local copies of a freed object.
  if (sym() == 0) 
    printf("ok\n");

  return 0;
}