From 9d5bbe8a309c5760166febf7edfc3b790d77ab7e Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 20 Oct 2023 22:03:38 +0100 Subject: On a symbolic allocation, retrieve size from a seed, if available --- test/Feature/SeedConcretizeMalloc.c | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 test/Feature/SeedConcretizeMalloc.c (limited to 'test') diff --git a/test/Feature/SeedConcretizeMalloc.c b/test/Feature/SeedConcretizeMalloc.c new file mode 100644 index 00000000..1f916723 --- /dev/null +++ b/test/Feature/SeedConcretizeMalloc.c @@ -0,0 +1,32 @@ +// RUN: %clang -emit-llvm -c -g %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --entry-point=SeedGen %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: not test -f %t.klee-out/test000002.ktest + +// RUN: rm -rf %t.klee-out-2 +// RUN: %klee --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc | FileCheck --allow-empty %s + +#include "klee/klee.h" + +#include +#include +#include + +void SeedGen() { + unsigned x; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x == 100); +} + +int main(int argc, char **argv) { + unsigned s; + klee_make_symbolic(&s, sizeof(s), "size"); + char *p = (char *)malloc(s); + if (!p) + return 0; + + if (s != 100) + printf("Error\n"); + // CHECK-NOT: Error +} -- cgit 1.4.1