34 if(src.
id() == ID_constant)
36 if(src.
type().
id() == ID_pointer)
51 else if(src.
id() == ID_typecast)
55 else if(src.
id() == ID_address_of)
59 if(
object.
id() == ID_symbol)
65 object.
id() == ID_member &&
73 object.
id() == ID_index &&
82 src.
id() == ID_member &&
103 if(type.
id() == ID_unsignedbv)
109 else if(type.
id() == ID_signedbv)
115 else if(type.
id() == ID_floatbv)
121 else if(type.
id() == ID_bv)
127 else if(type.
id() == ID_c_bit_field)
133 else if(type.
id() == ID_c_enum_tag)
139 else if(type.
id() == ID_fixedbv)
145 else if(type.
id() == ID_pointer)
150 else if(type.
id() == ID_bool)
154 else if(type.
id() == ID_array)
160 else if(type.
id() == ID_vector)
166 else if(type.
id() == ID_struct)
179 else if(type.
id() == ID_struct_tag)
183 else if(type.
id() == ID_union)
196 else if(type.
id() == ID_union_tag)
209 if(src.
type().
id() == ID_c_enum)
228 if(expr.
id() == ID_constant)
234 std::unique_ptr<languaget> lang;
235 if(mode != ID_unknown)
240 const typet &underlying_type =
244 std::string type_string;
245 bool error = lang->from_type(underlying_type, type_string, ns);
248 std::string value_string;
249 lang->from_expr(expr, value_string, ns);
252 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
253 type.
id() == ID_c_bit_field || type.
id() == ID_c_bool)
263 else if(type.
id() == ID_c_enum)
272 else if(type.
id() == ID_c_enum_tag)
277 return json(tmp, ns, mode);
279 else if(type.
id() == ID_bv)
284 else if(type.
id() == ID_fixedbv)
293 else if(type.
id() == ID_floatbv)
302 else if(type.
id() == ID_pointer)
308 simpl_expr.
get(ID_value) == ID_NULL ||
310 (simpl_expr.
id() == ID_constant &&
311 simpl_expr.
type().
id() == ID_pointer &&
316 else if(simpl_expr.
id() == ID_symbol)
322 "pointer identifier should have non-empty components");
326 else if(type.
id() == ID_bool)
332 else if(type.
id() == ID_string)
342 else if(expr.
id() == ID_array)
347 std::size_t index = 0;
352 {
"value",
json(*it, ns, mode)}};
357 else if(expr.
id() == ID_struct)
364 if(type.
id() == ID_struct)
369 components.size() == expr.
operands().size(),
370 "number of struct components should match with its type");
373 for(std::size_t m = 0; m < expr.
operands().size(); m++)
381 else if(expr.
id() == ID_union)
void base_type(typet &type, const namespacet &ns)
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
std::size_t get_width() const
const typet & underlying_type() const
const typet & underlying_type() const
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
bool value_is_zero_string() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
jsont & push_back(const jsont &json)
json_arrayt & make_array()
static jsont json_boolean(bool value)
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
const irep_idt & get_identifier() const
The type of an expression, extends irept.
Union constructor from single element.
irep_idt get_component_name() const
#define forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
static std::string binary(const constant_exprt &src)
static exprt simplify_json_expr(const exprt &src)
json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
Output a CBMC type in json.
Abstract interface to support a programming language.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
std::unique_ptr< languaget > get_default_language()
Returns the default language.
const std::string integer2binary(const mp_integer &n, std::size_t width)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
#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())
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.