Merge pull request diffblue#4524 from antlechner/antonia/fewer-param-constructors

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -867,8 +867,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     location.set_function(local_name);
     side_effect_exprt java_new_array(
       ID_java_new_array, java_reference_type(struct_tag_type), location);
-    dereference_exprt old_array(this_symbol.symbol_expr(), struct_tag_type);
-    dereference_exprt new_array(local_symexpr, struct_tag_type);
+    dereference_exprt old_array{this_symbol.symbol_expr()};
+    dereference_exprt new_array{local_symexpr};
     member_exprt old_length(
       old_array, length_component.get_name(), length_component.type());
     java_new_array.copy_to_operands(old_length);

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1623,7 +1623,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
 
       const typecast_exprt pointer(op[0], java_array_type(statement[0]));
 
-      dereference_exprt array(pointer, pointer.type().subtype());
+      dereference_exprt array{pointer};
       PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);
       array.set(ID_java_member_access, true);
 
@@ -2832,17 +2832,16 @@ exprt java_bytecode_convert_methodt::convert_aload(
   const char &type_char = statement[0];
   const typecast_exprt pointer(op[0], java_array_type(type_char));
 
-  dereference_exprt deref(pointer, pointer.type().subtype());
+  dereference_exprt deref{pointer};
   deref.set(ID_java_member_access, true);
 
   const member_exprt data_ptr(
     deref, "data", pointer_type(java_type_from_char(type_char)));
 
-  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
+  plus_exprt data_plus_offset{data_ptr, op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
-  const typet &element_type = data_ptr.type().subtype();
-  const dereference_exprt element(data_plus_offset, element_type);
+  const dereference_exprt element{data_plus_offset};
   return java_bytecode_promotion(element);
 }
 
@@ -2881,17 +2880,16 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
   const char type_char = statement[0];
   const typecast_exprt pointer(op[0], java_array_type(type_char));
 
-  dereference_exprt deref(pointer, pointer.type().subtype());
+  dereference_exprt deref{pointer};
   deref.set(ID_java_member_access, true);
 
   const member_exprt data_ptr(
     deref, "data", pointer_type(java_type_from_char(type_char)));
 
-  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
+  plus_exprt data_plus_offset{data_ptr, op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
-  const typet &element_type = data_ptr.type().subtype();
-  const dereference_exprt element(data_plus_offset, element_type);
+  const dereference_exprt element{data_plus_offset};
 
   code_blockt block;
   block.add_source_location() = location;

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1102,8 +1102,7 @@ void java_object_factoryt::array_primitive_init_code(
 
   // *array_data_init = NONDET(TYPE [max_length_expr]);
   side_effect_expr_nondett nondet_data(array_type, location);
-  const dereference_exprt data_pointer_deref(
-    tmp_finite_array_pointer, array_type);
+  const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
   assignments.add(code_assignt(data_pointer_deref, std::move(nondet_data)));
   assignments.statements().back().add_source_location() = location;
 
@@ -1201,9 +1200,8 @@ void java_object_factoryt::array_loop_init_code(
     assignments.add(std::move(max_test));
   }
 
-  const dereference_exprt arraycellref(
-    plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
-    array_init_symexpr.type().subtype());
+  const dereference_exprt arraycellref{
+    plus_exprt{array_init_symexpr, counter_expr}};
 
   bool new_item_is_primitive = arraycellref.type().id() != ID_pointer;
 
@@ -1303,7 +1301,7 @@ void java_object_factoryt::gen_nondet_array_init(
     is_valid_java_array(struct_type),
     "Java struct array does not conform to expectations");
 
-  dereference_exprt deref_expr(expr, expr.type().subtype());
+  dereference_exprt deref_expr(expr);
   const auto &comps = struct_type.components();
   const member_exprt length_expr(deref_expr, "length", comps[1].type());
   exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -21,9 +21,7 @@ Author: Daniel Kroening, [email protected]
 /// \return dereferenced pointer
 static exprt clean_deref(const exprt &ptr)
 {
-  return ptr.id()==ID_address_of
-             ? ptr.op0()
-             : dereference_exprt(ptr, ptr.type().subtype());
+  return ptr.id() == ID_address_of ? ptr.op0() : dereference_exprt{ptr};
 }
 
 /// \par parameters: pointer

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -602,7 +602,7 @@ exprt make_nondet_infinite_char_array(
   code.add(code_declt(data_pointer));
   code.add(make_allocate_code(data_pointer, array_type.size()));
   const exprt nondet_data = side_effect_expr_nondett(array_type, loc);
-  const exprt data = dereference_exprt(data_pointer, array_type);
+  const exprt data = dereference_exprt{data_pointer};
   code.add(code_assignt(data, nondet_data), loc);
   return data;
 }

src/analyses/goto_check.cpp

@@ -1106,7 +1106,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
       binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
 
-      plus_exprt ub(int_ptr, size, int_ptr.type());
+      plus_exprt ub{int_ptr, size};
 
       binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second));
 
@@ -1576,7 +1576,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
       const exprt new_address_casted =
         typecast_exprt::conditional_cast(new_address, new_pointer_type);
 
-      dereference_exprt new_deref(new_address_casted, expr.type());
+      dereference_exprt new_deref{new_address_casted};
       new_deref.add_source_location() = deref.source_location();
       pointer_validity_check(new_deref, guard);
 

src/ansi-c/c_typecheck_expr.cpp

@@ -2009,7 +2009,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
   }
   else
   {
-    dereference_exprt tmp(f_op, f_op_type.subtype());
+    dereference_exprt tmp{f_op};
     tmp.set(ID_C_implicit, true);
     tmp.add_source_location()=f_op.source_location();
     f_op.swap(tmp);

src/goto-instrument/wmm/shared_buffers.cpp

@@ -1214,7 +1214,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
                     read_delayed_expr,
                     if_exprt(
                       choice1_expr,
-                      dereference_exprt(new_read_expr, vars.type),
+                      dereference_exprt{new_read_expr},
                       to_replace_expr),
                     to_replace_expr); // original_instruction.code.op1());
 

src/goto-programs/builtin_functions.cpp

@@ -299,7 +299,7 @@ void goto_convertt::do_scanf(
               copy(array_copy_statement, OTHER, dest);
               #else
               const index_exprt new_lhs(
-                dereference_exprt(ptr, *type), from_integer(0, index_type()));
+                dereference_exprt{ptr}, from_integer(0, index_type()));
               const side_effect_expr_nondett rhs(
                 type->subtype(), function.source_location());
               code_assignt assign(new_lhs, rhs);
@@ -310,7 +310,7 @@ void goto_convertt::do_scanf(
             else
             {
               // make it nondet for now
-              const dereference_exprt new_lhs(ptr, *type);
+              const dereference_exprt new_lhs{ptr};
               const side_effect_expr_nondett rhs(
                 *type, function.source_location());
               code_assignt assign(new_lhs, rhs);
@@ -1222,7 +1222,7 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // build *ptr
-    dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
+    dereference_exprt deref_ptr{arguments[0]};
 
     dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
@@ -1287,7 +1287,7 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // build *ptr
-    dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
+    dereference_exprt deref_ptr{arguments[0]};
 
     dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
@@ -1356,7 +1356,7 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // build *ptr
-    dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
+    dereference_exprt deref_ptr{arguments[0]};
 
     dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
@@ -1412,7 +1412,7 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // build *ptr
-    dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
+    dereference_exprt deref_ptr{arguments[0]};
 
     dest.add(goto_programt::make_atomic_begin(function.source_location()));
 

src/goto-programs/class_identifier.cpp

@@ -67,7 +67,7 @@ exprt get_class_identifier_field(
   const auto &points_to=this_expr.type().subtype();
   if(points_to==empty_typet())
     this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
-  const dereference_exprt deref(this_expr, this_expr.type().subtype());
+  const dereference_exprt deref{this_expr};
   return build_class_identifier(deref, ns);
 }
 

src/goto-programs/string_abstraction.cpp

@@ -964,7 +964,7 @@ bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest)
   dest=str_symbol.symbol_expr();
   if(current_args.find(symbol.name)!=current_args.end() &&
       !is_ptr_argument(abstract_type))
-    dest=dereference_exprt(dest, dest.type().subtype());
+    dest = dereference_exprt{dest};
 
   return false;
 }
@@ -1218,10 +1218,9 @@ goto_programt::targett string_abstractiont::value_assignments(
           index_exprt(lhs, from_integer(i, a_size.type())),
           index_exprt(rhs, from_integer(i, a_size.type())));
   }
-  else if(lhs.type().id()==ID_pointer)
-    return value_assignments(dest, target,
-        dereference_exprt(lhs, lhs.type().subtype()),
-        dereference_exprt(rhs, rhs.type().subtype()));
+  else if(lhs.type().id() == ID_pointer)
+    return value_assignments(
+      dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});
   else if(lhs.type()==string_struct)
     return value_assignments_string_struct(dest, target, lhs, rhs);
   else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)

src/goto-programs/string_instrumentation.cpp

@@ -552,9 +552,7 @@ void string_instrumentationt::do_format_string_write(
         default: // everything else
         {
           const exprt &argument=arguments[argument_start_inx+args];
-          const typet &arg_type = argument.type();
-
-          const dereference_exprt lhs(argument, arg_type.subtype());
+          const dereference_exprt lhs{argument};
 
           side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 
@@ -594,7 +592,7 @@ void string_instrumentationt::do_format_string_write(
       }
       else
       {
-        dereference_exprt lhs(arguments[i], arg_type.subtype());
+        dereference_exprt lhs{arguments[i]};
 
         side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 

src/goto-symex/symex_dereference.cpp

@@ -255,8 +255,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
     address_of_exprt address_of_expr(index_expr.array());
     address_of_expr.type()=pointer_type(expr.type());
 
-    dereference_exprt tmp(
-      plus_exprt(address_of_expr, index_expr.index()), expr.type());
+    dereference_exprt tmp{plus_exprt{address_of_expr, index_expr.index()}};
     tmp.add_source_location()=expr.source_location();
 
     // recursive call

src/pointer-analysis/value_set_dereference.cpp

@@ -306,7 +306,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     result.pointer_guard = dynamic_object(pointer_expr);
 
     // can't remove here, turn into *p
-    result.value=dereference_exprt(pointer_expr, dereference_type);
+    result.value = dereference_exprt{pointer_expr};
   }
   else if(root_object.id()==ID_integer_address)
   {

src/solvers/smt2/smt2_conv.cpp

@@ -561,10 +561,7 @@ void smt2_convt::convert_address_of_rec(
         new_index_expr,
         pointer_type(array.type().subtype()));
 
-      plus_exprt plus_expr(
-        address_of_expr,
-        index,
-        address_of_expr.type());
+      plus_exprt plus_expr{address_of_expr, index};
 
       convert_expr(plus_expr);
     }

src/util/simplify_expr_pointer.cpp

@@ -87,7 +87,7 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
               from_integer((*step_size) * (*index) + address, index_type()),
               pointer_type);
 
-            expr = dereference_exprt(typecast_expr, expr.type());
+            expr = dereference_exprt{typecast_expr};
             result = true;
           }
         }
@@ -124,7 +124,7 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
             pointer_type.subtype()=expr.type();
             typecast_exprt typecast_expr(
               from_integer(address + *offset, index_type()), pointer_type);
-            expr = dereference_exprt(typecast_expr, expr.type());
+            expr = dereference_exprt{typecast_expr};
             result=true;
           }
         }