Merge pull request #1839 from thomasspriggs/tidy_up1

Refactoring usage of `forall_symbols` macro into c++11 loops and replacement of asserts.

Author: Daniel Kroening

src/analyses/invariant_propagation.cpp

@@ -173,10 +173,13 @@ void invariant_propagationt::get_globals(
   object_listt &dest)
 {
   // static ones
-  forall_symbols(it, ns.get_symbol_table().symbols)
-    if(it->second.is_lvalue &&
-       it->second.is_static_lifetime)
-      get_objects(it->second, dest);
+  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
+  {
+    if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
+    {
+      get_objects(symbol_pair.second, dest);
+    }
+  }
 }
 
 bool invariant_propagationt::check_type(const typet &type) const

src/goto-instrument/alignment_checks.cpp

@@ -19,21 +19,21 @@ void print_struct_alignment_problems(
   const symbol_tablet &symbol_table,
   std::ostream &out)
 {
-  forall_symbols(it, symbol_table.symbols)
-    if(it->second.is_type && it->second.type.id()==ID_struct)
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
-      const struct_typet &str=to_struct_type(it->second.type);
-      const struct_typet::componentst &components=str.components();
+      const struct_typet &str = to_struct_type(symbol_pair.second.type);
+      const struct_typet::componentst &components = str.components();
 
-      bool first_time_seen_in_struct=true;
+      bool first_time_seen_in_struct = true;
 
-      for(struct_typet::componentst::const_iterator
-          it_mem=components.begin();
-          it_mem!=components.end();
+      for(struct_typet::componentst::const_iterator it_mem = components.begin();
+          it_mem != components.end();
           it_mem++)
       {
-        mp_integer cumulated_length=0;
-        bool first_time_seen_from=true;
+        mp_integer cumulated_length = 0;
+        bool first_time_seen_from = true;
 
         // if the instruction cannot be aligned to the address,
         // try the next one
@@ -42,40 +42,39 @@ void print_struct_alignment_problems(
           // || alignment(it_mem->type())%config.ansi_c.alignment!=0)
           continue;
 
-        for(struct_typet::componentst::const_iterator
-            it_next=it_mem;
-            it_next!=components.end();
+        for(struct_typet::componentst::const_iterator it_next = it_mem;
+            it_next != components.end();
             it_next++)
         {
-          const typet &it_type=it_next->type();
+          const typet &it_type = it_next->type();
           const namespacet ns(symbol_table);
-          mp_integer size=pointer_offset_size(it_type, ns);
+          mp_integer size = pointer_offset_size(it_type, ns);
 
-          if(size<0)
-            throw "type of unknown size:\n"+it_type.pretty();
+          if(size < 0)
+            throw "type of unknown size:\n" + it_type.pretty();
 
-          cumulated_length+=size;
+          cumulated_length += size;
           // [it_mem;it_next] cannot be covered by an instruction
-          if(cumulated_length>config.ansi_c.memory_operand_size)
+          if(cumulated_length > config.ansi_c.memory_operand_size)
           {
             // if interferences have been found, no need to check with
             // starting from an already covered member
             if(!first_time_seen_from)
-              it_mem=it_next-1;
+              it_mem = it_next - 1;
             break;
           }
 
-          if(it_mem!=it_next && !it_next->get_is_padding())
+          if(it_mem != it_next && !it_next->get_is_padding())
           {
             if(first_time_seen_in_struct)
             {
-              first_time_seen_in_struct=false;
-              first_time_seen_from=false;
+              first_time_seen_in_struct = false;
+              first_time_seen_from = false;
 
               out << "\nWARNING: "
                   << "declaration of structure "
-                  << str.find_type(ID_tag).pretty()
-                  << " at " << it->second.location << '\n';
+                  << str.find_type(ID_tag).pretty() << " at "
+                  << symbol_pair.second.location << '\n';
             }
 
             out << "members " << it_mem->get_pretty_name() << " and "
@@ -84,12 +83,12 @@ void print_struct_alignment_problems(
         }
       }
     }
-    else if(it->second.type.id()==ID_array)
+    else if(symbol_pair.second.type.id() == ID_array)
     {
       // is this structure likely to introduce data races?
       #if 0
       const namespacet ns(symbol_table);
-      const array_typet array=to_array_type(it->second.type);
+      const array_typet array=to_array_type(symbol_pair.second.type);
       const mp_integer size=
         pointer_offset_size(array.subtype(), ns);
 
@@ -100,9 +99,10 @@ void print_struct_alignment_problems(
       {
         out << "\nWARNING: "
             << "declaration of an array at "
-            << it->second.location <<
+            << symbol_pair.second.location <<
             << "\nmight be concurrently accessed\n";
       }
       #endif
     }
+  }
 }

src/goto-instrument/dump_c.cpp

@@ -82,8 +82,10 @@ void dump_ct::operator()(std::ostream &os)
       }
     }
   }
-  forall_symbols(it, symbols_transparent.symbols)
-    copied_symbol_table.add(it->second);
+  for(const auto &symbol_pair : symbols_transparent.symbols)
+  {
+    copied_symbol_table.add(symbol_pair.second);
+  }
 
   typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
   unique_tagst unique_tags;

src/goto-instrument/model_argc_argv.cpp

@@ -114,25 +114,27 @@ bool model_argc_argv(
   // locate the body of the newly built start function as well as any
   // additional declarations we might need; the body will then be
   // converted and inserted into the start function
-  forall_symbols(it, tmp_symbol_table.symbols)
+  for(const auto &symbol_pair : tmp_symbol_table.symbols)
   {
     // add __CPROVER_assume if necessary (it might exist already)
-    if(it->first==CPROVER_PREFIX "assume" ||
-       it->first==CPROVER_PREFIX "input")
-      goto_model.symbol_table.add(it->second);
-    else if(it->first==goto_model.goto_functions.entry_point())
+    if(
+      symbol_pair.first == CPROVER_PREFIX "assume" ||
+      symbol_pair.first == CPROVER_PREFIX "input")
+      goto_model.symbol_table.add(symbol_pair.second);
+    else if(symbol_pair.first == goto_model.goto_functions.entry_point())
     {
-      value=it->second.value;
+      value = symbol_pair.second.value;
 
       replace_symbolt replace;
       replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
       replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
       replace(value);
     }
-    else if(has_prefix(
-        id2string(it->first),
-        id2string(goto_model.goto_functions.entry_point())+"::") &&
-      goto_model.symbol_table.add(it->second))
+    else if(
+      has_prefix(
+        id2string(symbol_pair.first),
+        id2string(goto_model.goto_functions.entry_point()) + "::") &&
+      goto_model.symbol_table.add(symbol_pair.second))
       UNREACHABLE;
   }
   POSTCONDITION(value.is_not_nil());

src/goto-programs/class_hierarchy.cpp

@@ -24,12 +24,11 @@ Date: April 2016
 /// \param symbol_table: The symbol table to analyze
 void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
 {
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(it->second.is_type && it->second.type.id()==ID_struct)
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
-      const struct_typet &struct_type=
-        to_struct_type(it->second.type);
+      const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
 
       const irept::subt &bases=
         struct_type.find(ID_bases).get_sub();
@@ -40,8 +39,8 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
         if(parent.empty())
           continue;
 
-        class_map[parent].children.push_back(it->first);
-        class_map[it->first].parents.push_back(parent);
+        class_map[parent].children.push_back(symbol_pair.first);
+        class_map[symbol_pair.first].parents.push_back(parent);
       }
     }
   }
@@ -55,28 +54,31 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
 void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
 {
   // Add nodes for all classes:
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(it->second.is_type && it->second.type.id() == ID_struct)
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
       node_indext new_node_index = add_node();
-      nodes_by_name[it->first] = new_node_index;
-      (*this)[new_node_index].class_identifier = it->first;
+      nodes_by_name[symbol_pair.first] = new_node_index;
+      (*this)[new_node_index].class_identifier = symbol_pair.first;
     }
   }
 
   // Add parent -> child edges:
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(it->second.is_type && it->second.type.id() == ID_struct)
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
-      const class_typet &class_type = to_class_type(it->second.type);
+      const class_typet &class_type = to_class_type(symbol_pair.second.type);
 
       for(const auto &base : class_type.bases())
       {
         const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
         if(!parent.empty())
-          add_edge(nodes_by_name.at(parent), nodes_by_name.at(it->first));
+        {
+          add_edge(
+            nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first));
+        }
       }
     }
   }

src/goto-programs/goto_convert_functions.cpp

@@ -38,16 +38,16 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
   typedef std::list<irep_idt> symbol_listt;
   symbol_listt symbol_list;
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(!it->second.is_type &&
-       !it->second.is_macro &&
-       it->second.type.id()==ID_code &&
-       (it->second.mode==ID_C ||
-        it->second.mode==ID_cpp ||
-        it->second.mode==ID_java ||
-        it->second.mode=="jsil"))
-      symbol_list.push_back(it->first);
+    if(
+      !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
+      symbol_pair.second.type.id() == ID_code &&
+      (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
+       symbol_pair.second.mode == ID_java || symbol_pair.second.mode == "jsil"))
+    {
+      symbol_list.push_back(symbol_pair.first);
+    }
   }
 
   for(const auto &id : symbol_list)
@@ -59,12 +59,14 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
 
   // this removes the parse tree of the bodies from memory
   #if 0
-  Forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair, symbol_table.symbols)
   {
-    if(!it->second.is_type &&
-       it->second.type.id()==ID_code &&
-       it->second.value.is_not_nil())
-      it->second.value=codet();
+    if(!symbol_pair.second.is_type &&
+       symbol_pair.second.type.id()==ID_code &&
+       symbol_pair.second.value.is_not_nil())
+    {
+      symbol_pair.second.value=codet();
+    }
   }
   #endif
 }

src/goto-programs/link_goto_model.cpp

@@ -110,13 +110,14 @@ static bool link_functions(
   // apply macros
   rename_symbolt macro_application;
 
-  forall_symbols(it, dest_symbol_table.symbols)
-    if(it->second.is_macro && !it->second.is_type)
+  for(const auto &symbol_pair : dest_symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
     {
-      const symbolt &symbol=it->second;
+      const symbolt &symbol = symbol_pair.second;
 
-      INVARIANT(symbol.value.id()==ID_symbol, "must have symbol");
-      const irep_idt &id=to_symbol_expr(symbol.value).get_identifier();
+      INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
+      const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
 
       #if 0
       if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
@@ -130,6 +131,7 @@ static bool link_functions(
 
       macro_application.insert_expr(symbol.name, id);
     }
+  }
 
   if(!macro_application.expr_map.empty())
     Forall_goto_functions(dest_it, dest_functions)
@@ -159,9 +161,11 @@ void link_goto_model(
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   id_sett weak_symbols;
 
-  forall_symbols(it, dest.symbol_table.symbols)
-    if(it->second.is_weak)
-      weak_symbols.insert(it->first);
+  for(const auto &symbol_pair : dest.symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_weak)
+      weak_symbols.insert(symbol_pair.first);
+  }
 
   linkingt linking(dest.symbol_table,
                    src.symbol_table,

src/goto-programs/show_symbol_table.cpp

@@ -30,8 +30,10 @@ void show_symbol_table_brief_plain(
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, symbol_table.symbols)
-    symbols.insert(id2string(it->first));
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    symbols.insert(id2string(symbol_pair.first));
+  }
 
   const namespacet ns(symbol_table);
 
@@ -68,8 +70,10 @@ void show_symbol_table_plain(
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, symbol_table.symbols)
-    symbols.insert(id2string(it->first));
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    symbols.insert(id2string(symbol_pair.first));
+  }
 
   const namespacet ns(symbol_table);
 

src/goto-programs/write_goto_binary.cpp

@@ -30,12 +30,12 @@ bool write_goto_binary_v3(
 
   write_gb_word(out, symbol_table.symbols.size());
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
     // Since version 2, symbols are not converted to ireps,
     // instead they are saved in a custom binary format
 
-    const symbolt &sym = it->second;
+    const symbolt &sym = symbol_pair.second;
 
     irepconverter.reference_convert(sym.type, out);
     irepconverter.reference_convert(sym.value, out);

src/goto-symex/symex_start_thread.cpp

@@ -97,9 +97,9 @@ void goto_symext::symex_start_thread(statet &state)
   // initialize all variables marked thread-local
   const symbol_tablet &symbol_table=ns.get_symbol_table();
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    const symbolt &symbol=it->second;
+    const symbolt &symbol = symbol_pair.second;
 
     if(!symbol.is_thread_local ||
        !symbol.is_static_lifetime ||