From 2e393db175cd55662f369d15905ce4eb44b154a9 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 18 Aug 2023 15:32:52 +0100 Subject: Changed use-after-free and double-free tests to expect KDAlloc, plus some small improvements. --- test/Feature/MultipleFreeResolution.c | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'test/Feature/MultipleFreeResolution.c') 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 #include @@ -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]); } -- cgit 1.4.1