Remove pointert default constructor

This constructor catered the risk of dealing with uninitialised object/offset pairs.
tautschnig · Dec 5, 2022 · 3302184 · 3302184
1 parent 6672791
commit 3302184
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 15 deletions.
diff --git a/src/cprover/bv_pointers_wide.cpp b/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)};

diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -795,10 +795,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)};

diff --git a/src/solvers/flattening/pointer_logic.h b/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))
     {

diff --git a/src/solvers/smt2/smt2_conv.cpp b/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)));