Go to the documentation of this file.
30 result.
name=
"location";
55 if(type.
id() == ID_symbol_type)
60 if(type.
id()==ID_unsignedbv)
62 result.
name=
"integer";
65 else if(type.
id()==ID_signedbv)
67 result.
name=
"integer";
70 else if(type.
id()==ID_floatbv)
75 else if(type.
id()==ID_bv)
77 result.
name=
"integer";
80 else if(type.
id()==ID_c_bit_field)
82 result.
name=
"integer";
85 else if(type.
id()==ID_c_enum_tag)
91 else if(type.
id()==ID_fixedbv)
96 else if(type.
id()==ID_pointer)
98 result.
name=
"pointer";
102 else if(type.
id()==ID_bool)
104 result.
name=
"boolean";
106 else if(type.
id()==ID_array)
112 else if(type.
id()==ID_vector)
114 result.
name=
"vector";
120 else if(type.
id()==ID_struct)
122 result.
name=
"struct";
132 else if(type.
id()==ID_union)
145 result.
name=
"unknown";
158 if(expr.
id()==ID_constant)
160 if(type.
id()==ID_unsignedbv ||
161 type.
id()==ID_signedbv ||
162 type.
id()==ID_c_bit_field)
166 result.
name=
"integer";
168 "binary",
integer2binary(numeric_cast_v<mp_integer>(expr), width));
171 const typet &underlying_type = type.
id() == ID_c_bit_field
177 std::string sig=
is_signed?
"":
"unsigned ";
194 else if(type.
id()==ID_c_enum)
196 result.
name=
"integer";
206 else if(type.
id()==ID_c_enum_tag)
213 else if(type.
id()==ID_bv)
215 result.
name=
"bitvector";
218 else if(type.
id()==ID_fixedbv)
225 else if(type.
id()==ID_floatbv)
232 else if(type.
id()==ID_pointer)
234 result.
name=
"pointer";
236 if(expr.
get(ID_value)==ID_NULL)
239 else if(type.
id()==ID_bool)
241 result.
name=
"boolean";
245 else if(type.
id()==ID_c_bool)
247 result.
name=
"integer";
250 const mp_integer b = numeric_cast_v<mp_integer>(expr);
255 result.
name=
"unknown";
258 else if(expr.
id()==ID_array)
272 else if(expr.
id()==ID_struct)
274 result.
name=
"struct";
277 if(type.
id()==ID_struct)
283 for(
unsigned m=0; m<expr.
operands().size(); m++)
291 else if(expr.
id()==ID_union)
301 result.
name=
"unknown";
const componentst & components() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const irep_idt & get_function() const
#define PRECONDITION(CONDITION)
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?
xmlt xml(const source_locationt &location)
Union constructor from single element.
const irep_idt & get_column() const
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.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
bool is_true() const
Return whether the expression is a constant representing true.
struct configt::ansi_ct ansi_c
const irep_idt & get_line() const
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
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
#define forall_operands(it, expr)
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 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
const std::string & get_string(const irep_namet &name) const
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
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 irep_idt & get_file() const
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.
const irep_idt & get_working_directory() const
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)