about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-11-22 22:59:32 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-30 17:30:11 +0000
commit42662b71a53d2e72481bc46994f44e47c7528a34 (patch)
tree6165c24d2b9659dff71dc2655c19934b11ecc50d
parent3e006dbfacd06e12818d97ae5aab1960324b27f9 (diff)
downloadklee-42662b71a53d2e72481bc46994f44e47c7528a34.tar.gz
Make Assignment::evaluate be const
-rw-r--r--include/klee/Expr/Assignment.h4
-rw-r--r--lib/Core/Executor.cpp2
2 files changed, 3 insertions, 3 deletions
diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h
index 7384e0cc..ba0c2a6c 100644
--- a/include/klee/Expr/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -44,7 +44,7 @@ namespace klee {
     }
     
     ref<Expr> evaluate(const Array *mo, unsigned index) const;
-    ref<Expr> evaluate(ref<Expr> e);
+    ref<Expr> evaluate(ref<Expr> e) const;
     ConstraintSet createConstraintsFromAssignment() const;
 
     template<typename InputIterator>
@@ -82,7 +82,7 @@ namespace klee {
     }
   }
 
-  inline ref<Expr> Assignment::evaluate(ref<Expr> e) { 
+  inline ref<Expr> Assignment::evaluate(ref<Expr> e) const { 
     AssignmentEvaluator v(*this);
     return v.visit(e); 
   }
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c07fa18e..73f994ce 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1351,7 +1351,7 @@ Executor::toConstant(ExecutionState &state,
 ref<klee::Expr>
 Executor::getValueFromSeeds(std::vector<SeedInfo> &seeds, ref<Expr> e) {
   assert(!seeds.empty());
-  for (auto seed:seeds) {
+  for (auto const &seed : seeds) {
     auto value = seed.assignment.evaluate(e);
     if (isa<ConstantExpr>(value))
       return value;