Clang whitespace changes

Author: JohnDumbell

src/solvers/strings/string_builtin_function.cpp

@@ -426,8 +426,8 @@ string_constraintst string_insertion_builtin_functiont::constraints(
 {
   if(args.size() == 1)
   {
-    auto pair = generator.add_axioms_for_insert(
-      result, input1, input2, args[0]);
+    auto pair =
+      generator.add_axioms_for_insert(result, input1, input2, args[0]);
     pair.second.existential.push_back(equal_exprt(pair.first, return_code));
     return pair.second;
   }
@@ -497,8 +497,8 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
 string_constraintst string_of_int_builtin_functiont::constraints(
   string_constraint_generatort &generator) const
 {
-  auto pair = generator.add_axioms_for_string_of_int_with_radix(
-    result, arg, radix, 0);
+  auto pair =
+    generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0);
   pair.second.existential.push_back(equal_exprt(pair.first, return_code));
   return pair.second;
 }

src/solvers/strings/string_builtin_function.h

@@ -394,7 +394,6 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   }
 };
 
-
 /// String creation from other types
 class string_creation_builtin_functiont : public string_builtin_functiont
 {

src/solvers/strings/string_concatenation_builtin_function.cpp

@@ -162,11 +162,7 @@ string_constraint_generatort::add_axioms_for_concat(
 {
   exprt index_zero = from_integer(0, s2.length_type());
   return add_axioms_for_concat_substr(
-    res,
-    s1,
-    s2,
-    index_zero,
-    array_pool.get_or_create_length(s2));
+    res, s1, s2, index_zero, array_pool.get_or_create_length(s2));
 }
 
 /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function
@@ -217,16 +213,11 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
 {
   auto pair = [&]() -> std::pair<exprt, string_constraintst> {
     if(args.size() == 0)
-      return generator.add_axioms_for_concat(
-        result, input1, input2);
+      return generator.add_axioms_for_concat(result, input1, input2);
     if(args.size() == 2)
     {
       return generator.add_axioms_for_concat_substr(
-        result,
-        input1,
-        input2,
-        args[0],
-        args[1]);
+        result, input1, input2, args[0], args[1]);
     }
     UNREACHABLE;
   }();

src/solvers/strings/string_constraint_generator_constants.cpp

@@ -94,8 +94,7 @@ string_constraint_generatort::add_axioms_for_cprover_string(
       add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false));
   }
   else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
-    return add_axioms_for_constant(
-      res, constant_expr->get_value(), guard);
+    return add_axioms_for_constant(res, constant_expr->get_value(), guard);
   else
     return {from_integer(1, get_return_code_type()), {}};
 }

src/solvers/strings/string_constraint_generator_float.cpp

@@ -207,8 +207,8 @@ string_constraint_generatort::add_axioms_for_string_of_float(
   const mod_exprt fractional_part(shifted, max_non_exponent_notation);
   const array_string_exprt fractional_part_str =
     array_pool.fresh_string(index_type, char_type);
-  auto result1 = add_axioms_for_fractional_part(
-    fractional_part_str, fractional_part, 6);
+  auto result1 =
+    add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
 
   // The axiom added to convert to integer should always be satisfiable even
   // when the preconditions are not satisfied.
@@ -218,11 +218,11 @@ string_constraint_generatort::add_axioms_for_string_of_float(
   // part of the float.
   const array_string_exprt integer_part_str =
     array_pool.fresh_string(index_type, char_type);
-  auto result2 = add_axioms_for_string_of_int(
-    integer_part_str, integer_part, 8);
+  auto result2 =
+    add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
 
-  auto result3 = add_axioms_for_concat(
-    res, integer_part_str, fractional_part_str);
+  auto result3 =
+    add_axioms_for_concat(res, integer_part_str, fractional_part_str);
   merge(result3.second, std::move(result1.second));
   merge(result3.second, std::move(result2.second));
 
@@ -485,19 +485,17 @@ string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const array_string_exprt string_expr_with_E =
     array_pool.fresh_string(index_type, char_type);
   auto result5 = add_axioms_for_concat(
-    string_expr_with_E,
-    string_expr_with_fractional_part,
-    stringE);
+    string_expr_with_E, string_expr_with_fractional_part, stringE);
 
   // exponent_string = string_of_int(decimal_exponent)
   const array_string_exprt exponent_string =
     array_pool.fresh_string(index_type, char_type);
-  auto result6 = add_axioms_for_string_of_int(
-    exponent_string, decimal_exponent, 3);
+  auto result6 =
+    add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
 
   // string_expr = concat(string_expr_with_E, exponent_string)
-  auto result7 = add_axioms_for_concat(
-    res, string_expr_with_E, exponent_string);
+  auto result7 =
+    add_axioms_for_concat(res, string_expr_with_E, exponent_string);
 
   const exprt return_code = maximum(
     result1.first,
@@ -531,6 +529,5 @@ string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &arg = f.arguments()[2];
-  return add_axioms_from_float_scientific_notation(
-    res, arg);
+  return add_axioms_from_float_scientific_notation(res, arg);
 }

src/solvers/strings/string_constraint_generator_indexof.cpp

@@ -325,8 +325,7 @@ string_constraint_generatort::add_axioms_for_index_of(
         "c can only be a (un)signedbv or a refined "
         "string and the (un)signedbv case is already handled"));
     array_string_exprt sub = get_string_expr(array_pool, c);
-    return add_axioms_for_index_of_string(
-      str, sub, from_index);
+    return add_axioms_for_index_of_string(str, sub, from_index);
   }
 }
 
@@ -444,7 +443,6 @@ string_constraint_generatort::add_axioms_for_last_index_of(
   else
   {
     const array_string_exprt sub = get_string_expr(array_pool, c);
-    return add_axioms_for_last_index_of_string(
-      str, sub, from_index);
+    return add_axioms_for_last_index_of_string(str, sub, from_index);
   }
 }

src/solvers/strings/string_constraint_generator_insert.cpp

@@ -126,10 +126,8 @@ string_constraint_generatort::add_axioms_for_insert(
     const array_string_exprt substring =
       array_pool.fresh_string(index_type, char_type);
     return combine_results(
-      add_axioms_for_substring(
-        substring, s2, start, end),
-      add_axioms_for_insert(
-        res, s1, substring, offset));
+      add_axioms_for_substring(substring, s2, start, end),
+      add_axioms_for_insert(res, s1, substring, offset));
   }
   else // 5 arguments
   {
@@ -224,8 +222,7 @@ string_constraint_generatort::add_axioms_for_insert_double(
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
-    add_axioms_for_string_of_float(
-      s2, f.arguments()[4]),
+    add_axioms_for_string_of_float(s2, f.arguments()[4]),
     add_axioms_for_insert(res, s1, s2, offset));
 }
 

src/solvers/strings/string_constraint_generator_main.cpp

@@ -172,8 +172,8 @@ string_constraint_generatort::add_axioms_for_constrain_characters(
     args.size() >= 4 ? args[3] : from_integer(0, s.length_type());
   const exprt &end =
     args.size() >= 5 ? args[4] : array_pool.get_or_create_length(s);
-  auto constraints = add_constraint_on_characters(
-    s, start, end, char_set_string.c_str());
+  auto constraints =
+    add_constraint_on_characters(s, start, end, char_set_string.c_str());
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }
 
@@ -262,7 +262,7 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id == ID_cprover_string_insert_long_func)
     return add_axioms_for_insert_int(expr);
   else if(id == ID_cprover_string_insert_bool_func)
-    return add_axioms_for_insert_bool( expr);
+    return add_axioms_for_insert_bool(expr);
   else if(id == ID_cprover_string_insert_char_func)
     return add_axioms_for_insert_char(expr);
   else if(id == ID_cprover_string_insert_double_func)
@@ -282,8 +282,7 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id == ID_cprover_string_of_float_func)
     return add_axioms_for_string_of_float(expr);
   else if(id == ID_cprover_string_of_float_scientific_notation_func)
-    return add_axioms_from_float_scientific_notation(
-      expr);
+    return add_axioms_from_float_scientific_notation(expr);
   else if(id == ID_cprover_string_of_double_func)
     return add_axioms_from_double(expr);
   else if(id == ID_cprover_string_of_long_func)
@@ -331,8 +330,7 @@ string_constraint_generatort::add_axioms_for_copy(
   const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
   const exprt count =
     args.size() == 3 ? array_pool.get_or_create_length(str) : args[4];
-  return add_axioms_for_substring(
-    res, str, offset, plus_exprt(offset, count));
+  return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count));
 }
 
 /// Length of a string

src/solvers/strings/string_constraint_generator_testing.cpp

@@ -115,8 +115,7 @@ string_constraint_generatort::add_axioms_for_is_prefix(
     get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
   const exprt offset =
     args.size() == 2 ? from_integer(0, s0.length_type()) : args[2];
-  auto pair =
-    add_axioms_for_is_prefix(s0, s1, offset);
+  auto pair = add_axioms_for_is_prefix(s0, s1, offset);
   return {typecast_exprt(pair.first, f.type()), std::move(pair.second)};
 }
 

src/solvers/strings/string_constraint_generator_transformation.cpp

@@ -352,10 +352,7 @@ string_constraint_generatort::add_axioms_for_delete_char_at(
   const array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]);
   exprt index_one = from_integer(1, str.length_type());
   return add_axioms_for_delete(
-    res,
-    str,
-    f.arguments()[3],
-    plus_exprt(f.arguments()[3], index_one));
+    res, str, f.arguments()[3], plus_exprt(f.arguments()[3], index_one));
 }
 
 /// Add axioms stating that `res` corresponds to the input `str`
@@ -389,16 +386,10 @@ string_constraint_generatort::add_axioms_for_delete(
     array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_for_substring(
-      sub1,
-      str,
-      from_integer(0, str.length_type()),
-      start),
+      sub1, str, from_integer(0, str.length_type()), start),
     combine_results(
       add_axioms_for_substring(
-        sub2,
-        str,
-        end,
-        array_pool.get_or_create_length(str)),
+        sub2, str, end, array_pool.get_or_create_length(str)),
       add_axioms_for_concat(res, sub1, sub2)));
 }
 
@@ -421,6 +412,5 @@ string_constraint_generatort::add_axioms_for_delete(
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt arg = get_string_expr(array_pool, f.arguments()[2]);
-  return add_axioms_for_delete(
-    res, arg, f.arguments()[3], f.arguments()[4]);
+  return add_axioms_for_delete(res, arg, f.arguments()[3], f.arguments()[4]);
 }

src/solvers/strings/string_constraint_generator_valueof.cpp

@@ -52,8 +52,7 @@ string_constraint_generatort::add_axioms_from_long(
     return add_axioms_for_string_of_int_with_radix(
       res, f.arguments()[2], f.arguments()[3], 0);
   else
-    return add_axioms_for_string_of_int(
-      res, f.arguments()[2], 0);
+    return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
 }
 
 /// Add axioms corresponding to the String.valueOf(Z) java function.
@@ -548,11 +547,7 @@ string_constraint_generatort::add_axioms_for_parse_int(
   /// \note the only thing stopping us from taking longer strings with many
   /// leading zeros is the axioms for correct number format
   auto constraints1 = add_axioms_for_correct_number_format(
-    str,
-    radix_as_char,
-    radix_ul,
-    max_string_length,
-    strict_formatting);
+    str, radix_as_char, radix_ul, max_string_length, strict_formatting);
 
   auto constraints2 = add_axioms_for_characters_in_integer_string(
     input_int,

src/solvers/strings/string_format_builtin_function.cpp

@@ -130,9 +130,7 @@ add_axioms_for_format_specifier(
   {
   case format_specifiert::DECIMAL_INTEGER:
     return_code = generator.add_axioms_for_string_of_int(
-      res,
-      format_arg_from_string(string_arg, ID_int, array_pool),
-      0);
+      res, format_arg_from_string(string_arg, ID_int, array_pool), 0);
     return {res, std::move(return_code.second)};
   case format_specifiert::HEXADECIMAL_INTEGER:
     return_code = generator.add_axioms_for_string_of_int_with_radix(
@@ -143,13 +141,11 @@ add_axioms_for_format_specifier(
     return {res, std::move(return_code.second)};
   case format_specifiert::SCIENTIFIC:
     return_code = generator.add_axioms_from_float_scientific_notation(
-      res,
-      format_arg_from_string(string_arg, ID_float, array_pool));
+      res, format_arg_from_string(string_arg, ID_float, array_pool));
     return {res, std::move(return_code.second)};
   case format_specifiert::DECIMAL_FLOAT:
     return_code = generator.add_axioms_for_string_of_float(
-      res,
-      format_arg_from_string(string_arg, ID_float, array_pool));
+      res, format_arg_from_string(string_arg, ID_float, array_pool));
     return {res, std::move(return_code.second)};
   case format_specifiert::CHARACTER:
   {
@@ -176,8 +172,7 @@ add_axioms_for_format_specifier(
   }
   case format_specifiert::BOOLEAN:
     return_code = generator.add_axioms_from_bool(
-      res,
-      format_arg_from_string(string_arg, ID_boolean, array_pool));
+      res, format_arg_from_string(string_arg, ID_boolean, array_pool));
     return {res, std::move(return_code.second)};
   case format_specifiert::STRING:
   {
@@ -187,9 +182,7 @@ add_axioms_for_format_specifier(
   }
   case format_specifiert::HASHCODE:
     return_code = generator.add_axioms_for_string_of_int(
-      res,
-      format_arg_from_string(string_arg, "hashcode", array_pool),
-      0);
+      res, format_arg_from_string(string_arg, "hashcode", array_pool), 0);
     return {res, std::move(return_code.second)};
   case format_specifiert::LINE_SEPARATOR:
     // TODO: the constant should depend on the system: System.lineSeparator()
@@ -210,18 +203,14 @@ add_axioms_for_format_specifier(
     format_specifiert fs_lower = fs;
     fs_lower.conversion = tolower(fs.conversion);
     auto format_specifier_result = add_axioms_for_format_specifier(
-      generator,
-      fs_lower,
-      string_arg,
-      index_type,
-      char_type,
-      message);
+      generator, fs_lower, string_arg, index_type, char_type, message);
 
     const exprt return_code_upper_case =
       generator.fresh_symbol("return_code_upper_case", get_return_code_type());
     const string_to_upper_case_builtin_functiont upper_case_function(
       return_code_upper_case, res, format_specifier_result.first, array_pool);
-    auto upper_case_constraints = upper_case_function.constraints(generator.fresh_symbol);
+    auto upper_case_constraints =
+      upper_case_function.constraints(generator.fresh_symbol);
     merge(upper_case_constraints, std::move(format_specifier_result.second));
     return {res, std::move(upper_case_constraints)};
   }
@@ -345,12 +334,7 @@ static std::pair<exprt, string_constraintst> add_axioms_for_format(
       }
 
       auto result = add_axioms_for_format_specifier(
-        generator,
-        fs,
-        string_arg,
-        index_type,
-        char_type,
-        message);
+        generator, fs, string_arg, index_type, char_type, message);
       merge(constraints, std::move(result.second));
       intermediary_strings.push_back(result.first);
     }
@@ -394,15 +378,14 @@ static std::pair<exprt, string_constraintst> add_axioms_for_format(
     const array_string_exprt &intermediary = intermediary_strings[i];
     const array_string_exprt fresh =
       array_pool.fresh_string(index_type, char_type);
-    auto result =
-      generator.add_axioms_for_concat(fresh, str, intermediary);
+    auto result = generator.add_axioms_for_concat(fresh, str, intermediary);
     return_code = maximum(return_code, result.first);
     merge(constraints, std::move(result.second));
     str = fresh;
   }
 
-  auto result = generator.add_axioms_for_concat(
-    res, str, intermediary_strings.back());
+  auto result =
+    generator.add_axioms_for_concat(res, str, intermediary_strings.back());
   merge(constraints, std::move(result.second));
   return {maximum(result.first, return_code), std::move(constraints)};
 }