diff options
Diffstat (limited to 'include/klee/util/ExprEvaluator.h')
-rw-r--r-- | include/klee/util/ExprEvaluator.h | 9 |
1 files changed, 5 insertions, 4 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; }; } |