Clang whitespace changes

Author: JohnDumbell

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

@@ -95,8 +95,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,
@@ -534,6 +532,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_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

@@ -351,10 +351,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`
@@ -388,16 +385,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)));
 }
 
@@ -420,6 +411,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]);
 }