diff options
| author | Andrea Mattavelli <andreamattavelli@users.noreply.github.com> | 2017-02-14 14:46:56 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-02-14 14:46:56 +0000 |
| commit | 293f6e05ab8abdfca141eaa348da716b674c30e7 (patch) | |
| tree | 55128d04f6d03b4308a8ae3e9a5241d2a94794e3 /test | |
| parent | c3c3332a039e8e9cc10f93c3acb71c4240d4cab8 (diff) | |
| parent | 44b24dac6a05ccde0e01b54fd2b787a31e5d8811 (diff) | |
| download | klee-293f6e05ab8abdfca141eaa348da716b674c30e7.tar.gz | |
Merge pull request #574 from delcypher/read_expr_missed_constaint_fold
ReadExpr::create() was missing an opportunity to constant fold
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; |