35 const exprt &given_alignment=
36 static_cast<const exprt &
>(type.
find(ID_C_alignment));
43 const auto a = numeric_cast<mp_integer>(given_alignment);
49 if(a_int>0 && !type.
get_bool(ID_C_packed))
52 else if(a_int==0 && type.
get_bool(ID_C_packed))
58 if(type.
id()==ID_array)
60 else if(type.
id()==ID_struct || type.
id()==ID_union)
67 result = std::max(result,
alignment(c.type(), ns));
69 else if(type.
id()==ID_unsignedbv ||
70 type.
id()==ID_signedbv ||
71 type.
id()==ID_fixedbv ||
72 type.
id()==ID_floatbv ||
73 type.
id()==ID_c_bool ||
74 type.
id()==ID_pointer)
78 else if(type.
id()==ID_c_enum)
80 else if(type.
id()==ID_c_enum_tag)
82 else if(type.
id() == ID_struct_tag)
84 else if(type.
id() == ID_union_tag)
86 else if(type.
id()==ID_c_bit_field)
96 if(a_int>0 && a_int<result)
107 if(subtype.
id() == ID_bool)
113 subtype.
id() == ID_signedbv || subtype.
id() == ID_unsignedbv ||
114 subtype.
id() == ID_c_bool)
118 else if(subtype.
id() == ID_c_enum_tag)
125 if(!c_enum_type.is_incomplete())
136 struct_typet::componentst::iterator where,
137 std::size_t pad_bits)
148 return std::next(components.insert(where,
component));
151 static struct_typet::componentst::iterator
pad(
153 struct_typet::componentst::iterator where,
154 std::size_t pad_bits)
164 return std::next(components.insert(where,
component));
171 std::size_t bit_field_bits = 0, underlying_bits = 0;
174 bool is_packed = type.
get_bool(ID_C_packed);
176 for(struct_typet::componentst::iterator it = components.begin();
177 it != components.end();
184 it->type().id() == ID_c_bit_field &&
191 bit_field_bits += width;
201 if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
203 const std::size_t pad_bits =
204 underlying_bits - (bit_field_bits % underlying_bits);
207 underlying_bits = bit_field_bits = 0;
212 underlying_bits = bit_field_bits = 0;
223 if(displacement != 0)
225 const mp_integer pad_bytes = a - displacement;
226 std::size_t pad_bits =
228 it =
pad(components, it, pad_bits);
235 if(it->type().id() == ID_c_bit_field)
240 bit_field_bits += width;
242 else if(it->type().id() == ID_bool)
251 if(size.has_value() && *size >= 1)
259 if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
261 const std::size_t
pad =
262 underlying_bits - (bit_field_bits % underlying_bits);
274 if(displacement != 0)
276 const mp_integer pad_bytes = a - displacement;
277 const std::size_t pad_bits =
279 pad(components, components.end(), pad_bits);
290 std::size_t bit_field_bits=0;
292 for(struct_typet::componentst::iterator
293 it=components.begin();
294 it!=components.end();
297 if(it->type().id()==ID_c_bit_field &&
302 bit_field_bits+=width;
304 else if(it->type().id() == ID_bool)
308 else if(bit_field_bits!=0)
325 const std::size_t
pad =
338 std::size_t bit_field_bits=0;
340 for(struct_typet::componentst::iterator
341 it=components.begin();
342 it!=components.end();
345 const typet it_type=it->type();
348 const bool packed=it_type.
get_bool(ID_C_packed) ||
351 if(it_type.
id()==ID_c_bit_field)
374 else if(it_type.
id() == ID_bool)
377 if(max_alignment < a)
390 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
406 const mp_integer pad_bytes = a - displacement;
407 const std::size_t pad_bits =
409 it =
pad(components, it, pad_bits);
422 static_cast<const exprt &
>(type.
find(ID_C_alignment));
429 if(tmp_i.has_value() && *tmp_i > max_alignment)
430 max_alignment = *tmp_i;
447 mp_integer pad_bytes = max_alignment - displacement;
448 std::size_t pad_bits =
450 pad(components, components.end(), pad_bits);
475 size_bits = std::max(size_bits, *s);
490 if(c.type().id() == ID_c_bit_field)
493 if(w.has_value() && w.value() > max_alignment_bits)
494 max_alignment_bits = w.value();
501 if(size_bits%max_alignment_bits!=0)
504 max_alignment_bits-(size_bits%max_alignment_bits);
507 numeric_cast_v<std::size_t>(size_bits + padding_bits));
std::size_t get_width() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
struct configt::ansi_ct ansi_c
Base class for all expressions.
bool get_bool(const irep_namet &name) const
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
The type of an expression, extends irept.
const typet & subtype() const
Fixed-width bit-vector with unsigned binary interpretation.
nonstd::optional< T > optionalt
mp_integer alignment(const typet &type, const namespacet &ns)
static optionalt< std::size_t > underlying_width(const c_bit_field_typet &type, const namespacet &ns)
static void add_padding_msvc(struct_typet &type, const namespacet &ns)
static void add_padding_gcc(struct_typet &type, const namespacet &ns)
void add_padding(struct_typet &type, const namespacet &ns)
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
static struct_typet::componentst::iterator pad_bit_field(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
ANSI-C Language Type Checking.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.