about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--lib/Core/AddressSpace.cpp6
-rw-r--r--lib/Core/AddressSpace.h6
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;
 
     /***/