diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-09-20 15:50:34 +0100 |
|---|---|---|
| committer | MartinNowack <martin.nowack@gmail.com> | 2018-10-03 12:25:49 +0100 |
| commit | da573cbf6a18892c4ad54ea622fbd4307d8cfdbc (patch) | |
| tree | 4de98f4b3f0215b7b4971f708794b9bd715c8f60 /lib | |
| parent | 888ae3b6193a29c5358331c789ba7949ae96d614 (diff) | |
| download | klee-da573cbf6a18892c4ad54ea622fbd4307d8cfdbc.tar.gz | |
Marking resolve methods as const
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Core/AddressSpace.cpp | 6 | ||||
| -rw-r--r-- | lib/Core/AddressSpace.h | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 78dab30a..0f5a2bb7 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -52,7 +52,7 @@ ObjectState *AddressSpace::getWriteable(const MemoryObject *mo, /// bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr, - ObjectPair &result) { + ObjectPair &result) const { uint64_t address = addr->getZExtValue(); MemoryObject hack(address); @@ -74,7 +74,7 @@ bool AddressSpace::resolveOne(ExecutionState &state, TimingSolver *solver, ref<Expr> address, ObjectPair &result, - bool &success) { + bool &success) const { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) { success = resolveOne(CE, result); return true; @@ -196,7 +196,7 @@ int AddressSpace::checkPointerInObject(ExecutionState &state, bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, ref<Expr> p, ResolutionList &rl, - unsigned maxResolutions, double timeout) { + unsigned maxResolutions, double timeout) const { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) { ObjectPair res; if (resolveOne(CE, res)) diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index fa814950..57c0e472 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -69,7 +69,7 @@ namespace klee { /// Resolve address to an ObjectPair in result. /// \return true iff an object was found. bool resolveOne(const ref<ConstantExpr> &address, - ObjectPair &result); + ObjectPair &result) const; /// Resolve address to an ObjectPair in result. /// @@ -84,7 +84,7 @@ namespace klee { TimingSolver *solver, ref<Expr> address, ObjectPair &result, - bool &success); + bool &success) const; /// Resolve pointer `p` to a list of `ObjectPairs` it can point /// to. If `maxResolutions` is non-zero then no more than that many @@ -97,7 +97,7 @@ namespace klee { ref<Expr> p, ResolutionList &rl, unsigned maxResolutions=0, - double timeout=0.); + double timeout=0.) const; /***/ |