diff options
author | Tomasz Kuchta <t.kuchta@samsung.com> | 2023-11-17 15:54:01 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-12 14:07:49 +0000 |
commit | 5ea5d436e4e52709c0f4e02a1b0ed97d944eeb4d (patch) | |
tree | e430ed64734e6cea5c0e0bf523e9a9f447971d65 /test/Feature/SingleObjectResolution.c | |
parent | ad0daf5bc3c534f93aff24d196efbfef2ef3e36b (diff) | |
download | klee-5ea5d436e4e52709c0f4e02a1b0ed97d944eeb4d.tar.gz |
Follow-up: applied review comments, implemented meta-data cleanup (one more map added to ExecutionState); now storing addresses of MemoryObjects for easier cleanup
Diffstat (limited to 'test/Feature/SingleObjectResolution.c')
-rw-r--r-- | test/Feature/SingleObjectResolution.c | 38 |
1 files changed, 27 insertions, 11 deletions
diff --git a/test/Feature/SingleObjectResolution.c b/test/Feature/SingleObjectResolution.c index 687ce9b6..7129d963 100644 --- a/test/Feature/SingleObjectResolution.c +++ b/test/Feature/SingleObjectResolution.c @@ -2,6 +2,8 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --single-object-resolution %t.bc > %t.log 2>&1 // RUN: FileCheck %s -input-file=%t.log +// RUN: %klee-stats --print-columns 'Queries' --table-format=csv %t.klee-out | FileCheck %s --check-prefix CHECK-STATS +// CHECK-STATS: 6218 #include "klee/klee.h" #include <stdlib.h> @@ -20,15 +22,19 @@ struct B { int z; }; -int foo(int *pointer) { - //printf("pointer is called\n"); - int *ptr = pointer + 123; +int bar(int *pointer, int selector) { + int *ptr = 0; + if (selector) + ptr = pointer + 123; + else + ptr = pointer + 124; + // CHECK: SingleObjectResolution.c:[[@LINE+1]]: memory error: out of bound pointer return *ptr; } -int main(int argc, char *argv[]) { - - int x; +int foo() { + size_t x; + int y; struct B b; // create a lot of memory objects @@ -38,15 +44,25 @@ int main(int argc, char *argv[]) { } klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&y, sizeof(y), "y"); b.y1 = malloc(20 * sizeof(struct A)); // dereference of a pointer within a struct int *tmp = &b.y1[x].z; - // CHECK: SingleObjectResolution.c:26: memory error: out of bound pointer - // CHECK: KLEE: done: completed paths = 1 - // CHECK: KLEE: done: partially completed paths = 1 - // CHECK: KLEE: done: generated tests = 2 - return foo(tmp); + int z = bar(tmp, y); + // cleanup test for heap + free(b.y1); + + tmp = &b.y[x].z; // this is to test the cleanup for stack vars + z = bar(tmp, y); + return z; +} + +int main(int argc, char *argv[]) { + // CHECK: KLEE: done: completed paths = 2 + // CHECK: KLEE: done: partially completed paths = 2 + // CHECK: KLEE: done: generated tests = 3 + return foo(); } |