Merge pull request #3607 from tautschnig/vs-shadow

Avoid shadowing of variables [blocks: #2310]

Author: tautschnig

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -191,8 +191,7 @@ SCENARIO("instantiate_not_contains",
 
     // Generating the corresponding axioms and simplifying, recording info
     string_constraint_generatort generator(empty_ns);
-    const auto pair = generator.add_axioms_for_function_application(
-      generator.fresh_symbol, func);
+    const auto pair = generator.add_axioms_for_function_application(func);
     const string_constraintst &constraints = pair.second;
 
     std::string axioms;

src/solvers/refinement/refine_arrays.cpp

@@ -119,9 +119,9 @@ void bv_refinementt::freeze_lazy_constraints()
 
   for(const auto &constraint : lazy_array_constraints)
   {
-    std::set<symbol_exprt> symbols;
-    find_symbols(constraint.lazy, symbols);
-    for(const auto &symbol : symbols)
+    std::set<symbol_exprt> symbols_in_constraint;
+    find_symbols(constraint.lazy, symbols_in_constraint);
+    for(const auto &symbol : symbols_in_constraint)
     {
       const bvt bv=convert_bv(symbol);
       forall_literals(b_it, bv)

src/solvers/refinement/string_builtin_function.cpp

@@ -129,12 +129,12 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
       ? std::max(std::min(args_value[1], input2_size), start_index)
       : input2_size;
 
-  std::vector<mp_integer> result(input1_value);
-  result.insert(
-    result.end(),
+  std::vector<mp_integer> eval_result(input1_value);
+  eval_result.insert(
+    eval_result.end(),
     input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
     input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
-  return result;
+  return eval_result;
 }
 
 string_constraintst string_concatenation_builtin_functiont::constraints(
@@ -458,12 +458,12 @@ std::vector<mp_integer> string_insertion_builtin_functiont::eval(
       ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
       : input2_size;
 
-  std::vector<mp_integer> result(input1_value);
-  result.insert(
-    result.begin() + numeric_cast_v<std::size_t>(offset),
+  std::vector<mp_integer> eval_result(input1_value);
+  eval_result.insert(
+    eval_result.begin() + numeric_cast_v<std::size_t>(offset),
     input2_value.begin() + numeric_cast_v<std::size_t>(start),
     input2_value.begin() + numeric_cast_v<std::size_t>(end));
-  return result;
+  return eval_result;
 }
 
 optionalt<exprt> string_insertion_builtin_functiont::eval(
@@ -634,8 +634,8 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
 string_constraintst string_builtin_function_with_no_evalt::constraints(
   string_constraint_generatort &generator) const
 {
-  auto pair = generator.add_axioms_for_function_application(
-    generator.fresh_symbol, function_application);
+  auto pair =
+    generator.add_axioms_for_function_application(function_application);
   pair.second.existential.push_back(equal_exprt(pair.first, return_code));
   return pair.second;
 }

src/solvers/refinement/string_constraint_generator.h

@@ -127,7 +127,6 @@ class string_constraint_generatort final
   explicit string_constraint_generatort(const namespacet &ns);
 
   std::pair<exprt, string_constraintst> add_axioms_for_function_application(
-    symbol_generatort &fresh_symbol,
     const function_application_exprt &expr);
 
   symbol_generatort fresh_symbol;
@@ -150,7 +149,6 @@ class string_constraint_generatort final
   /// string pointers.
   /// \deprecated Not tested.
   std::pair<symbol_exprt, string_constraintst> add_axioms_for_intern(
-    symbol_generatort &fresh_symbol,
     const function_application_exprt &f);
 
   exprt associate_array_to_pointer(const function_application_exprt &f);
@@ -161,7 +159,6 @@ class string_constraint_generatort final
   // The specification is partial: the actual value is not actually computed
   // but we ensure that hash codes of equal strings are equal.
   std::pair<exprt, string_constraintst> add_axioms_for_hash_code(
-    symbol_generatort &fresh_symbol,
     const function_application_exprt &f,
     array_poolt &pool);
 

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -182,18 +182,16 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
 /// These axioms are, for each string `s` on which hash was called:
 ///   * \f$ hash(str)=hash(s) \lor |str| \ne |s|
 ///       \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with argument refined_string `str`
 /// \param pool: pool of arrays representing strings
 /// \return integer expression `hash(str)`
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_hash_code(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
   array_poolt &pool)
 {
   PRECONDITION(f.arguments().size() == 1);
-  string_constraintst constraints;
+  string_constraintst hash_constraints;
   const array_string_exprt str = get_string_expr(pool, f.arguments()[0]);
   const typet &return_type = f.type();
   const typet &index_type = str.length().type();
@@ -212,9 +210,9 @@ string_constraint_generatort::add_axioms_for_hash_code(
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
         and_exprt(length_gt(str, i), is_positive(i))));
-    constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
+    hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
-  return {hash, std::move(constraints)};
+  return {hash, std::move(hash_constraints)};
 }
 
 /// Lexicographic comparison of two strings
@@ -302,17 +300,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
 /// Add axioms stating that the return value for two equal string should be the
 /// same
 /// \deprecated never tested
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with one string argument
 /// \return a string expression
 DEPRECATED("never tested")
 std::pair<symbol_exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_intern(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 1);
-  string_constraintst constraints;
+  string_constraintst intern_constraints;
   const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
   // For now we only enforce content equality and not pointer equality
   const typet &return_type=f.type();
@@ -330,14 +326,14 @@ string_constraint_generatort::add_axioms_for_intern(
   exprt::operandst disj;
   for(auto it : intern_of_string)
     disj.push_back(equal_exprt(intern, it.second));
-  constraints.existential.push_back(disjunction(disj));
+  intern_constraints.existential.push_back(disjunction(disj));
 
   // WARNING: the specification may be incomplete or incorrect
   for(auto it : intern_of_string)
     if(it.second!=str)
     {
       symbol_exprt i = fresh_symbol("index_intern", index_type);
-      constraints.existential.push_back(or_exprt(
+      intern_constraints.existential.push_back(or_exprt(
         equal_exprt(it.second, intern),
         or_exprt(
           notequal_exprt(str.length(), it.first.length()),
@@ -348,5 +344,5 @@ string_constraint_generatort::add_axioms_for_intern(
               and_exprt(length_gt(str, i), is_positive(i)))))));
     }
 
-  return {intern, std::move(constraints)};
+  return {intern, std::move(intern_constraints)};
 }

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -337,14 +337,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
 /// \todo For now we only consider single precision.
 /// \param fresh_symbol: generator of fresh symbols
 /// \param res: string expression representing the float in scientific notation
-/// \param f: a float expression, which is positive
+/// \param float_expr: a float expression, which is positive
 /// \param array_pool: pool of arrays representing strings
 /// \param ns: namespace
 /// \return a integer expression different from 0 to signal an exception
 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
-  const exprt &f,
+  const exprt &float_expr,
   array_poolt &array_pool,
   const namespacet &ns)
 {
@@ -359,13 +359,13 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type);
 
   // `bin_exponent` is $e$ in the formulas
-  exprt bin_exponent=get_exponent(f, float_spec);
+  exprt bin_exponent = get_exponent(float_expr, float_spec);
 
   // $m$ from the formula is a value between 0.0 and 2.0 represented
   // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
   // `bin_significand_int` represents $m * 0x800000$
-  exprt bin_significand_int=
-    get_significand(f, float_spec, unsignedbv_typet(32));
+  exprt bin_significand_int =
+    get_significand(float_expr, float_spec, unsignedbv_typet(32));
   // `bin_significand` represents $m$ and is obtained
   // by multiplying `binary_significand_as_int` by
   // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
@@ -375,7 +375,8 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
 
   // This is a first approximation of the exponent that will adjust
   // if the fraction we get is greater than 10
-  exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec);
+  exprt dec_exponent_estimate =
+    estimate_decimal_exponent(float_expr, float_spec);
 
   // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
   std::vector<double> two_power_e_over_ten_power_d_table(
@@ -422,10 +423,12 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
     int_type);
   array_exprt conversion_factor_table(
     array_typet(float_type, conversion_factor_table_size));
-  for(const auto &f : two_power_e_over_ten_power_d_table_negatives)
-    conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
-  for(const auto &f : two_power_e_over_ten_power_d_table)
-    conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
+  for(const auto &negative : two_power_e_over_ten_power_d_table_negatives)
+    conversion_factor_table.copy_to_operands(
+      constant_float(negative, float_spec));
+  for(const auto &positive : two_power_e_over_ten_power_d_table)
+    conversion_factor_table.copy_to_operands(
+      constant_float(positive, float_spec));
 
   // The index in the table, corresponding to exponent e is e+128
   plus_exprt shifted_index(bin_exponent, from_integer(128, int_type));
@@ -460,7 +463,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   minus_exprt fractional_part(
     dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
 
-  // shifted_float is floor(f * 1e5)
+  // shifted_float is floor(float_expr * 1e5)
   exprt shifting=constant_float(1e5, float_spec);
   exprt shifted_float=
     round_expr_to_zero(floatbv_mult(fractional_part, shifting));
@@ -469,7 +472,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   // the exponent notation.
   exprt max_non_exponent_notation=from_integer(100000, shifted_float.type());
 
-  // fractional_part_shifted is floor(f * 100000) % 100000
+  // fractional_part_shifted is floor(float_expr * 100000) % 100000
   const mod_exprt fractional_part_shifted(
     shifted_float, max_non_exponent_notation);
 

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -363,12 +363,10 @@ optionalt<exprt> string_constraint_generatort::make_array_pointer_association(
 /// strings contained in this call are converted to objects of type
 /// `string_exprt`, through adding axioms. Axioms are then added to enforce that
 /// the result corresponds to the function application.
-/// \param fresh_symbol: generator of fresh symbols
 /// \param expr: an expression containing a function application
 /// \return expression corresponding to the result of the function application
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_function_application(
-  symbol_generatort &fresh_symbol,
   const function_application_exprt &expr)
 {
   const irep_idt &id = get_function_name(expr);
@@ -396,7 +394,7 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id==ID_cprover_string_contains_func)
     return add_axioms_for_contains(fresh_symbol, expr, array_pool);
   else if(id==ID_cprover_string_hash_code_func)
-    return add_axioms_for_hash_code(fresh_symbol, expr, array_pool);
+    return add_axioms_for_hash_code(expr, array_pool);
   else if(id==ID_cprover_string_index_of_func)
     return add_axioms_for_index_of(fresh_symbol, expr, array_pool);
   else if(id==ID_cprover_string_last_index_of_func)
@@ -463,7 +461,7 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id==ID_cprover_string_replace_func)
     return add_axioms_for_replace(fresh_symbol, expr, array_pool);
   else if(id==ID_cprover_string_intern_func)
-    return add_axioms_for_intern(fresh_symbol, expr);
+    return add_axioms_for_intern(expr);
   else if(id==ID_cprover_string_format_func)
     return add_axioms_for_format(fresh_symbol, expr, array_pool, message, ns);
   else if(id == ID_cprover_string_constrain_characters_func)

src/solvers/refinement/string_refinement.cpp

@@ -738,8 +738,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   // Initial try without index set
   const auto get = [this](const exprt &expr) { return this->get(expr); };
   dependencies.clean_cache();
-  const decision_proceduret::resultt res=supert::dec_solve();
-  if(res==resultt::D_SATISFIABLE)
+  const decision_proceduret::resultt initial_result = supert::dec_solve();
+  if(initial_result == resultt::D_SATISFIABLE)
   {
     bool satisfied;
     std::vector<exprt> counter_examples;
@@ -762,23 +762,23 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   else
   {
     debug() << "check_SAT: got UNSAT or ERROR" << eom;
-    return res;
+    return initial_result;
   }
 
   initial_index_set(index_sets, ns, axioms);
   update_index_set(index_sets, ns, current_constraints);
   current_constraints.clear();
-  const auto instances =
+  const auto initial_instances =
     generate_instantiations(index_sets, axioms, not_contain_witnesses);
-  for(const auto &instance : instances)
+  for(const auto &instance : initial_instances)
     add_lemma(instance);
 
   while((loop_bound_--)>0)
   {
     dependencies.clean_cache();
-    const decision_proceduret::resultt res=supert::dec_solve();
+    const decision_proceduret::resultt refined_result = supert::dec_solve();
 
-    if(res==resultt::D_SATISFIABLE)
+    if(refined_result == resultt::D_SATISFIABLE)
     {
       bool satisfied;
       std::vector<exprt> counter_examples;
@@ -833,8 +833,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     }
     else
     {
-      debug() << "check_SAT: default return " << static_cast<int>(res) << eom;
-      return res;
+      debug() << "check_SAT: default return "
+              << static_cast<int>(refined_result) << eom;
+      return refined_result;
     }
   }
   debug() << "string_refinementt::dec_solve reached the maximum number"