34 if(src.
id()==ID_constant)
38 if(type.
id()==ID_pointer)
43 (value!=std::string(value.
size(),
'0') ||
46 src.
op0().
id()!=ID_constant)
51 else if(src.
id()==ID_address_of &&
53 src.
op0().
id()==ID_member &&
55 src.
op0()).get_component_name()).find(
"@")!=std::string::npos)
60 else if(src.
id()==ID_address_of &&
62 src.
op0().
id()==ID_index &&
70 else if(src.
id()==ID_member &&
74 .find(
"@")!=std::string::npos)
120 if(type.
id()==ID_symbol)
125 if(type.
id()==ID_unsignedbv)
131 else if(type.
id()==ID_signedbv)
137 else if(type.
id()==ID_floatbv)
143 else if(type.
id()==ID_bv)
148 else if(type.
id()==ID_c_bit_field)
154 else if(type.
id()==ID_c_enum_tag)
159 else if(type.
id()==ID_fixedbv)
165 else if(type.
id()==ID_pointer)
170 else if(type.
id()==ID_bool)
174 else if(type.
id()==ID_array)
179 else if(type.
id()==ID_vector)
185 else if(type.
id()==ID_struct)
191 for(
const auto &component : components)
195 e[
"type"]=
json(component.type(), ns, mode);
198 else if(type.
id()==ID_union)
204 for(
const auto &component : components)
208 e[
"type"]=
json(component.type(), ns, mode);
233 if(expr.
id()==ID_constant)
235 std::unique_ptr<languaget> lang;
245 const typet &underlying_type=
246 type.
id()==ID_c_bit_field?type.
subtype():
249 std::string type_string;
250 bool error=lang->
from_type(underlying_type, type_string, ns);
253 std::string value_string;
257 if(type.
id()==ID_unsignedbv ||
258 type.
id()==ID_signedbv ||
259 type.
id()==ID_c_bit_field)
269 else if(type.
id()==ID_c_enum)
277 else if(type.
id()==ID_c_enum_tag)
282 return json(tmp, ns, mode);
284 else if(type.
id()==ID_bv)
289 else if(type.
id()==ID_fixedbv)
297 else if(type.
id()==ID_floatbv)
305 else if(type.
id()==ID_pointer)
310 if(simpl_expr.
get(ID_value)==ID_NULL ||
312 (simpl_expr.
id()==ID_constant && simpl_expr.
type().
id()==ID_pointer &&
313 simpl_expr.
op0().
get(ID_value)==ID_NULL))
315 else if(simpl_expr.
id()==ID_symbol)
321 "pointer identifier should have non-empty components");
325 else if(type.
id()==ID_bool)
331 else if(type.
id()==ID_c_bool)
339 else if(type.
id()==ID_string)
349 else if(expr.
id()==ID_array)
360 e[
"value"]=
json(*it, ns, mode);
364 else if(expr.
id()==ID_struct)
369 if(type.
id()==ID_struct)
374 components.size()==expr.
operands().size(),
375 "number of struct components should match with its type");
378 for(std::size_t m=0; m<expr.
operands().size(); m++)
386 else if(expr.
id()==ID_union)
392 e[
"value"]=
json(union_expr.
op(), ns, mode);
The type of an expression.
const irep_idt & get_working_directory() const
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
std::unique_ptr< languaget > get_default_language()
Returns the default language.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
const irep_idt & get_function() const
const irep_idt & get_identifier() const
std::vector< componentt > componentst
const irep_idt & get_value() const
const componentst & components() const
static jsont json_boolean(bool value)
A constant literal expression.
#define CHECK_RETURN(CONDITION)
const typet & follow_tag(const union_tag_typet &) const
json_arrayt & make_array()
const irep_idt & get_column() const
jsont & push_back(const jsont &json)
const irep_idt & id() const
void set_value(const irep_idt &value)
const irep_idt & get_line() const
union constructor from single element
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Abstract interface to support a programming language.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
static exprt simplify_json_expr(const exprt &src, const namespacet &ns)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
const irep_idt & get_file() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Base class for all expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const std::string & get_string(const irep_namet &name) const
irep_idt get_component_name() const
const irep_idt & get_java_bytecode_index() const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
json_objectt & make_object()
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
json_objectt json(const source_locationt &location)