Merge pull request #1722 from diffblue/unsafe_type_constructors

Unsafe type constructors

Author: tautschnig

src/ansi-c/padding.cpp

@@ -225,8 +225,8 @@ void add_padding(struct_typet &type, const namespacet &ns)
       {
         mp_integer pad=a-displacement;
 
-        unsignedbv_typet padding_type;
-        padding_type.set_width(integer2unsigned(pad*8));
+        std::size_t width=integer2size_t(pad*8);
+        unsignedbv_typet padding_type(width);
 
         struct_typet::componentt component;
         component.type()=padding_type;
@@ -282,8 +282,8 @@ void add_padding(struct_typet &type, const namespacet &ns)
     {
       mp_integer pad=max_alignment-displacement;
 
-      unsignedbv_typet padding_type;
-      padding_type.set_width(integer2unsigned(pad*8));
+      std::size_t width=integer2size_t(pad*8);
+      unsignedbv_typet padding_type(width);
 
       // we insert after any final 'flexible member'
       struct_typet::componentt component;
@@ -324,8 +324,8 @@ void add_padding(union_typet &type, const namespacet &ns)
     mp_integer padding_bits=
       max_alignment_bits-(size_bits%max_alignment_bits);
 
-    unsignedbv_typet padding_type;
-    padding_type.set_width(integer2size_t(size_bits+padding_bits));
+    unsignedbv_typet padding_type(
+      integer2size_t(size_bits+padding_bits));
 
     struct_typet::componentt component;
     component.type()=padding_type;

src/solvers/flattening/boolbv_extractbit.cpp

@@ -55,8 +55,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     mp_integer index_width=
       std::max(address_bits(width_op0), mp_integer(width_op1));
 
-    unsignedbv_typet index_type;
-    index_type.set_width(integer2unsigned(index_width));
+    unsignedbv_typet index_type(integer2size_t(index_width));
 
     equal_exprt equality;
     equality.lhs()=operands[1]; // index operand

src/solvers/smt1/smt1_conv.cpp

@@ -234,9 +234,7 @@ exprt smt1_convt::ce_value(
 
 typet smt1_convt::array_index_type() const
 {
-  signedbv_typet t;
-  t.set_width(array_index_bits);
-  return t;
+  return signedbv_typet(array_index_bits);
 }
 
 void smt1_convt::array_index(const exprt &expr)

src/solvers/smt2/smt2_conv.cpp

@@ -550,8 +550,7 @@ void smt2_convt::convert_address_of_rec(
       mp_integer offset=member_offset(struct_type, component_name, ns);
       assert(offset>=0);
 
-      unsignedbv_typet index_type;
-      index_type.set_width(boolbv_width(result_type));
+      unsignedbv_typet index_type(boolbv_width(result_type));
 
       // pointer arithmetic
       out << "(bvadd ";

src/util/std_types.h

@@ -1134,10 +1134,6 @@ inline bitvector_typet &to_bitvector_type(typet &type)
 class bv_typet:public bitvector_typet
 {
 public:
-  bv_typet():bitvector_typet(ID_bv)
-  {
-  }
-
   explicit bv_typet(std::size_t width):bitvector_typet(ID_bv)
   {
     set_width(width);
@@ -1174,10 +1170,6 @@ inline bv_typet &to_bv_type(typet &type)
 class unsignedbv_typet:public bitvector_typet
 {
 public:
-  unsignedbv_typet():bitvector_typet(ID_unsignedbv)
-  {
-  }
-
   explicit unsignedbv_typet(std::size_t width):
     bitvector_typet(ID_unsignedbv, width)
   {
@@ -1220,10 +1212,6 @@ inline unsignedbv_typet &to_unsignedbv_type(typet &type)
 class signedbv_typet:public bitvector_typet
 {
 public:
-  signedbv_typet():bitvector_typet(ID_signedbv)
-  {
-  }
-
   explicit signedbv_typet(std::size_t width):
     bitvector_typet(ID_signedbv, width)
   {
@@ -1343,10 +1331,6 @@ inline const floatbv_typet &to_floatbv_type(const typet &type)
 class c_bit_field_typet:public bitvector_typet
 {
 public:
-  c_bit_field_typet():bitvector_typet(ID_c_bit_field)
-  {
-  }
-
   explicit c_bit_field_typet(const typet &subtype, std::size_t width):
     bitvector_typet(ID_c_bit_field, subtype, width)
   {