diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2023-11-20 22:41:19 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-30 17:56:08 +0000 |
| commit | f813c88c8cb868fc9c0be78fbf92a94d72ac02b0 (patch) | |
| tree | 6647c2eb38a4a1502d9806bcdbfd919a07acaedc /test/regression | |
| parent | cb5e898561f9b8769d8838bc1bdca17a6f4f5d20 (diff) | |
| download | klee-f813c88c8cb868fc9c0be78fbf92a94d72ac02b0.tar.gz | |
Avoid generating array names in solver builders that could accidently collide
If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668
Diffstat (limited to 'test/regression')
| -rw-r--r-- | test/regression/2023-11-20-solver.c | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/test/regression/2023-11-20-solver.c b/test/regression/2023-11-20-solver.c new file mode 100644 index 00000000..ceef8180 --- /dev/null +++ b/test/regression/2023-11-20-solver.c @@ -0,0 +1,36 @@ +// Test case based on #1668, generates array names as part of the solver builder that collide. +// This depends on the order of expression evaluation. +// +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -silent-klee-assume --use-branch-cache=false --use-cex-cache=false --use-independent-solver=false %t1.bc 2>&1 | FileCheck %s +#include "klee/klee.h" +#include <assert.h> + +int main() { + int p1 = klee_int("val"); + int p2 = klee_int("val"); + int p3 = klee_int("val"); + int p4 = klee_int("val"); + int p5 = klee_int("val"); + int p6 = klee_int("val"); + int p7 = klee_int("val"); + int p8 = klee_int("val"); + int p9 = klee_int("val"); + int p10 = klee_int("val"); + int p11 = klee_int("val"); + int p12 = klee_int("val"); + int p13 = klee_int("val"); + int p14 = klee_int("val"); + int p15 = klee_int("val"); + int cond = klee_int("val"); + klee_assume(p12 > p14); + klee_assume(p6 > p3); + // klee_assume(p2 > 0); + klee_assume(p7 != 0); + klee_assume(p11 < p14 & p15 < p13); + klee_assume(cond > p5); + klee_assume(0 > p4); + // CHECK: [[@LINE+1]]: ASSERTION FAIL + assert(p2 > p11); +} \ No newline at end of file |