no longer use deprecated constructors for some bitvector types

Author: Daniel Kroening

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 ";