Go to the documentation of this file.
34 if(src.
id()==ID_constant)
38 if(type.
id()==ID_pointer)
54 src.
id() == ID_address_of &&
58 .find(
"@") != std::string::npos)
64 src.
id() == ID_address_of &&
75 else if(src.
id()==ID_member &&
78 .find(
"@")!=std::string::npos)
124 if(type.
id() == ID_symbol_type)
129 if(type.
id()==ID_unsignedbv)
135 else if(type.
id()==ID_signedbv)
141 else if(type.
id()==ID_floatbv)
147 else if(type.
id()==ID_bv)
152 else if(type.
id()==ID_c_bit_field)
158 else if(type.
id()==ID_c_enum_tag)
166 else if(type.
id()==ID_fixedbv)
172 else if(type.
id()==ID_pointer)
177 else if(type.
id()==ID_bool)
181 else if(type.
id()==ID_array)
186 else if(type.
id()==ID_vector)
192 else if(type.
id()==ID_struct)
205 else if(type.
id()==ID_union)
247 if(expr.
id()==ID_constant)
249 std::unique_ptr<languaget> lang;
259 const typet &underlying_type =
262 std::string type_string;
263 bool error=lang->
from_type(underlying_type, type_string, ns);
266 std::string value_string;
270 if(type.
id()==ID_unsignedbv ||
271 type.
id()==ID_signedbv ||
272 type.
id()==ID_c_bit_field)
282 else if(type.
id()==ID_c_enum)
291 else if(type.
id()==ID_c_enum_tag)
296 return json(tmp, ns, mode);
298 else if(type.
id()==ID_bv)
303 else if(type.
id()==ID_fixedbv)
311 else if(type.
id()==ID_floatbv)
319 else if(type.
id()==ID_pointer)
325 simpl_expr.
get(ID_value) == ID_NULL ||
327 (simpl_expr.
id() == ID_constant &&
328 simpl_expr.
type().
id() == ID_pointer &&
333 else if(simpl_expr.
id()==ID_symbol)
339 "pointer identifier should have non-empty components");
343 else if(type.
id()==ID_bool)
349 else if(type.
id()==ID_c_bool)
357 else if(type.
id()==ID_string)
367 else if(expr.
id()==ID_array)
378 e[
"value"]=
json(*it, ns, mode);
382 else if(expr.
id()==ID_struct)
387 if(type.
id()==ID_struct)
392 components.size()==expr.
operands().size(),
393 "number of struct components should match with its type");
396 for(std::size_t m=0; m<expr.
operands().size(); m++)
404 else if(expr.
id()==ID_union)
410 e[
"value"]=
json(union_expr.
op(), ns, mode);
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
json_objectt json(const source_locationt &location)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
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())
struct configt::ansi_ct ansi_c
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool is_true() const
Return whether the expression is a constant representing true.
json_objectt & make_object()
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
#define forall_operands(it, expr)
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
const irep_idt & get_identifier() const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
json_arrayt & make_array()
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
const irep_idt & get_java_bytecode_index() 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
bool value_is_zero_string() const
static exprt simplify_json_expr(const exprt &src, const namespacet &ns)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
static std::string binary(const constant_exprt &src)
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.
const irep_idt & get_file() const
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
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
static jsont json_boolean(bool value)
const irep_idt & get_value() const
jsont & push_back(const jsont &json)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::unique_ptr< languaget > get_default_language()
Returns the default language.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
#define CHECK_RETURN(CONDITION)