From 251b28e464921a9507f56f1d1138ff8df146888f Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 20 Oct 2023 20:50:29 +0100 Subject: Concretize arguments to external function calls using seeds, if available. Added a test case. --- test/Feature/SeedConcretizeExternalCall.c | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 test/Feature/SeedConcretizeExternalCall.c (limited to 'test') diff --git a/test/Feature/SeedConcretizeExternalCall.c b/test/Feature/SeedConcretizeExternalCall.c new file mode 100644 index 00000000..7eb69698 --- /dev/null +++ b/test/Feature/SeedConcretizeExternalCall.c @@ -0,0 +1,25 @@ +// 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=TestGen %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 --external-calls=all --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc + +#include "klee/klee.h" + +#include +#include + +void TestGen() { + int x; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x == 12345678); +} + +int main() { + int x; + klee_make_symbolic(&x, sizeof(x), "x"); + assert(abs(x) == 12345678); +} -- cgit 1.4.1