diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-20 18:38:36 +0000 |
|---|---|---|
| committer | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-02-14 13:10:05 +0000 |
| commit | daf4eef5c3b99cdbc894f6bee40b4d047c5e6553 (patch) | |
| tree | 6336f7aa46c84a3b19f4c0e982101d444aa00adc /test | |
| parent | 19b7bdd916c484b52ce1237401b15a346575b4cf (diff) | |
| download | klee-daf4eef5c3b99cdbc894f6bee40b4d047c5e6553.tar.gz | |
ReadExpr::create() was missing an opportunity to constant fold when handling constant arrays.
Diffstat (limited to 'test')
| -rw-r--r-- | test/Feature/RewriteEqualities.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c index 6bf199f7..b3cc0ef7 100644 --- a/test/Feature/RewriteEqualities.c +++ b/test/Feature/RewriteEqualities.c @@ -5,7 +5,7 @@ // RUN: grep "N0)" %t.klee-out/test000003.kquery // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities %t.bc -// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.kquery +// RUN: FileCheck -input-file=%t.klee-out/test000003.kquery %s #include <stdio.h> #include <klee/klee.h> @@ -19,6 +19,8 @@ int run(unsigned char * x, unsigned char * y) { if(y[x[2]] < 11){ if(x[2] == 8){ + // CHECK: (query [(Eq 8 (Read w8 2 x))] + // CHECK-NEXT: false) return 2; } else{ return 3; |