1 files changed, 20 insertions, 10 deletions

diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 10549e7a..fa814950 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -32,15 +32,26 @@ namespace klee {
   };
   
   typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
-  
+
   class AddressSpace {
   private:
     /// Epoch counter used to control ownership of objects.
     mutable unsigned cowKey;
 
     /// Unsupported, use copy constructor
-    AddressSpace &operator=(const AddressSpace&); 
-    
+    AddressSpace &operator=(const AddressSpace &);
+
+    /// Check if pointer `p` can point to the memory object in the
+    /// given object pair.  If so, add it to the given resolution list.
+    ///
+    /// \return 1 iff the resolution is incomplete (`maxResolutions`
+    /// is non-zero and it was reached, or a query timed out), 0 iff
+    /// the resolution is complete (`p` can only point to the given
+    /// memory object), and 2 otherwise.
+    int checkPointerInObject(ExecutionState &state, TimingSolver *solver,
+                             ref<Expr> p, const ObjectPair &op,
+                             ResolutionList &rl, unsigned maxResolutions) const;
+
   public:
     /// The MemoryObject -> ObjectState map that constitutes the
     /// address space.
@@ -51,7 +62,6 @@ namespace klee {
     /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
     MemoryMap objects;
     
-  public:
     AddressSpace() : cowKey(1) {}
     AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { }
     ~AddressSpace() {}
@@ -76,15 +86,15 @@ namespace klee {
                     ObjectPair &result,
                     bool &success);
 
-    /// Resolve address to a list of ObjectPairs it can point to. If
-    /// maxResolutions is non-zero then no more than that many pairs
-    /// will be returned. 
+    /// Resolve pointer `p` to a list of `ObjectPairs` it can point
+    /// to. If `maxResolutions` is non-zero then no more than that many
+    /// pairs will be returned.
     ///
-    /// \return true iff the resolution is incomplete (maxResolutions
-    /// is non-zero and the search terminated early, or a query timed out).
+    /// \return true iff the resolution is incomplete (`maxResolutions`
+    /// is non-zero and it was reached, or a query timed out).
     bool resolve(ExecutionState &state,
                  TimingSolver *solver,
-                 ref<Expr> address, 
+                 ref<Expr> p,
                  ResolutionList &rl, 
                  unsigned maxResolutions=0,
                  double timeout=0.);