Merge pull request #3415 from tautschnig/vs-shadow-1

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

Author: Daniel Kroening

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;