From 7ef508afbc4651362f05e0989f7a1700f50a5f22 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Tue, 9 Jun 2009 07:42:33 +0000 Subject: Add initial support for constant Arrays. - This doesn't actually start using them, it just attempts to update all clients to do the right thing in the presence of them. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73130 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Solver/IndependentSolver.cpp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/Solver/IndependentSolver.cpp') diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 69f9567c..1f3ea798 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -95,6 +95,12 @@ public: for (unsigned i = 0; i != reads.size(); ++i) { ReadExpr *re = reads[i].get(); const Array *array = re->updates.root; + + // Reads of a constant array don't alias. + if (re->updates.root->isConstantArray() && + !re->updates.head) + continue; + if (!wholeObjects.count(array)) { if (ConstantExpr *CE = dyn_cast(re->index)) { DenseSet &dis = elements[array]; -- cgit 1.4.1