Merge pull request diffblue#186 from diffblue/cleanup/misc

Cleanup

Author: NathanJPhillips

cbmc/src/goto-analyzer/taint_analysis.cpp

@@ -272,8 +272,7 @@ bool taint_analysist::operator()(
       end.add_instruction(END_FUNCTION);
 
       forall_goto_functions(f_it, goto_functions)
-        if(f_it->second.body_available() &&
-           f_it->first!=goto_functionst::entry_point())
+        if(f_it->second.body_available())
         {
           goto_programt::targett t=calls.add_instruction();
           code_function_callt call;
@@ -284,14 +283,12 @@ bool taint_analysist::operator()(
           g->make_goto(t, side_effect_expr_nondett(bool_typet()));
         }
 
-      goto_functionst::goto_functiont &entry=
-        goto_functions.function_map[goto_functionst::entry_point()];
-
+      goto_functionst::goto_functiont entry;
       goto_programt &body=entry.body;
-
       body.destructive_append(gotos);
       body.destructive_append(calls);
       body.destructive_append(end);
+      goto_functions.function_map.emplace(goto_functionst::entry_point(), std::move(entry));
 
       goto_functions.update();
     }

cbmc/src/goto-instrument/thread_instrumentation.cpp

@@ -78,7 +78,7 @@ void thread_exit_instrumentation(goto_functionst &goto_functions)
   // now instrument
   for(const auto &fkt : thread_fkts)
   {
-    thread_exit_instrumentation(goto_functions.function_map[fkt].body);
+    thread_exit_instrumentation(goto_functions.function_map.at(fkt).body);
   }
 }
 

cbmc/src/goto-instrument/wmm/goto2graph.cpp

@@ -175,12 +175,12 @@ void instrumentert::cfg_visitort::visit_cfg_function(
 
 #ifdef LOCAL_MAY
   local_may_aliast local_may(
-    instrumenter.goto_functions.function_map[function]);
+    instrumenter.goto_functions.function_map.at(function));
 #endif
 
   /* goes through the function */
   Forall_goto_program_instructions(i_it,
-    instrumenter.goto_functions.function_map[function].body)
+    instrumenter.goto_functions.function_map.at(function).body)
   {
     goto_programt::instructiont &instruction=*i_it;
 
@@ -274,15 +274,15 @@ void instrumentert::cfg_visitort::visit_cfg_function(
   egraph.map_data_dp.insert(new_dp);
   data_dp.print(instrumenter.message);
 
-  if(instrumenter.goto_functions.function_map[function]
+  if(instrumenter.goto_functions.function_map.at(function)
      .body.instructions.empty())
   {
     /* empty set of ending edges */
   }
   else
   {
     goto_programt::instructionst::iterator it=instrumenter
-      .goto_functions.function_map[function].body.instructions.end();
+      .goto_functions.function_map.at(function).body.instructions.end();
     --it;
     ending_vertex=in_pos[it];
   }
@@ -319,7 +319,7 @@ void inline instrumentert::cfg_visitort::visit_cfg_reference_function(
 
   /* gets the body of the function */
   goto_programt::instructionst &body=instrumenter.goto_functions
-    .function_map[id_function].body.instructions;
+    .function_map.at(id_function).body.instructions;
 
   if(body.empty())
     return;
@@ -502,7 +502,7 @@ void inline instrumentert::cfg_visitort::visit_cfg_duplicate(
 {
   instrumenter.message.status() << "Duplication..." << messaget::eom;
   const goto_functionst::goto_functiont &fun=
-    instrumenter.goto_functions.function_map[i_it->function];
+    instrumenter.goto_functions.function_map.at(i_it->function);
 
   bool found_pos=false;
   goto_programt::const_targett new_targ=targ;
@@ -1300,15 +1300,12 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
     }
 
   /* now test whether this part of the code can exist */
-  goto_functionst::function_mapt map;
+  goto_functionst this_interleaving;
   goto_function_templatet<goto_programt> one_interleaving;
   one_interleaving.body.copy_from(interleaving);
-  map.insert(std::make_pair(
+  this_interleaving.function_map.insert(std::make_pair(
     goto_functionst::entry_point(),
     std::move(one_interleaving)));
-
-  goto_functionst this_interleaving;
-  this_interleaving.function_map=std::move(map);
   optionst no_option;
   null_message_handlert no_message;
 

cbmc/src/goto-instrument/wmm/shared_buffers.cpp

@@ -1058,7 +1058,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
     return;
 
   namespacet ns(symbol_table);
-  goto_programt &goto_program=goto_functions.function_map[function].body;
+  goto_programt &goto_program=goto_functions.function_map.at(function).body;
 
 #ifdef LOCAL_MAY
   local_may_aliast local_may(goto_functions.function_map[function]);

cbmc/src/goto-programs/goto_functions_template.h

@@ -185,42 +185,29 @@ template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_location_numbers()
 {
   unsigned nr=0;
-
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_location_numbers(nr);
+  for(auto &named_function : function_map)
+    named_function.second.body.compute_location_numbers(nr);
 }
 
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_incoming_edges()
 {
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_incoming_edges();
+  for(auto &named_function : function_map)
+    named_function.second.body.compute_incoming_edges();
 }
 
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_target_numbers()
 {
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_target_numbers();
+  for(auto &named_function : function_map)
+    named_function.second.body.compute_target_numbers();
 }
 
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_loop_numbers()
 {
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_loop_numbers();
+  for(auto &named_function : function_map)
+    named_function.second.body.compute_loop_numbers();
 }
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H

cbmc/src/goto-programs/read_goto_binary.cpp

@@ -255,22 +255,17 @@ static bool link_functions(
     goto_functionst::function_mapt::iterator dest_f_it=
       dest_functions.function_map.find(final_id);
 
+    goto_functionst::goto_functiont &src_func=src_it->second;
     if(dest_f_it==dest_functions.function_map.end()) // not there yet
     {
-      rename_symbols_in_function(src_it->second, rename_symbol);
-
-      goto_functionst::goto_functiont &in_dest_symbol_table=
-        dest_functions.function_map[final_id];
-
-      in_dest_symbol_table.body.swap(src_it->second.body);
-      in_dest_symbol_table.type=src_it->second.type;
+      rename_symbols_in_function(src_func, rename_symbol);
+      dest_functions.function_map.insert(
+        std::make_pair(final_id, std::move(src_func)));
     }
     else // collision!
     {
       goto_functionst::goto_functiont &in_dest_symbol_table=
-        dest_functions.function_map[final_id];
-
-      goto_functionst::goto_functiont &src_func=src_it->second;
+        dest_f_it->second;
 
       if(in_dest_symbol_table.body.instructions.empty() ||
          weak_symbols.find(final_id)!=weak_symbols.end())

cbmc/src/util/symbol_table.cpp

@@ -45,23 +45,23 @@ bool symbol_tablet::add(const symbolt &symbol)
 ///   location in the symbol table
 bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
 {
-  symbolt tmp;
-
+  // Add an empty symbol to the table or retrieve existing symbol with same name
   std::pair<symbolst::iterator, bool> result=
-    symbols.insert(std::pair<irep_idt, symbolt>(symbol.name, tmp));
+    symbols.emplace(symbol.name, symbolt());
 
   if(!result.second)
   {
+    // Return the address of the symbol that already existed in the table
     new_symbol=&result.first->second;
     return true;
   }
 
-  symbol_base_map.insert(
-    std::pair<irep_idt, irep_idt>(symbol.base_name, symbol.name));
-  symbol_module_map.insert(
-    std::pair<irep_idt, irep_idt>(symbol.module, symbol.name));
+  symbol_base_map.emplace(symbol.base_name, symbol.name);
+  symbol_module_map.emplace(symbol.module, symbol.name);
 
+  // Move the provided symbol into the symbol table
   result.first->second.swap(symbol);
+  // Return the address of the new symbol in the table
   new_symbol=&result.first->second;
 
   return false;