diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2019-10-30 10:48:05 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-12-12 17:50:24 +0000 |
commit | 85c22c2486c79b463451aeeba56a33313d4e460d (patch) | |
tree | 03b703cacaed2749e7130017395619211ae6e0a4 /lib/Expr/ArrayExprVisitor.cpp | |
parent | b715ffa0c805f4d4813f0cda8b17eeb618e1ebf0 (diff) | |
download | klee-85c22c2486c79b463451aeeba56a33313d4e460d.tar.gz |
[optimize-array] Fix value transformation
Value transformation operates on word instead of byte arrays. That means the Read indicies need to be adjusted to reflect that. Previously IndexCleanerVisitor tried to remove the multiplications in the index to covert byte indicies to word indicies. However as the two added test cases show this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide the index with word size which should always be correct.
Diffstat (limited to 'lib/Expr/ArrayExprVisitor.cpp')
-rw-r--r-- | lib/Expr/ArrayExprVisitor.cpp | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index 75604104..cada7867 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -256,19 +256,3 @@ ExprVisitor::Action ArrayValueOptReplaceVisitor::visitRead(const ReadExpr &re) { } return Action::doChildren(); } - -ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) { - if (mul) { - if (!isa<ConstantExpr>(e.getKid(0))) - index = e.getKid(0); - else if (!isa<ConstantExpr>(e.getKid(1))) - index = e.getKid(1); - mul = false; - } - return Action::doChildren(); -} - -ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &) { - mul = false; - return Action::doChildren(); -} |