35 const exprt &given_alignment=
36 static_cast<const exprt &
>(type.
find(ID_C_alignment));
41 if(given_alignment.
is_nil() ||
46 if(a_int>0 && !type.
get_bool(ID_C_packed))
49 else if(a_int==0 && type.
get_bool(ID_C_packed))
55 if(type.
id()==ID_array)
57 else if(type.
id()==ID_struct || type.
id()==ID_union)
66 for(struct_union_typet::componentst::const_iterator
67 it=components.begin();
70 result=std::max(result,
alignment(it->type(), ns));
72 else if(type.
id()==ID_unsignedbv ||
73 type.
id()==ID_signedbv ||
74 type.
id()==ID_fixedbv ||
75 type.
id()==ID_floatbv ||
79 result=width%8?width/8+1:width/8;
81 else if(type.
id()==ID_c_enum)
83 else if(type.
id()==ID_c_enum_tag)
85 else if(type.
id()==ID_pointer)
88 result=width%8?width/8+1:width/8;
90 else if(type.
id()==ID_symbol)
92 else if(type.
id()==ID_c_bit_field)
102 if(a_int>0 && a_int<result)
116 std::size_t padding_counter=0;
117 std::size_t bit_field_bits=0;
119 for(struct_typet::componentst::iterator
120 it=components.begin();
121 it!=components.end();
124 if(it->type().id()==ID_c_bit_field &&
129 bit_field_bits+=width;
131 else if(bit_field_bits!=0)
134 if((bit_field_bits%8)!=0)
136 std::size_t pad=8-bit_field_bits%8;
140 component.
type()=padding_type;
142 "$bit_field_pad"+std::to_string(padding_counter++));
145 it=components.insert(it, component);
156 if((bit_field_bits%8)!=0)
158 std::size_t pad=8-bit_field_bits%8;
162 component.
type()=padding_type;
163 component.
set_name(
"$bit_field_pad"+std::to_string(padding_counter++));
166 components.push_back(component);
176 std::size_t padding_counter=0;
178 std::size_t bit_field_bits=0;
180 for(struct_typet::componentst::iterator
181 it=components.begin();
182 it!=components.end();
185 const typet it_type=it->type();
188 const bool packed=it_type.
get_bool(ID_C_packed) ||
191 if(it_type.
id()==ID_c_bit_field)
208 for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
237 component.
type()=padding_type;
238 component.
set_name(
"$pad"+std::to_string(padding_counter++));
241 it=components.insert(it, component);
254 if(bit_field_bits!=0)
257 offset+=bit_field_bits/8;
264 static_cast<const exprt &
>(type.
find(ID_C_alignment));
265 if(alignment.
id()!=ID_default)
270 if(!
to_integer(tmp, tmp_i) && tmp_i>max_alignment)
295 component.
type()=padding_type;
296 component.
set_name(
"$pad"+std::to_string(padding_counter++));
299 components.push_back(component);
310 throw "type of unknown size:\n"+type.
pretty();
324 if(size_bits%max_alignment!=0)
326 mp_integer padding=max_alignment-(size_bits%max_alignment);
332 component.
type()=padding_type;
336 components.push_back(component);
The type of an expression.
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set_name(const irep_idt &name)
std::vector< componentt > componentst
const componentst & components() const
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
bool get_bool(const irep_namet &name) const
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const typet & follow_tag(const union_tag_typet &src) const
const irep_idt & id() const
void set_is_padding(bool is_padding)
void add_padding(struct_typet &type, const namespacet &ns)
ANSI-C Language Type Checking.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
std::size_t get_width() const
unsigned integer2unsigned(const mp_integer &n)
Base class for all expressions.
const typet & subtype() const
const irept & find(const irep_namet &name) const
bool simplify(exprt &expr, const namespacet &ns)
void set_width(std::size_t width)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.