Merge pull request #5766 from tautschnig/forall-objects

tautschnig · web-flow · commit 30b4af8e2afe · 2021-01-19T21:49:39.000+01:00
Remove {f,F}orall_objects
diff --git a/.clang-format b/.clang-format
@@ -38,8 +38,6 @@ ForEachMacros: [
   'Forall_goto_functions',
   'forall_goto_program_instructions',
   'Forall_goto_program_instructions',
-  'forall_objects',
-  'Forall_objects',
   'forall_valid_objects',
   'Forall_valid_objects',
   'forall_literals',
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
@@ -32,16 +32,6 @@ numberingt<irep_idt> value_set_fit::function_numbering;
 
 static const char *alloc_adapter_prefix="alloc_adaptor::";
 
-#define forall_objects(it, map) \
-  for(object_map_dt::const_iterator it = (map).begin(); \
-  it!=(map).end(); \
-  (it)++)
-
-#define Forall_objects(it, map) \
-  for(object_map_dt::iterator it = (map).begin(); \
-  it!=(map).end(); \
-  (it)++)
-
 void value_set_fit::output(
   const namespacet &ns,
   std::ostream &out) const
@@ -81,7 +71,10 @@ void value_set_fit::output(
 
     std::size_t width=0;
 
-    forall_objects(o_it, object_map.read())
+    const auto &entries = object_map.read();
+    for(object_map_dt::const_iterator o_it = entries.begin();
+        o_it != entries.end();
+        ++o_it)
     {
       const exprt &o=object_numbering[o_it->first];
 
@@ -124,7 +117,7 @@ void value_set_fit::output(
       object_map_dt::const_iterator next(o_it);
       next++;
 
-      if(next!=object_map.read().end())
+      if(next != entries.end())
       {
         out << ", ";
         if(width>=40)
@@ -168,9 +161,9 @@ void value_set_fit::flatten_rec(
 
   seen.insert(identifier + e.suffix);
 
-  forall_objects(it, e.object_map.read())
+  for(const auto &object_entry : e.object_map.read())
   {
-    const exprt &o=object_numbering[it->first];
+    const exprt &o = object_numbering[object_entry.first];
 
     if(o.type().id()=="#REF#")
     {
@@ -196,26 +189,26 @@ void value_set_fit::flatten_rec(
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second && it->second)
+          if(t_it->second && object_entry.second)
           {
-            *t_it->second += *it->second;
+            *t_it->second += *object_entry.second;
           }
           else
             t_it->second.reset();
         }
 
-        forall_objects(oit, temp.read())
-          insert(dest, *oit);
+        for(const auto &object_entry : temp.read())
+          insert(dest, object_entry);
       }
     }
     else
-      insert(dest, *it);
+      insert(dest, object_entry);
   }
 
   if(generalize_index) // this means we had recursive symbols in there
   {
-    Forall_objects(it, dest.write())
-      it->second.reset();
+    for(auto &object_entry : dest.write())
+      object_entry.second.reset();
   }
 
   seen.erase(identifier + e.suffix);
@@ -284,9 +277,9 @@ bool value_set_fit::make_union(object_mapt &dest, const object_mapt &src) const
 {
   bool result=false;
 
-  forall_objects(it, src.read())
+  for(const auto &object_entry : src.read())
   {
-    if(insert(dest, *it))
+    if(insert(dest, object_entry))
       result=true;
   }
 
@@ -301,9 +294,9 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
 
   object_mapt flat_map;
 
-  forall_objects(it, object_map.read())
+  for(const auto &object_entry : object_map.read())
   {
-    const exprt &object=object_numbering[it->first];
+    const exprt &object = object_numbering[object_entry.first];
     if(object.type().id()=="#REF#")
     {
       assert(object.id()==ID_symbol);
@@ -320,9 +313,9 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second && it->second)
+          if(t_it->second && object_entry.second)
           {
-            *t_it->second += *it->second;
+            *t_it->second += *object_entry.second;
           }
           else
             t_it->second.reset();
@@ -332,12 +325,12 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
       }
     }
     else
-      flat_map.write()[it->first]=it->second;
+      flat_map.write()[object_entry.first] = object_entry.second;
   }
 
   std::vector<exprt> result;
-  forall_objects(fit, flat_map.read())
-    result.push_back(to_expr(*fit));
+  for(const auto &object_entry : flat_map.read())
+    result.push_back(to_expr(object_entry));
 
 #if 0
   // Sanity check!
@@ -388,9 +381,16 @@ void value_set_fit::get_value_set_rec(
 
     if(fi!=values.end())
     {
-      forall_objects(it, fi->second.object_map.read())
-        get_value_set_rec(object_numbering[it->first], dest, suffix,
-                          original_type, ns, recursion_set);
+      for(const auto &object_entry : fi->second.object_map.read())
+      {
+        get_value_set_rec(
+          object_numbering[object_entry.first],
+          dest,
+          suffix,
+          original_type,
+          ns,
+          recursion_set);
+      }
       return;
     }
     else
@@ -502,9 +502,9 @@ void value_set_fit::get_value_set_rec(
 
     if(object_map.begin()!=object_map.end())
     {
-      forall_objects(it1, object_map)
+      for(const auto &object_entry : object_map)
       {
-        const exprt &object=object_numbering[it1->first];
+        const exprt &object = object_numbering[object_entry.first];
         get_value_set_rec(object, dest, suffix,
                           original_type, ns, recursion_set);
       }
@@ -560,9 +560,9 @@ void value_set_fit::get_value_set_rec(
       get_value_set_rec(*ptr_operand, pointer_expr_set, "",
                         ptr_operand->type(), ns, recursion_set);
 
-      forall_objects(it, pointer_expr_set.read())
+      for(const auto &object_entry : pointer_expr_set.read())
       {
-        offsett offset = it->second;
+        offsett offset = object_entry.second;
 
         if(offset_is_zero(offset) && expr.operands().size() == 2)
         {
@@ -586,7 +586,7 @@ void value_set_fit::get_value_set_rec(
         else
           offset.reset();
 
-        insert(dest, it->first, offset);
+        insert(dest, object_entry.first, offset);
       }
 
       return;
@@ -699,9 +699,9 @@ void value_set_fit::get_reference_set(
   object_mapt object_map;
   get_reference_set_sharing(expr, object_map, ns);
 
-  forall_objects(it, object_map.read())
+  for(const auto &object_entry : object_map.read())
   {
-    const exprt &object = object_numbering[it->first];
+    const exprt &object = object_numbering[object_entry.first];
 
     if(object.type().id() == "#REF#")
     {
@@ -722,9 +722,9 @@ void value_set_fit::get_reference_set(
             t_it!=omt.write().end();
             t_it++)
         {
-          if(t_it->second && it->second)
+          if(t_it->second && object_entry.second)
           {
-            *t_it->second += *it->second;
+            *t_it->second += *object_entry.second;
           }
           else
             t_it->second.reset();
@@ -735,7 +735,7 @@ void value_set_fit::get_reference_set(
       }
     }
     else
-      dest.insert(to_expr(*it));
+      dest.insert(to_expr(object_entry));
   }
 }
 
@@ -747,8 +747,8 @@ void value_set_fit::get_reference_set_sharing(
   object_mapt object_map;
   get_reference_set_sharing(expr, object_map, ns);
 
-  forall_objects(it, object_map.read())
-    dest.insert(to_expr(*it));
+  for(const auto &object_entry : object_map.read())
+    dest.insert(to_expr(object_entry));
 }
 
 void value_set_fit::get_reference_set_sharing_rec(
@@ -766,8 +766,11 @@ void value_set_fit::get_reference_set_sharing_rec(
     valuest::const_iterator fi = values.find(expr.get(ID_identifier));
     if(fi!=values.end())
     {
-      forall_objects(it, fi->second.object_map.read())
-        get_reference_set_sharing_rec(object_numbering[it->first], dest, ns);
+      for(const auto &object_entry : fi->second.object_map.read())
+      {
+        get_reference_set_sharing_rec(
+          object_numbering[object_entry.first], dest, ns);
+      }
       return;
     }
   }
@@ -796,9 +799,9 @@ void value_set_fit::get_reference_set_sharing_rec(
       recset);
 
     // REF's need to be dereferenced manually!
-    forall_objects(it, temp.read())
+    for(const auto &object_entry : temp.read())
     {
-      const exprt &obj = object_numbering[it->first];
+      const exprt &obj = object_numbering[object_entry.first];
       if(obj.type().id()=="#REF#")
       {
         const irep_idt &ident = obj.get(ID_identifier);
@@ -813,22 +816,22 @@ void value_set_fit::get_reference_set_sharing_rec(
               t_it!=t2.write().end();
               t_it++)
           {
-            if(t_it->second && it->second)
+            if(t_it->second && object_entry.second)
             {
-              *t_it->second += *it->second;
+              *t_it->second += *object_entry.second;
             }
             else
               t_it->second.reset();
           }
 
-          forall_objects(it2, t2.read())
-            insert(dest, *it2);
+          for(const auto &t2_object_entry : t2.read())
+            insert(dest, t2_object_entry);
         }
         else
           insert(dest, exprt(ID_unknown, obj.type().subtype()));
       }
       else
-        insert(dest, *it);
+        insert(dest, object_entry);
     }
 
     #if 0
@@ -854,9 +857,9 @@ void value_set_fit::get_reference_set_sharing_rec(
 
     const object_map_dt &object_map=array_references.read();
 
-    forall_objects(a_it, object_map)
+    for(const auto &object_entry : object_map)
     {
-      const exprt &object=object_numbering[a_it->first];
+      const exprt &object = object_numbering[object_entry.first];
 
       if(object.id()==ID_unknown)
         insert(dest, exprt(ID_unknown, expr.type()));
@@ -873,7 +876,7 @@ void value_set_fit::get_reference_set_sharing_rec(
         else
           casted_index = index_expr;
 
-        offsett o = a_it->second;
+        offsett o = object_entry.second;
         const auto i = numeric_cast<mp_integer>(offset);
 
         if(offset.is_zero())
@@ -899,9 +902,9 @@ void value_set_fit::get_reference_set_sharing_rec(
     object_mapt struct_references;
     get_reference_set_sharing(struct_op, struct_references, ns);
 
-    forall_objects(it, struct_references.read())
+    for(const auto &object_entry : struct_references.read())
     {
-      const exprt &object=object_numbering[it->first];
+      const exprt &object = object_numbering[object_entry.first];
       const typet &obj_type = object.type();
 
       if(object.id()==ID_unknown)
@@ -917,7 +920,7 @@ void value_set_fit::get_reference_set_sharing_rec(
       }
       else
       {
-        offsett o = it->second;
+        offsett o = object_entry.second;
 
         member_exprt member_expr(object, component_name, expr.type());
 
@@ -1127,10 +1130,13 @@ void value_set_fit::assign_rec(
     {
       recursion_set.insert(ident);
 
-      forall_objects(it, temp.read())
-        if(object_numbering[it->first].id()!=ID_unknown)
-          assign_rec(object_numbering[it->first], values_rhs,
-                     suffix, ns, recursion_set);
+      for(const auto &object_entry : temp.read())
+      {
+        const exprt &object = object_numbering[object_entry.first];
+
+        if(object.id() != ID_unknown)
+          assign_rec(object, values_rhs, suffix, ns, recursion_set);
+      }
 
       recursion_set.erase(ident);
     }
@@ -1172,9 +1178,9 @@ void value_set_fit::assign_rec(
     object_mapt reference_set;
     get_reference_set_sharing(lhs, reference_set, ns);
 
-    forall_objects(it, reference_set.read())
+    for(const auto &object_entry : reference_set.read())
     {
-      const exprt &object=object_numbering[it->first];
+      const exprt &object = object_numbering[object_entry.first];
 
       if(object.id()!=ID_unknown)
         assign_rec(object, values_rhs, suffix, ns, recursion_set);

Original file line number	Diff line number	Diff line change
`@@ -32,16 +32,6 @@ numberingt<irep_idt> value_set_fit::function_numbering;`
`32`	`32`
`33`	`33`	`static const char *alloc_adapter_prefix="alloc_adaptor::";`
`34`	`34`
`35`		`-#define forall_objects(it, map) \`
`36`		`- for(object_map_dt::const_iterator it = (map).begin(); \`
`37`		`- it!=(map).end(); \`
`38`		`- (it)++)`
`39`		`-`
`40`		`-#define Forall_objects(it, map) \`
`41`		`- for(object_map_dt::iterator it = (map).begin(); \`
`42`		`- it!=(map).end(); \`
`43`		`- (it)++)`
`44`		`-`
`45`	`35`	`void value_set_fit::output(`
`46`	`36`	`const namespacet &ns,`
`47`	`37`	`std::ostream &out) const`
`@@ -81,7 +71,10 @@ void value_set_fit::output(`
`81`	`71`
`82`	`72`	`std::size_t width=0;`
`83`	`73`
`84`		`- forall_objects(o_it, object_map.read())`
	`74`	`+ const auto &entries = object_map.read();`
	`75`	`+ for(object_map_dt::const_iterator o_it = entries.begin();`
	`76`	`+ o_it != entries.end();`
	`77`	`+ ++o_it)`
`85`	`78`	`{`
`86`	`79`	`const exprt &o=object_numbering[o_it->first];`
`87`	`80`
`@@ -124,7 +117,7 @@ void value_set_fit::output(`
`124`	`117`	`object_map_dt::const_iterator next(o_it);`
`125`	`118`	`next++;`
`126`	`119`
`127`		`- if(next!=object_map.read().end())`
	`120`	`+ if(next != entries.end())`
`128`	`121`	`{`
`129`	`122`	`out << ", ";`
`130`	`123`	`if(width>=40)`
`@@ -168,9 +161,9 @@ void value_set_fit::flatten_rec(`
`168`	`161`
`169`	`162`	`seen.insert(identifier + e.suffix);`
`170`	`163`
`171`		`- forall_objects(it, e.object_map.read())`
	`164`	`+ for(const auto &object_entry : e.object_map.read())`
`172`	`165`	`{`
`173`		`- const exprt &o=object_numbering[it->first];`
	`166`	`+ const exprt &o = object_numbering[object_entry.first];`
`174`	`167`
`175`	`168`	`if(o.type().id()=="#REF#")`
`176`	`169`	`{`
`@@ -196,26 +189,26 @@ void value_set_fit::flatten_rec(`
`196`	`189`	`t_it!=temp.write().end();`
`197`	`190`	`t_it++)`
`198`	`191`	`{`
`199`		`- if(t_it->second && it->second)`
	`192`	`+ if(t_it->second && object_entry.second)`
`200`	`193`	`{`
`201`		`- t_it->second += it->second;`
	`194`	`+ t_it->second += object_entry.second;`
`202`	`195`	`}`
`203`	`196`	`else`
`204`	`197`	`t_it->second.reset();`
`205`	`198`	`}`
`206`	`199`
`207`		`- forall_objects(oit, temp.read())`
`208`		`- insert(dest, *oit);`
	`200`	`+ for(const auto &object_entry : temp.read())`
	`201`	`+ insert(dest, object_entry);`
`209`	`202`	`}`
`210`	`203`	`}`
`211`	`204`	`else`
`212`		`- insert(dest, *it);`
	`205`	`+ insert(dest, object_entry);`
`213`	`206`	`}`
`214`	`207`
`215`	`208`	`if(generalize_index) // this means we had recursive symbols in there`
`216`	`209`	`{`
`217`		`- Forall_objects(it, dest.write())`
`218`		`- it->second.reset();`
	`210`	`+ for(auto &object_entry : dest.write())`
	`211`	`+ object_entry.second.reset();`
`219`	`212`	`}`
`220`	`213`
`221`	`214`	`seen.erase(identifier + e.suffix);`
`@@ -284,9 +277,9 @@ bool value_set_fit::make_union(object_mapt &dest, const object_mapt &src) const`
`284`	`277`	`{`
`285`	`278`	`bool result=false;`
`286`	`279`
`287`		`- forall_objects(it, src.read())`
	`280`	`+ for(const auto &object_entry : src.read())`
`288`	`281`	`{`
`289`		`- if(insert(dest, *it))`
	`282`	`+ if(insert(dest, object_entry))`
`290`	`283`	`result=true;`
`291`	`284`	`}`
`292`	`285`
`@@ -301,9 +294,9 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const`
`301`	`294`
`302`	`295`	`object_mapt flat_map;`
`303`	`296`
`304`		`- forall_objects(it, object_map.read())`
	`297`	`+ for(const auto &object_entry : object_map.read())`
`305`	`298`	`{`
`306`		`- const exprt &object=object_numbering[it->first];`
	`299`	`+ const exprt &object = object_numbering[object_entry.first];`
`307`	`300`	`if(object.type().id()=="#REF#")`
`308`	`301`	`{`
`309`	`302`	`assert(object.id()==ID_symbol);`
`@@ -320,9 +313,9 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const`
`320`	`313`	`t_it!=temp.write().end();`
`321`	`314`	`t_it++)`
`322`	`315`	`{`
`323`		`- if(t_it->second && it->second)`
	`316`	`+ if(t_it->second && object_entry.second)`
`324`	`317`	`{`
`325`		`- t_it->second += it->second;`
	`318`	`+ t_it->second += object_entry.second;`
`326`	`319`	`}`
`327`	`320`	`else`
`328`	`321`	`t_it->second.reset();`
`@@ -332,12 +325,12 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const`
`332`	`325`	`}`
`333`	`326`	`}`
`334`	`327`	`else`
`335`		`- flat_map.write()[it->first]=it->second;`
	`328`	`+ flat_map.write()[object_entry.first] = object_entry.second;`
`336`	`329`	`}`
`337`	`330`
`338`	`331`	`std::vector<exprt> result;`
`339`		`- forall_objects(fit, flat_map.read())`
`340`		`- result.push_back(to_expr(*fit));`
	`332`	`+ for(const auto &object_entry : flat_map.read())`
	`333`	`+ result.push_back(to_expr(object_entry));`
`341`	`334`
`342`	`335`	`#if 0`
`343`	`336`	`// Sanity check!`
`@@ -388,9 +381,16 @@ void value_set_fit::get_value_set_rec(`
`388`	`381`
`389`	`382`	`if(fi!=values.end())`
`390`	`383`	`{`
`391`		`- forall_objects(it, fi->second.object_map.read())`
`392`		`- get_value_set_rec(object_numbering[it->first], dest, suffix,`
`393`		`- original_type, ns, recursion_set);`
	`384`	`+ for(const auto &object_entry : fi->second.object_map.read())`
	`385`	`+ {`
	`386`	`+ get_value_set_rec(`
	`387`	`+ object_numbering[object_entry.first],`
	`388`	`+ dest,`
	`389`	`+ suffix,`
	`390`	`+ original_type,`
	`391`	`+ ns,`
	`392`	`+ recursion_set);`
	`393`	`+ }`
`394`	`394`	`return;`
`395`	`395`	`}`
`396`	`396`	`else`
`@@ -502,9 +502,9 @@ void value_set_fit::get_value_set_rec(`
`502`	`502`
`503`	`503`	`if(object_map.begin()!=object_map.end())`
`504`	`504`	`{`
`505`		`- forall_objects(it1, object_map)`
	`505`	`+ for(const auto &object_entry : object_map)`
`506`	`506`	`{`
`507`		`- const exprt &object=object_numbering[it1->first];`
	`507`	`+ const exprt &object = object_numbering[object_entry.first];`
`508`	`508`	`get_value_set_rec(object, dest, suffix,`
`509`	`509`	`original_type, ns, recursion_set);`
`510`	`510`	`}`
`@@ -560,9 +560,9 @@ void value_set_fit::get_value_set_rec(`
`560`	`560`	`get_value_set_rec(*ptr_operand, pointer_expr_set, "",`
`561`	`561`	`ptr_operand->type(), ns, recursion_set);`
`562`	`562`
`563`		`- forall_objects(it, pointer_expr_set.read())`
	`563`	`+ for(const auto &object_entry : pointer_expr_set.read())`
`564`	`564`	`{`
`565`		`- offsett offset = it->second;`
	`565`	`+ offsett offset = object_entry.second;`
`566`	`566`
`567`	`567`	`if(offset_is_zero(offset) && expr.operands().size() == 2)`
`568`	`568`	`{`
`@@ -586,7 +586,7 @@ void value_set_fit::get_value_set_rec(`
`586`	`586`	`else`
`587`	`587`	`offset.reset();`
`588`	`588`
`589`		`- insert(dest, it->first, offset);`
	`589`	`+ insert(dest, object_entry.first, offset);`
`590`	`590`	`}`
`591`	`591`
`592`	`592`	`return;`
`@@ -699,9 +699,9 @@ void value_set_fit::get_reference_set(`
`699`	`699`	`object_mapt object_map;`
`700`	`700`	`get_reference_set_sharing(expr, object_map, ns);`
`701`	`701`
`702`		`- forall_objects(it, object_map.read())`
	`702`	`+ for(const auto &object_entry : object_map.read())`
`703`	`703`	`{`
`704`		`- const exprt &object = object_numbering[it->first];`
	`704`	`+ const exprt &object = object_numbering[object_entry.first];`
`705`	`705`
`706`	`706`	`if(object.type().id() == "#REF#")`
`707`	`707`	`{`
`@@ -722,9 +722,9 @@ void value_set_fit::get_reference_set(`
`722`	`722`	`t_it!=omt.write().end();`
`723`	`723`	`t_it++)`
`724`	`724`	`{`
`725`		`- if(t_it->second && it->second)`
	`725`	`+ if(t_it->second && object_entry.second)`
`726`	`726`	`{`
`727`		`- t_it->second += it->second;`
	`727`	`+ t_it->second += object_entry.second;`
`728`	`728`	`}`
`729`	`729`	`else`
`730`	`730`	`t_it->second.reset();`
`@@ -735,7 +735,7 @@ void value_set_fit::get_reference_set(`
`735`	`735`	`}`
`736`	`736`	`}`
`737`	`737`	`else`
`738`		`- dest.insert(to_expr(*it));`
	`738`	`+ dest.insert(to_expr(object_entry));`
`739`	`739`	`}`
`740`	`740`	`}`
`741`	`741`
`@@ -747,8 +747,8 @@ void value_set_fit::get_reference_set_sharing(`
`747`	`747`	`object_mapt object_map;`
`748`	`748`	`get_reference_set_sharing(expr, object_map, ns);`
`749`	`749`
`750`		`- forall_objects(it, object_map.read())`
`751`		`- dest.insert(to_expr(*it));`
	`750`	`+ for(const auto &object_entry : object_map.read())`
	`751`	`+ dest.insert(to_expr(object_entry));`
`752`	`752`	`}`
`753`	`753`
`754`	`754`	`void value_set_fit::get_reference_set_sharing_rec(`
`@@ -766,8 +766,11 @@ void value_set_fit::get_reference_set_sharing_rec(`
`766`	`766`	`valuest::const_iterator fi = values.find(expr.get(ID_identifier));`
`767`	`767`	`if(fi!=values.end())`
`768`	`768`	`{`
`769`		`- forall_objects(it, fi->second.object_map.read())`
`770`		`- get_reference_set_sharing_rec(object_numbering[it->first], dest, ns);`
	`769`	`+ for(const auto &object_entry : fi->second.object_map.read())`
	`770`	`+ {`
	`771`	`+ get_reference_set_sharing_rec(`
	`772`	`+ object_numbering[object_entry.first], dest, ns);`
	`773`	`+ }`
`771`	`774`	`return;`
`772`	`775`	`}`
`773`	`776`	`}`
`@@ -796,9 +799,9 @@ void value_set_fit::get_reference_set_sharing_rec(`
`796`	`799`	`recset);`
`797`	`800`
`798`	`801`	`// REF's need to be dereferenced manually!`
`799`		`- forall_objects(it, temp.read())`
	`802`	`+ for(const auto &object_entry : temp.read())`
`800`	`803`	`{`
`801`		`- const exprt &obj = object_numbering[it->first];`
	`804`	`+ const exprt &obj = object_numbering[object_entry.first];`
`802`	`805`	`if(obj.type().id()=="#REF#")`
`803`	`806`	`{`
`804`	`807`	`const irep_idt &ident = obj.get(ID_identifier);`
`@@ -813,22 +816,22 @@ void value_set_fit::get_reference_set_sharing_rec(`
`813`	`816`	`t_it!=t2.write().end();`
`814`	`817`	`t_it++)`
`815`	`818`	`{`
`816`		`- if(t_it->second && it->second)`
	`819`	`+ if(t_it->second && object_entry.second)`
`817`	`820`	`{`
`818`		`- t_it->second += it->second;`
	`821`	`+ t_it->second += object_entry.second;`
`819`	`822`	`}`
`820`	`823`	`else`
`821`	`824`	`t_it->second.reset();`
`822`	`825`	`}`
`823`	`826`
`824`		`- forall_objects(it2, t2.read())`
`825`		`- insert(dest, *it2);`
	`827`	`+ for(const auto &t2_object_entry : t2.read())`
	`828`	`+ insert(dest, t2_object_entry);`
`826`	`829`	`}`
`827`	`830`	`else`
`828`	`831`	`insert(dest, exprt(ID_unknown, obj.type().subtype()));`
`829`	`832`	`}`
`830`	`833`	`else`
`831`		`- insert(dest, *it);`
	`834`	`+ insert(dest, object_entry);`
`832`	`835`	`}`
`833`	`836`
`834`	`837`	`#if 0`
`@@ -854,9 +857,9 @@ void value_set_fit::get_reference_set_sharing_rec(`
`854`	`857`
`855`	`858`	`const object_map_dt &object_map=array_references.read();`
`856`	`859`
`857`		`- forall_objects(a_it, object_map)`
	`860`	`+ for(const auto &object_entry : object_map)`
`858`	`861`	`{`
`859`		`- const exprt &object=object_numbering[a_it->first];`
	`862`	`+ const exprt &object = object_numbering[object_entry.first];`
`860`	`863`
`861`	`864`	`if(object.id()==ID_unknown)`
`862`	`865`	`insert(dest, exprt(ID_unknown, expr.type()));`
`@@ -873,7 +876,7 @@ void value_set_fit::get_reference_set_sharing_rec(`
`873`	`876`	`else`
`874`	`877`	`casted_index = index_expr;`
`875`	`878`
`876`		`- offsett o = a_it->second;`
	`879`	`+ offsett o = object_entry.second;`
`877`	`880`	`const auto i = numeric_cast<mp_integer>(offset);`
`878`	`881`
`879`	`882`	`if(offset.is_zero())`
`@@ -899,9 +902,9 @@ void value_set_fit::get_reference_set_sharing_rec(`
`899`	`902`	`object_mapt struct_references;`
`900`	`903`	`get_reference_set_sharing(struct_op, struct_references, ns);`
`901`	`904`
`902`		`- forall_objects(it, struct_references.read())`
	`905`	`+ for(const auto &object_entry : struct_references.read())`
`903`	`906`	`{`
`904`		`- const exprt &object=object_numbering[it->first];`
	`907`	`+ const exprt &object = object_numbering[object_entry.first];`
`905`	`908`	`const typet &obj_type = object.type();`
`906`	`909`
`907`	`910`	`if(object.id()==ID_unknown)`
`@@ -917,7 +920,7 @@ void value_set_fit::get_reference_set_sharing_rec(`
`917`	`920`	`}`
`918`	`921`	`else`
`919`	`922`	`{`
`920`		`- offsett o = it->second;`
	`923`	`+ offsett o = object_entry.second;`
`921`	`924`
`922`	`925`	`member_exprt member_expr(object, component_name, expr.type());`
`923`	`926`
`@@ -1127,10 +1130,13 @@ void value_set_fit::assign_rec(`
`1127`	`1130`	`{`
`1128`	`1131`	`recursion_set.insert(ident);`
`1129`	`1132`
`1130`		`- forall_objects(it, temp.read())`
`1131`		`- if(object_numbering[it->first].id()!=ID_unknown)`
`1132`		`- assign_rec(object_numbering[it->first], values_rhs,`
`1133`		`- suffix, ns, recursion_set);`
	`1133`	`+ for(const auto &object_entry : temp.read())`
	`1134`	`+ {`
	`1135`	`+ const exprt &object = object_numbering[object_entry.first];`
	`1136`	`+`
	`1137`	`+ if(object.id() != ID_unknown)`
	`1138`	`+ assign_rec(object, values_rhs, suffix, ns, recursion_set);`
	`1139`	`+ }`
`1134`	`1140`
`1135`	`1141`	`recursion_set.erase(ident);`
`1136`	`1142`	`}`
`@@ -1172,9 +1178,9 @@ void value_set_fit::assign_rec(`
`1172`	`1178`	`object_mapt reference_set;`
`1173`	`1179`	`get_reference_set_sharing(lhs, reference_set, ns);`
`1174`	`1180`
`1175`		`- forall_objects(it, reference_set.read())`
	`1181`	`+ for(const auto &object_entry : reference_set.read())`
`1176`	`1182`	`{`
`1177`		`- const exprt &object=object_numbering[it->first];`
	`1183`	`+ const exprt &object = object_numbering[object_entry.first];`
`1178`	`1184`
`1179`	`1185`	`if(object.id()!=ID_unknown)`
`1180`	`1186`	`assign_rec(object, values_rhs, suffix, ns, recursion_set);`