From 4e99f8f1c7a336d83168ceb07b576a63b838cb2e Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Wed, 8 Nov 2023 16:26:37 +0000
Subject: Refactored some code related to seeding.

---
 lib/Core/SeedInfo.cpp | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

(limited to 'lib/Core/SeedInfo.cpp')

diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 55f4ed48..ddc40b26 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -74,27 +74,22 @@ void SeedInfo::patchSeed(const ExecutionState &state,
   std::set< std::pair<const Array*, unsigned> > directReads;
   std::vector< ref<ReadExpr> > reads;
   findReads(condition, false, reads);
-  for (std::vector< ref<ReadExpr> >::iterator it = reads.begin(), 
-         ie = reads.end(); it != ie; ++it) {
-    ReadExpr *re = it->get();
+  for (auto const &re : reads) {
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
       directReads.insert(std::make_pair(re->updates.root, 
                                         (unsigned) CE->getZExtValue(32)));
     }
   }
-  
-  for (std::set< std::pair<const Array*, unsigned> >::iterator
-         it = directReads.begin(), ie = directReads.end(); it != ie; ++it) {
-    const Array *array = it->first;
-    unsigned i = it->second;
+
+  for (auto const &[array, i] : directReads) {
     ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                       ConstantExpr::alloc(i, Expr::Int32));
     
-    // If not in bindings then this can't be a violation?
-    Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
-    if (it2 != assignment.bindings.end()) {
+    // If not in bindings, then this can't be a violation?
+    auto a = assignment.bindings.find(array);
+    if (a != assignment.bindings.end()) {
       ref<Expr> isSeed = EqExpr::create(read, 
-                                        ConstantExpr::alloc(it2->second[i], 
+                                        ConstantExpr::alloc(a->second[i],
                                                             Expr::Int8));
       bool res;
       bool success =
@@ -107,9 +102,9 @@ void SeedInfo::patchSeed(const ExecutionState &state,
             solver->getValue(required, read, value, state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");            
         (void) success;
-        it2->second[i] = value->getZExtValue(8);
+        a->second[i] = value->getZExtValue(8);
         cm.addConstraint(EqExpr::create(
-            read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
+            read, ConstantExpr::alloc(a->second[i], Expr::Int8)));
       } else {
         cm.addConstraint(isSeed);
       }
-- 
cgit 1.4.1