From 807b4e140d8afb55b3651fdcaf9ebe733afeb67e Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Mon, 8 Jun 2009 06:34:38 +0000 Subject: FastCexSolver: Add exact value contents to CexObjectData. - The exact contents are a conservative approximation for the values of each array location, to be used for proving valid queries. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73054 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Solver/FastCexSolver.cpp | 42 +++++++++++++++++++++++++++++------------- 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index f638f2ce..516df85d 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -288,35 +288,51 @@ inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) { typedef ValueRange CexValueData; class CexObjectData { - std::vector contents; + /// possibleContents - An array of "possible" values for the object. + /// + /// The possible values is an inexact approximation for the set of values for + /// each array location. + std::vector possibleContents; + + /// exactContents - An array of exact values for the object. + /// + /// The exact values are a conservative approximation for the set of values + /// for each array location. + std::vector exactContents; CexObjectData(const CexObjectData&); // DO NOT IMPLEMENT void operator=(const CexObjectData&); // DO NOT IMPLEMENT public: - CexObjectData(uint64_t size) : contents(size) { - for (uint64_t i = 0; i != size; ++i) - contents[i] = ValueRange(0, 255); + CexObjectData(uint64_t size) : possibleContents(size), exactContents(size) { + for (uint64_t i = 0; i != size; ++i) { + possibleContents[i] = ValueRange(0, 255); + exactContents[i] = ValueRange(0, 255); + } } - CexValueData getPossibleValues(size_t index) { - return contents[index]; - } const CexValueData getPossibleValues(size_t index) const { - return contents[index]; + return possibleContents[index]; } void setPossibleValues(size_t index, CexValueData values) { - contents[index] = values; + possibleContents[index] = values; + } + void setPossibleValue(size_t index, unsigned char value) { + possibleContents[index] = CexValueData(value); + } + + const CexValueData getExactValues(size_t index) const { + return exactContents[index]; + } + void setExactValues(size_t index, CexValueData values) { + exactContents[index] = values; } /// getPossibleValue - Return some possible value. unsigned char getPossibleValue(size_t index) const { - const CexValueData &cvd = contents[index]; + const CexValueData &cvd = possibleContents[index]; return cvd.min() + (cvd.max() - cvd.min()) / 2; } - void setPossibleValue(size_t index, unsigned char value) { - contents[index] = CexValueData(value); - } }; class CexRangeEvaluator : public ExprRangeEvaluator { -- cgit 1.4.1