Avoid shadowing of variables (several instances) [blocks: #2310]

src/goto-cc/linker_script_merge.cpp

@@ -480,11 +480,13 @@ int linker_script_merget::ls_data2instructions(
       symbol_exprt end_sym(d["end-symbol"].value, pointer_type(char_type()));
       linker_values[d["end-symbol"].value]=std::make_pair(end_sym, array_end);
 
-      auto it=std::find_if(data["addresses"].array.begin(),
-                           data["addresses"].array.end(),
-                           [&d](const jsont &add)
-                           { return add["sym"].value==d["end-symbol"].value; });
-      if(it==data["addresses"].array.end())
+      auto entry = std::find_if(
+        data["addresses"].array.begin(),
+        data["addresses"].array.end(),
+        [&d](const jsont &add) {
+          return add["sym"].value == d["end-symbol"].value;
+        });
+      if(entry == data["addresses"].array.end())
       {
         error() << "Could not find address corresponding to symbol '"
                 << d["end-symbol"].value << "' (end of section)" << eom;
@@ -493,9 +495,9 @@ int linker_script_merget::ls_data2instructions(
       source_locationt  end_loc;
       end_loc.set_file(linker_script);
       std::ostringstream end_comment;
-      end_comment << "Pointer to end of object section '"
-                  << d["section"].value << "'. Original address in object file"
-                  << " is " << (*it)["val"].value;
+      end_comment << "Pointer to end of object section '" << d["section"].value
+                  << "'. Original address in object file"
+                  << " is " << (*entry)["val"].value;
       end_loc.set_comment(end_comment.str());
       end_sym.add_source_location()=end_loc;
 

src/goto-instrument/accelerate/accelerate.cpp

@@ -183,15 +183,18 @@ void acceleratet::insert_accelerator(
   goto_programt::targett &loop_header,
   goto_programt::targett &back_jump,
   path_acceleratort &accelerator,
-  subsumed_patht &subsumed)
+  subsumed_patht &subsumed_path)
 {
   insert_looping_path(
-    loop_header, back_jump, accelerator.pure_accelerator, subsumed.accelerator);
+    loop_header,
+    back_jump,
+    accelerator.pure_accelerator,
+    subsumed_path.accelerator);
 
   if(!accelerator.overflow_path.instructions.empty())
   {
     insert_looping_path(
-      loop_header, back_jump, accelerator.overflow_path, subsumed.residue);
+      loop_header, back_jump, accelerator.overflow_path, subsumed_path.residue);
   }
 }
 

src/goto-instrument/accelerate/accelerate.h

@@ -84,7 +84,7 @@ class acceleratet
     goto_programt::targett &loop_header,
     goto_programt::targett &back_jump,
     path_acceleratort &accelerator,
-    subsumed_patht &subsumed);
+    subsumed_patht &subsumed_path);
 
   void set_dirty_vars(path_acceleratort &accelerator);
   void add_dirty_checks();

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -556,7 +556,6 @@ acceleration_utilst::expr_pairst acceleration_utilst::gather_array_assignments(
 bool acceleration_utilst::do_arrays(
   goto_programt::instructionst &loop_body,
   std::map<exprt, polynomialt> &polynomials,
-  exprt &loop_counter,
   substitutiont &substitution,
   scratch_programt &program)
 {
@@ -881,7 +880,6 @@ bool acceleration_utilst::expr2poly(
 bool acceleration_utilst::do_nonrecursive(
   goto_programt::instructionst &body,
   std::map<exprt, polynomialt> &polynomials,
-  exprt &loop_counter,
   substitutiont &substitution,
   expr_sett &nonrecursive,
   scratch_programt &program)
@@ -1004,7 +1002,7 @@ bool acceleration_utilst::do_nonrecursive(
     const exprt &lhs=*it;
     const exprt &rhs=state[*it];
 
-    if(!assign_array(lhs, rhs, loop_counter, program))
+    if(!assign_array(lhs, rhs, program))
     {
 #ifdef DEBUG
       std::cout << "Failed to assign a nonrecursive array: " <<
@@ -1020,7 +1018,6 @@ bool acceleration_utilst::do_nonrecursive(
 bool acceleration_utilst::assign_array(
   const exprt &lhs,
   const exprt &rhs,
-  const exprt &loop_counter,
   scratch_programt &program)
 {
 #ifdef DEBUG
@@ -1245,12 +1242,8 @@ void acceleration_utilst::extract_polynomial(
       continue;
     }
 
-    for(expr_listt::iterator it=terms.begin();
-        it!=terms.end();
-        ++it)
+    for(const auto &term : terms)
     {
-      exprt term=*it;
-
       if(degrees.find(term)!=degrees.end())
       {
         degrees[term]++;

src/goto-instrument/accelerate/acceleration_utils.h

@@ -101,7 +101,6 @@ class acceleration_utilst
 
   bool do_arrays(goto_programt::instructionst &loop_body,
                  std::map<exprt, polynomialt> &polynomials,
-                 exprt &loop_counter,
                  substitutiont &substitution,
                  scratch_programt &program);
   expr_pairst gather_array_assignments(
@@ -120,14 +119,12 @@ class acceleration_utilst
   bool do_nonrecursive(
     goto_programt::instructionst &loop_body,
     std::map<exprt, polynomialt> &polynomials,
-    exprt &loop_counter,
     substitutiont &substitution,
     expr_sett &nonrecursive,
     scratch_programt &program);
   bool assign_array(
     const exprt &lhs,
     const exprt &rhs,
-    const exprt &loop_counter,
     scratch_programt &program);
 
   void gather_array_accesses(const exprt &expr, expr_sett &arrays);
@@ -157,8 +154,6 @@ class acceleration_utilst
   const goto_functionst &goto_functions;
   exprt &loop_counter;
   nil_exprt nil;
-
-  static int num_symbols;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -315,7 +315,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   }
 
   // Add in any array assignments we can do now.
-  if(!utils.do_arrays(assigns, polynomials, loop_counter, stashed, program))
+  if(!utils.do_arrays(assigns, polynomials, stashed, program))
   {
     // We couldn't model some of the array assignments with polynomials...
     // Unfortunately that means we just have to bail out.

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -251,7 +251,7 @@ bool polynomial_acceleratort::accelerate(
 
   // Add in any array assignments we can do now.
   if(!utils.do_nonrecursive(
-      assigns, polynomials, loop_counter, stashed, nonrecursive, program))
+       assigns, polynomials, stashed, nonrecursive, program))
   {
     // We couldn't model some of the array assignments with polynomials...
     // Unfortunately that means we just have to bail out.

src/goto-instrument/accelerate/polynomial_accelerator.h

@@ -133,7 +133,6 @@ class polynomial_acceleratort
   bool do_arrays(
     goto_programt::instructionst &loop_body,
     std::map<exprt, polynomialt> &polynomials,
-    exprt &loop_counter,
     substitutiont &substitution,
     scratch_programt &program);
   expr_pairst gather_array_assignments(

src/goto-instrument/concurrency.cpp

@@ -130,8 +130,8 @@ void concurrency_instrumentationt::instrument(
       instrument(code.function());
 
       // instrument(code.lhs(), LHS);
-      Forall_expr(it, code.arguments())
-        instrument(*it);
+      for(auto &arg : code.arguments())
+        instrument(arg);
     }
   }
 }

src/goto-instrument/document_properties.cpp

@@ -155,9 +155,9 @@ void document_propertiest::get_code(
   dest="";
 
   const irep_idt &file=source_location.get_file();
-  const irep_idt &line=source_location.get_line();
+  const irep_idt &source_line = source_location.get_line();
 
-  if(file=="" || line=="")
+  if(file == "" || source_line == "")
     return;
 
   std::ifstream in(id2string(file));
@@ -170,7 +170,7 @@ void document_propertiest::get_code(
     return;
   }
 
-  int line_int=unsafe_string2int(id2string(line));
+  int line_int = unsafe_string2int(id2string(source_line));
 
   int line_start=line_int-3,
       line_end=line_int+3;

src/goto-instrument/dot.cpp

@@ -264,8 +264,6 @@ void dott::output(std::ostream &out)
   out << "digraph G {\n";
   out << DOTGRAPHSETTINGS << '\n';
 
-  std::list<exprt> clusters;
-
   forall_goto_functions(it, goto_model.goto_functions)
     if(it->second.body_available())
       write_dot_subgraph(out, id2string(it->first), it->second.body);

src/goto-instrument/nondet_static.cpp

@@ -73,11 +73,11 @@ void nondet_static(
   goto_functionst &goto_functions,
   const irep_idt &fct_name)
 {
-  goto_functionst::function_mapt::iterator
-    i_it=goto_functions.function_map.find(fct_name);
-  assert(i_it!=goto_functions.function_map.end());
+  goto_functionst::function_mapt::iterator fct_entry =
+    goto_functions.function_map.find(fct_name);
+  CHECK_RETURN(fct_entry != goto_functions.function_map.end());
 
-  goto_programt &init=i_it->second.body;
+  goto_programt &init = fct_entry->second.body;
 
   Forall_goto_program_instructions(i_it, init)
   {

src/goto-instrument/thread_instrumentation.cpp

@@ -120,14 +120,14 @@ void mutex_init_instrumentation(goto_modelt &goto_model)
 {
   // get pthread_mutex_lock
 
-  symbol_tablet::symbolst::const_iterator f_it=
+  symbol_tablet::symbolst::const_iterator lock_entry =
     goto_model.symbol_table.symbols.find("pthread_mutex_lock");
 
-  if(f_it==goto_model.symbol_table.symbols.end())
+  if(lock_entry == goto_model.symbol_table.symbols.end())
     return;
 
   // get type of lock argument
-  code_typet code_type=to_code_type(to_code_type(f_it->second.type));
+  code_typet code_type = to_code_type(to_code_type(lock_entry->second.type));
   if(code_type.parameters().size()!=1)
     return;
 

src/goto-instrument/unwind.cpp

@@ -55,9 +55,10 @@ void goto_unwindt::copy_segment(
   assert(goto_program.instructions.size()==target_vector.size());
 
   // adjust intra-segment gotos
-  for(std::size_t i=0; i<target_vector.size(); i++)
+  for(std::size_t target_index = 0; target_index < target_vector.size();
+      target_index++)
   {
-    goto_programt::targett t=target_vector[i];
+    goto_programt::targett t = target_vector[target_index];
 
     if(!t->is_goto())
       continue;

src/goto-instrument/wmm/goto2graph.cpp

@@ -210,9 +210,13 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     /* a:=b -o-> Rb -po-> Wa */
     else if(instruction.is_assign())
     {
-      visit_cfg_assign(value_sets, ns, i_it, no_dependencies
+      visit_cfg_assign(
+        value_sets,
+        i_it,
+        no_dependencies
 #ifdef LOCAL_MAY
-        , local_may
+        ,
+        local_may
 #endif
       ); // NOLINT(whitespace/parens)
     }
@@ -783,7 +787,6 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence(
 
 void instrumentert::cfg_visitort::visit_cfg_assign(
   value_setst &value_sets,
-  namespacet &ns,
   goto_programt::instructionst::iterator &i_it,
   bool no_dependencies
 #ifdef LOCAL_MAY

src/goto-instrument/wmm/goto2graph.h

@@ -125,11 +125,14 @@ class instrumentert
       goto_programt::const_targett i_it);
     void inline visit_cfg_duplicate(goto_programt::const_targett targ,
       goto_programt::const_targett i_it);
-    void visit_cfg_assign(value_setst &value_sets, namespacet &ns,
-      goto_programt::instructionst::iterator &i_it, bool no_dependencies
-      #ifdef LOCAL_MAY
-      , local_may_aliast &local_may
-      #endif
+    void visit_cfg_assign(
+      value_setst &value_sets,
+      goto_programt::instructionst::iterator &i_it,
+      bool no_dependencies
+#ifdef LOCAL_MAY
+      ,
+      local_may_aliast &local_may
+#endif
     ); // NOLINT(whitespace/parens)
     void visit_cfg_fence(goto_programt::instructionst::iterator i_it);
     void visit_cfg_skip(goto_programt::instructionst::iterator i_it);