2 files changed, 8 insertions, 5 deletions
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
index 739e51e6..6b67a1cf 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/util/ExprEvaluator.h
@@ -29,10 +29,11 @@ namespace klee {
   public:
     ExprEvaluator() {}
 
-    // override to implement evaluation, this function is called to
-    // get the initial value for a symbolic byte. if the value is
-    // unknown then the user can simply return a ReadExpr at version 0
-    // of this MemoryObject.
+    /// getInitialValue - Return the initial value for a symbolic byte.
+    ///
+    /// This will only be called for constant arrays if the index is
+    /// out-of-bounds. If the value is unknown then the user should return a
+    /// ReadExpr at the initial version of this array.
     virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
   };
 }
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index 2dafd6ff..61444c76 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -55,6 +55,8 @@ public:
 template<class T>
 class ExprRangeEvaluator {
 protected:
+  /// getInitialReadRange - Return a range for the initial value of the given
+  /// array (which may be constant), for the given range of indices.
   virtual T getInitialReadRange(const Array &os, T index) = 0;
 
   T evalRead(const UpdateList &ul, T index);
@@ -83,7 +85,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
       } 
     }
   }
-
+  
   return res.set_union(getInitialReadRange(*ul.root, index));
 }