test/regression/2007-10-11-illegal-access-after-free-and-branch.c


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

// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
// RUN: %klee --optimize %t1.bc
// RUN: test -f klee-last/test000001.ptr.err

#include <stdlib.h>
#include <stdio.h>
#include <assert.h>

int main(int argc, char **argv) {
  unsigned char *buf = malloc(3);
  klee_make_symbolic(buf, 3);
  if (buf[0]>4) klee_silent_exit(0);
  unsigned char x = buf[1];
  free(buf);
  if (x)
    return buf[2];
  klee_silent_exit(0);
  return 0;
}