Go to the documentation of this file.
40 {ID_notequal, {
u8"\u2260"}},
41 {ID_and, {
u8"\u2227"}},
42 {ID_or, {
u8"\u2228"}},
43 {ID_xor, {
u8"\u2295"}},
44 {ID_implies, {
u8"\u21d2"}},
45 {ID_le, {
u8"\u2264"}},
46 {ID_ge, {
u8"\u2265"}},
67 (sub_expr.
id() == ID_mult || sub_expr.
id() == ID_div) &&
68 (expr.
id() == ID_plus || expr.
id() == ID_minus))
73 (sub_expr.
id() == ID_equal || sub_expr.
id() == ID_notequal ||
74 sub_expr.
id() == ID_lt || sub_expr.
id() == ID_gt ||
75 sub_expr.
id() == ID_le || sub_expr.
id() == ID_ge) &&
76 (expr.
id() == ID_and || expr.
id() == ID_or))
81 (sub_expr.
id() == ID_plus || sub_expr.
id() == ID_minus ||
82 sub_expr.
id() == ID_mult || sub_expr.
id() == ID_div) &&
83 (expr.
id() == ID_equal || expr.
id() == ID_notequal || expr.
id() == ID_lt ||
84 expr.
id() == ID_gt || expr.
id() == ID_le || expr.
id() == ID_ge))
100 if(src.
id() == ID_equal &&
to_equal_expr(src).op0().type().
id() == ID_bool)
102 operator_str =
u8"\u21d4";
108 operator_str = infix_map_it->second.rep;
111 for(
const auto &op : src.
operands())
116 os <<
' ' << operator_str <<
' ';
143 if(src.
id() == ID_not)
145 else if(src.
id() == ID_unary_minus)
147 else if(src.
id() == ID_count_leading_zeros)
149 else if(src.
id() == ID_count_trailing_zeros)
152 return os << src.
pretty();
155 return os <<
'(' <<
format(src.
op()) <<
')';
163 auto type = src.
type().
id();
170 return os <<
"false";
172 return os << src.
pretty();
175 type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool ||
176 type == ID_c_bit_field)
177 return os << *numeric_cast<mp_integer>(src);
178 else if(type == ID_integer)
180 else if(type == ID_string)
182 else if(type == ID_floatbv)
184 else if(type == ID_pointer)
187 return os << ID_NULL;
190 return os <<
"INVALID-POINTER";
196 return os <<
"pointer(" <<
format(unary_expr.op()) <<
", "
204 return os <<
"pointer(0x" <<
integer2string(int_value, 16) <<
", "
209 return os << src.
pretty();
217 if(s.first != ID_type)
218 os <<
' ' << s.first <<
"=\"" << s.second.id() <<
'"';
225 for(
const auto &op : expr.
operands())
250 std::function<std::ostream &(std::ostream &,
const exprt &)>;
251 using expr_mapt = std::unordered_map<irep_idt, formattert>;
270 auto multi_ary_expr =
271 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
281 auto binary_expr = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
293 expr_map[ID_notequal] = binary_expr;
295 auto unary_expr = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
300 expr_map[ID_unary_minus] = unary_expr;
303 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
308 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
310 <<
format(expr.type()) <<
')';
314 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
316 return os << expr.id() <<
'(' <<
format(byte_extract_expr.op()) <<
", "
317 <<
format(byte_extract_expr.offset()) <<
", "
318 <<
format(byte_extract_expr.type()) <<
')';
321 expr_map[ID_byte_extract_little_endian] = byte_extract;
322 expr_map[ID_byte_extract_big_endian] = byte_extract;
324 auto byte_update = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
326 return os << expr.id() <<
'(' <<
format(byte_update_expr.op()) <<
", "
327 <<
format(byte_update_expr.offset()) <<
", "
328 <<
format(byte_update_expr.value()) <<
", "
329 <<
format(byte_update_expr.type()) <<
')';
332 expr_map[ID_byte_update_little_endian] = byte_update;
333 expr_map[ID_byte_update_big_endian] = byte_update;
336 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
342 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
347 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
349 return os <<
format(index_expr.array()) <<
'[' <<
format(index_expr.index())
354 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
359 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
366 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
372 expr_map[ID_let] = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
379 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
386 for(
auto &v : lambda_expr.variables())
396 return os <<
" . " <<
format(lambda_expr.where());
399 auto compound = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
404 for(
const auto &op : expr.operands())
420 expr_map[ID_if] = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
422 return os <<
'(' <<
format(if_expr.cond()) <<
" ? "
423 <<
format(if_expr.true_case()) <<
" : "
424 <<
format(if_expr.false_case()) <<
')';
428 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
429 const auto &code =
to_code(expr);
430 const irep_idt &statement = code.get_statement();
432 if(statement == ID_assign)
435 else if(statement == ID_block)
442 else if(statement == ID_dead)
446 else if(
const auto decl = expr_try_dynamic_cast<code_declt>(code))
448 const auto &declaration_symb = decl->symbol();
449 os <<
"decl " <<
format(declaration_symb.type()) <<
" "
450 <<
format(declaration_symb);
452 os <<
" = " <<
format(*initial_value);
455 else if(statement == ID_function_call)
463 func_call.arguments().begin(),
464 func_call.arguments().end(),
466 [](
const exprt &expr) { return format(expr); });
475 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
476 return os <<
'"' << expr.get_string(ID_value) <<
'"';
480 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
482 os <<
format(function_application_expr.function()) <<
'(';
484 for(
auto &argument : function_application_expr.arguments())
497 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
500 if(dereference_expr.pointer().id() != ID_symbol)
501 os <<
'(' <<
format(dereference_expr.pointer()) <<
')';
503 os <<
format(dereference_expr.pointer());
507 fallback = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
527 return formatter(os, expr);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
A base class for multi-ary expressions Associativity is not specified.
const typet & subtype() const
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Base class for all expressions.
Generic base class for unary expressions.
A base class for binary expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
typet & type()
Return the type of the expression.
Expression classes for byte-level operators.
bool has_prefix(const std::string &s, const std::string &prefix)
bool has_operands() const
Return true if there is at least one operand.
const std::string & id2string(const irep_idt &d)
named_subt & get_named_sub()
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
nonstd::optional< T > optionalt
std::size_t get_width() const
bool is_zero() const
Return whether the expression is a constant representing 0.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const code_assignt & to_code_assign(const codet &code)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const code_blockt & to_code_block(const codet &code)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
A constant literal expression.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const irep_idt & get_value() const
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
API to expression classes for 'mathematical' expressions.
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)