diff options
Diffstat (limited to 'test/Feature/MultipleFreeResolution.c')
| -rw-r--r-- | test/Feature/MultipleFreeResolution.c | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c index aa931c13..f30eabed 100644 --- a/test/Feature/MultipleFreeResolution.c +++ b/test/Feature/MultipleFreeResolution.c @@ -1,9 +1,11 @@ // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --kdalloc --emit-all-errors %t1.bc 2>&1 | FileCheck %s // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4 // RUN: ls %t.klee-out/ | grep .err | wc -l | grep 3 +#include "klee/klee.h" + #include <stdio.h> #include <stdlib.h> @@ -34,9 +36,9 @@ int main() { free(buf[s]); for (i = 0; i < 3; i++) { - // CHECK: MultipleFreeResolution.c:[[@LINE+3]]: memory error: out of bound pointer - // CHECK: MultipleFreeResolution.c:[[@LINE+2]]: memory error: out of bound pointer - // CHECK: MultipleFreeResolution.c:[[@LINE+1]]: memory error: out of bound pointer + // CHECK: MultipleFreeResolution.c:[[@LINE+3]]: memory error: use after free + // CHECK: MultipleFreeResolution.c:[[@LINE+2]]: memory error: use after free + // CHECK: MultipleFreeResolution.c:[[@LINE+1]]: memory error: use after free printf("*buf[%d] = %d\n", i, *buf[i]); } |