diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/Solver/Z3ConstantArray.c | 8 | ||||
| -rw-r--r-- | test/regression/2023-11-20-solver.c | 36 |
2 files changed, 40 insertions, 4 deletions
diff --git a/test/Solver/Z3ConstantArray.c b/test/Solver/Z3ConstantArray.c index d9495795..c49bbd1b 100644 --- a/test/Solver/Z3ConstantArray.c +++ b/test/Solver/Z3ConstantArray.c @@ -9,10 +9,10 @@ #include "klee/klee.h" int main(int argc, char **argv) { - // CHECK-DAG: (assert (= (select const_arr11 #x00000000) #x67)) - // CHECK-DAG: (assert (= (select const_arr11 #x00000001) #x79)) - // CHECK-DAG: (assert (= (select const_arr11 #x00000002) #x7a)) - // CHECK-DAG: (assert (= (select const_arr11 #x00000003) #x00)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000000) #x67)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000001) #x79)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000002) #x7a)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000003) #x00)) // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv0 32) ) (_ bv103 8) ) ) // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv1 32) ) (_ bv121 8) ) ) // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv2 32) ) (_ bv122 8) ) ) 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 |