about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2024-02-22 22:37:34 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-02-27 09:45:01 +0000
commit7a640c68ba7517b4a64f2cd684e91bd3de804580 (patch)
tree62388a9dc29e1641016d537b5838fd6b1944c87f /lib
parenta802c6dfd600f81d6131c055685188e0ac08bb9e (diff)
downloadklee-7a640c68ba7517b4a64f2cd684e91bd3de804580.tar.gz
Extend toConstant() to take an additional boolean argument that decides whether the expression is concretised. Also changed a C string argument to std::string.
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp15
-rw-r--r--lib/Core/Executor.h11
2 files changed, 12 insertions, 14 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c869f49d..d12af171 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1316,13 +1316,9 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
   return result;
 }
 
-
-/* Concretize the given expression, and return a possible constant value. 
-   'reason' is just a documentation string stating the reason for concretization. */
-ref<klee::ConstantExpr> 
-Executor::toConstant(ExecutionState &state, 
-                     ref<Expr> e,
-                     const char *reason) {
+ref<klee::ConstantExpr> Executor::toConstant(ExecutionState &state, ref<Expr> e,
+                                             const std::string &reason,
+                                             bool concretize) {
   e = ConstraintManager::simplifyExpr(state.constraints, e);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
     return CE;
@@ -1344,9 +1340,10 @@ Executor::toConstant(ExecutionState &state,
   if (ExternalCallWarnings == ExtCallWarnings::All)
     klee_warning("%s", os.str().c_str());
   else
-    klee_warning_once(reason, "%s", os.str().c_str());
+    klee_warning_once(reason.c_str(), "%s", os.str().c_str());
 
-  addConstraint(state, EqExpr::create(e, cvalue));
+  if (concretize)
+    addConstraint(state, EqExpr::create(e, cvalue));
 
   return cvalue;
 }
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,