Merge pull request #7412 from tautschnig/cleanup/pointert-constructor

Remove pointert default constructor

Author: kroening

src/cprover/bv_pointers_wide.cpp

@@ -788,10 +788,9 @@ exprt bv_pointers_widet::bv_get_rec(
 
   constant_exprt result(bvrep, type);
 
-  pointer_logict::pointert pointer;
-  pointer.object =
-    numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
-  pointer.offset = binary2integer(value_offset, true);
+  pointer_logict::pointert pointer{
+    numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
+    binary2integer(value_offset, true)};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};

src/solvers/flattening/bv_pointers.cpp

@@ -804,10 +804,9 @@ exprt bv_pointerst::bv_get_rec(
 
   constant_exprt result(bvrep, type);
 
-  pointer_logict::pointert pointer;
-  pointer.object =
-    numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
-  pointer.offset=binary2integer(value_offset, true);
+  pointer_logict::pointert pointer{
+    numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
+    binary2integer(value_offset, true)};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};

src/solvers/flattening/pointer_logic.h

@@ -29,10 +29,6 @@ class pointer_logict
   {
     mp_integer object, offset;
 
-    pointert()
-    {
-    }
-
     pointert(mp_integer _obj, mp_integer _off)
       : object(std::move(_obj)), offset(std::move(_off))
     {

src/solvers/smt2/smt2_conv.cpp

@@ -659,9 +659,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
 
     // split into object and offset
     mp_integer pow=power(2, width-config.bv_encoding.object_bits);
-    pointer_logict::pointert ptr;
-    ptr.object = numeric_cast_v<std::size_t>(v / pow);
-    ptr.offset=v%pow;
+    pointer_logict::pointert ptr{numeric_cast_v<std::size_t>(v / pow), v % pow};
     return annotated_pointer_constant_exprt(
       bv_expr.get_value(),
       pointer_logic.pointer_expr(ptr, to_pointer_type(type)));