From 3f65d6e9e41b5a5b458fb4642d8ac5bf684f3bc7 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 8 Nov 2023 18:24:40 +0000 Subject: Added a test for --allow-seed-extension --- test/Feature/SeedExtension.c | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 test/Feature/SeedExtension.c (limited to 'test/Feature/SeedExtension.c') diff --git a/test/Feature/SeedExtension.c b/test/Feature/SeedExtension.c new file mode 100644 index 00000000..04f6d7a6 --- /dev/null +++ b/test/Feature/SeedExtension.c @@ -0,0 +1,39 @@ +/* This test checks the case where the seed needs to be patched on re-run */ + +// RUN: %clang -emit-llvm -c %O0opt -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 --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest --allow-seed-extension %t.bc 2>&1 | FileCheck %s + +#include "klee/klee.h" + +#include +#include +#include + +void TestGen() { + int x; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x == 12345678); +} + +int main() { + int i; + klee_make_symbolic(&i, sizeof(i), "i"); + double d = i; + // CHECK: concretizing (reason: floating point) + assert((unsigned)d == 12345678); + + int j; + klee_make_symbolic(&j, sizeof(j), "j"); + if (j) + printf("Yes\n"); + // CHECK-DAG: Yes + else + printf("No\n"); + // CHECK-DAG: No +} -- cgit 1.4.1