diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index 9970298b440..3b87a6190d8 100644 --- a/src/ansi-c/padding.cpp +++ b/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; diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp index f24b8a1394a..7dbea100aeb 100644 --- a/src/solvers/flattening/boolbv_extractbit.cpp +++ b/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 diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index 87d7858ef02..4276c55d0d0 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/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) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 0e4c95f3609..71b35530150 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/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 "; diff --git a/src/util/std_types.h b/src/util/std_types.h index 3412abff13c..784dbdc0a9d 100644 --- a/src/util/std_types.h +++ b/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) {