Skip to content

Unsafe type constructors #1722

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 10, 2018
Merged

Unsafe type constructors #1722

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c96e02a
no longer use deprecated constructors for some bitvector types
Jan 10, 2018
9c5add4
remove deprecated constructors for three bitvector types
Jan 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/ansi-c/padding.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down
3 changes: 1 addition & 2 deletions src/solvers/flattening/boolbv_extractbit.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 1 addition & 3 deletions src/solvers/smt1/smt1_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
3 changes: 1 addition & 2 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ";
Expand Down
16 changes: 0 additions & 16 deletions src/util/std_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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)
{
Expand Down