Go to the documentation of this file.
30 if(type.
id() == ID_unsignedbv)
32 result.
name =
"integer";
35 else if(type.
id() == ID_signedbv)
37 result.
name =
"integer";
40 else if(type.
id() == ID_floatbv)
42 result.
name =
"float";
45 else if(type.
id() == ID_bv)
47 result.
name =
"integer";
50 else if(type.
id() == ID_c_bit_field)
52 result.
name =
"integer";
55 else if(type.
id() == ID_c_enum_tag)
60 else if(type.
id() == ID_fixedbv)
62 result.
name =
"fixed";
65 else if(type.
id() == ID_pointer)
67 result.
name =
"pointer";
71 else if(type.
id() == ID_bool)
73 result.
name =
"boolean";
75 else if(type.
id() == ID_array)
77 result.
name =
"array";
83 else if(type.
id() == ID_vector)
85 result.
name =
"vector";
91 else if(type.
id() == ID_struct)
93 result.
name =
"struct";
103 else if(type.
id() == ID_struct_tag)
107 else if(type.
id() == ID_union)
109 result.
name =
"union";
119 else if(type.
id() == ID_union_tag)
124 result.
name =
"unknown";
133 if(expr.
id() == ID_constant)
136 const auto &value = constant_expr.get_value();
141 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
142 type.
id() == ID_c_bit_field || type.
id() == ID_c_bool)
144 mp_integer i = numeric_cast_v<mp_integer>(constant_expr);
147 result.
name =
"integer";
151 const typet &underlying_type = type.
id() == ID_c_bit_field
155 bool is_signed = underlying_type.
id() == ID_signedbv;
157 std::string sig =
is_signed ?
"" :
"unsigned ";
159 if(type.
id() == ID_c_bool)
174 else if(type.
id() == ID_c_enum)
179 const auto integer_value =
bvrep2integer(value, width,
false);
180 result.
name =
"integer";
187 else if(type.
id() == ID_c_enum_tag)
193 else if(type.
id() == ID_bv)
195 result.
name =
"bitvector";
196 result.
set_attribute(
"binary", constant_expr.get_string(ID_value));
198 else if(type.
id() == ID_fixedbv)
201 result.
name =
"fixed";
207 else if(type.
id() == ID_floatbv)
210 result.
name =
"float";
216 else if(type.
id() == ID_pointer)
219 result.
name =
"pointer";
222 if(constant_expr.get(ID_value) == ID_NULL)
223 result.
data =
"NULL";
225 else if(type.
id() == ID_bool)
227 result.
name =
"boolean";
228 result.
set_attribute(
"binary", constant_expr.is_true() ?
"1" :
"0");
229 result.
data = constant_expr.is_true() ?
"TRUE" :
"FALSE";
233 result.
name =
"unknown";
236 else if(expr.
id() == ID_array)
238 result.
name =
"array";
250 else if(expr.
id() == ID_struct)
252 result.
name =
"struct";
257 if(type.
id() == ID_struct)
263 for(
unsigned m = 0; m < expr.
operands().size(); m++)
271 else if(expr.
id() == ID_union)
274 result.
name =
"union";
281 result.
name =
"unknown";
const componentst & components() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
std::string to_ansi_c_string() const
bool is_signed(const typet &t)
Convenience function – is the type signed?
Union constructor from single element.
Base class for all expressions.
std::vector< componentt > componentst
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
struct configt::ansi_ct ansi_c
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const std::string & id2string(const irep_idt &d)
std::string to_ansi_c_string() const
#define forall_operands(it, expr)
#define PRECONDITION(CONDITION)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
std::size_t long_long_int_width
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
xmlt xml(const typet &type, const namespacet &ns)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::size_t get_width() const
irep_idt get_component_name() const
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set_attribute(const std::string &attribute, unsigned value)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
std::size_t short_int_width
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const std::string integer2binary(const mp_integer &n, std::size_t width)
A constant literal expression.
API to expression classes.
std::size_t long_int_width
xmlt & new_element(const std::string &key)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)