diff options
Diffstat (limited to 'test/regression/2008-03-11-free-of-malloc-zero.c')
-rw-r--r-- | test/regression/2008-03-11-free-of-malloc-zero.c | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regression/2008-03-11-free-of-malloc-zero.c b/test/regression/2008-03-11-free-of-malloc-zero.c new file mode 100644 index 00000000..d096818b --- /dev/null +++ b/test/regression/2008-03-11-free-of-malloc-zero.c @@ -0,0 +1,16 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +#include <stdlib.h> + +int main() { + // concrete case + void *p = malloc(0); + free(p); + + p = malloc(0); + void *arr[4] = { p, 0, 0, 0 }; + + // symbolic case + free(arr[klee_range(0, 4, "range")]); +} |