From 667ce0f1ef33c32fbe2d1836fc1b334066e244ca Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 25 Jun 2022 21:02:58 +0100 Subject: Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. --- test/Feature/LargeArrayBecomesSym.c | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 test/Feature/LargeArrayBecomesSym.c (limited to 'test') diff --git a/test/Feature/LargeArrayBecomesSym.c b/test/Feature/LargeArrayBecomesSym.c new file mode 100644 index 00000000..a875e99e --- /dev/null +++ b/test/Feature/LargeArrayBecomesSym.c @@ -0,0 +1,33 @@ +/* This test checks that KLEE emits a warning when a large (> 4096) + concrete array becomes symbolic. */ + +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +/* The solver timeout is needed as some solvers, such as metaSMT+CVC4, time out here. */ +// RUN: %klee --max-solver-time=2 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s + +#include "klee/klee.h" + +#include +#include + +#define N 4100 + +int main() { + char a[N] = { + 1, + 2, + }; + + unsigned k; + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < N); + a[k] = 3; + // CHECK: KLEE: WARNING ONCE: Symbolic memory access will send the following array of 4100 bytes to the constraint solver + + unsigned i; + klee_make_symbolic(&i, sizeof(i), "i"); + klee_assume(i < N); + if (a[i] == 2) + assert(i == 1); +} -- cgit 1.4.1