Extend toConstant() to take an additional boolean argument that decides whether the expression is concretised. Also changed a C string argument to std::string.

1 files changed, 6 insertions, 5 deletions

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index d19758d4..7be056a1 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -387,14 +387,15 @@ private:
   /// value). Otherwise return the original expression.
   ref<Expr> toUnique(const ExecutionState &state, ref<Expr> &e);
 
-  /// Return a constant value for the given expression, forcing it to
-  /// be constant in the given state by adding a constraint if
+  /// Return a constant value for the given expression.  If \param concretize is
+  /// true, the expression is forced to be a constant by adding a constraint if
   /// necessary. Note that this function breaks completeness and
   /// should generally be avoided.
   ///
-  /// \param purpose An identify string to printed in case of concretization.
-  ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e, 
-                                     const char *purpose);
+  /// \param reason A documentation string stating the reason for concretization
+  ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e,
+                                     const std::string &reason,
+                                     bool concretize = true);
 
   /// Evaluate the given expression under each seed, and return the
   /// first one that results in a constant, if such a seed exist.  Otherwise,