cprover
Loading...
Searching...
No Matches
format_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expression Pretty Printing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "format_expr.h"
13
14#include "arith_tools.h"
15#include "bitvector_expr.h"
16#include "byte_operators.h"
17#include "expr_util.h"
18#include "floatbv_expr.h"
19#include "format_type.h"
20#include "ieee_float.h"
21#include "mathematical_expr.h"
22#include "mp_arith.h"
23#include "pointer_expr.h"
24#include "string_utils.h"
25
26#include <map>
27#include <ostream>
28
29// expressions that are rendered with infix operators
31{
32 const char *rep;
33};
34
35const std::map<irep_idt, infix_opt> infix_map = {
36 {ID_plus, {"+"}},
37 {ID_minus, {"-"}},
38 {ID_mult, {"*"}},
39 {ID_div, {"/"}},
40 {ID_equal, {"="}},
41 {ID_notequal, {u8"\u2260"}}, // /=, U+2260
42 {ID_and, {u8"\u2227"}}, // wedge, U+2227
43 {ID_or, {u8"\u2228"}}, // vee, U+2228
44 {ID_xor, {u8"\u2295"}}, // + in circle, U+2295
45 {ID_implies, {u8"\u21d2"}}, // =>, U+21D2
46 {ID_le, {u8"\u2264"}}, // <=, U+2264
47 {ID_ge, {u8"\u2265"}}, // >=, U+2265
48 {ID_lt, {"<"}},
49 {ID_gt, {">"}},
50};
51
55static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
56{
57 // no need for parentheses whenever the subexpression
58 // doesn't have operands
59 if(!sub_expr.has_operands())
60 return false;
61
62 // no need if subexpression isn't an infix operator
63 if(infix_map.find(sub_expr.id()) == infix_map.end())
64 return false;
65
66 // * and / bind stronger than + and -
67 if(
68 (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
69 (expr.id() == ID_plus || expr.id() == ID_minus))
70 return false;
71
72 // ==, !=, <, <=, >, >= bind stronger than && and ||
73 if(
74 (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
75 sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
76 sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
77 (expr.id() == ID_and || expr.id() == ID_or))
78 return false;
79
80 // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
81 if(
82 (sub_expr.id() == ID_plus || sub_expr.id() == ID_minus ||
83 sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
84 (expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
85 expr.id() == ID_gt || expr.id() == ID_le || expr.id() == ID_ge))
86 {
87 return false;
88 }
89
90 return true;
91}
92
95static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
96{
97 bool first = true;
98
99 std::string operator_str = id2string(src.id()); // default
100
101 if(src.id() == ID_equal && to_equal_expr(src).op0().is_boolean())
102 {
103 operator_str = u8"\u21d4"; // <=>, U+21D4
104 }
105 else
106 {
107 auto infix_map_it = infix_map.find(src.id());
108 if(infix_map_it != infix_map.end())
109 operator_str = infix_map_it->second.rep;
110 }
111
112 for(const auto &op : src.operands())
113 {
114 if(first)
115 first = false;
116 else
117 os << ' ' << operator_str << ' ';
118
119 const bool need_parentheses = bracket_subexpression(op, src);
120
121 if(need_parentheses)
122 os << '(';
123
124 os << format(op);
125
126 if(need_parentheses)
127 os << ')';
128 }
129
130 return os;
131}
132
135static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
136{
137 return format_rec(os, to_multi_ary_expr(src));
138}
139
142static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
143{
144 if(src.id() == ID_not)
145 os << u8"\u00ac"; // neg, U+00AC
146 else if(src.id() == ID_unary_minus)
147 os << '-';
148 else if(src.id() == ID_count_leading_zeros)
149 os << "clz";
150 else if(src.id() == ID_count_trailing_zeros)
151 os << "ctz";
152 else if(src.id() == ID_find_first_set)
153 os << "ffs";
154 else
155 return os << src.pretty();
156
157 if(src.op().has_operands())
158 return os << '(' << format(src.op()) << ')';
159 else
160 return os << format(src.op());
161}
162
164static std::ostream &format_rec(std::ostream &os, const ternary_exprt &src)
165{
166 os << src.id() << '(' << format(src.op0()) << ", " << format(src.op1())
167 << ", " << format(src.op2()) << ')';
168 return os;
169}
170
172static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
173{
174 auto type = src.type().id();
175
176 if(type == ID_bool)
177 {
178 if(src.is_true())
179 return os << "true";
180 else if(src.is_false())
181 return os << "false";
182 else
183 return os << src.pretty();
184 }
185 else if(
186 type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool ||
187 type == ID_c_bit_field)
188 return os << *numeric_cast<mp_integer>(src);
189 else if(type == ID_bv)
190 {
191 // These do not have a numerical interpretation.
192 // We'll print the 0/1 bit pattern, starting with the bit
193 // that has the highest index. We use vector notation
194 // [...] to avoid confusion with decimal numbers.
195 auto width = to_bv_type(src.type()).get_width();
196 std::string result;
197 result.reserve(width + 2);
198 auto &value = src.get_value();
199 result += '[';
200 for(std::size_t i = 0; i < width; i++)
201 result += get_bvrep_bit(value, width, width - i - 1) ? '1' : '0';
202 result += ']';
203 return os << result;
204 }
205 else if(type == ID_integer || type == ID_natural || type == ID_range)
206 return os << src.get_value();
207 else if(type == ID_string)
208 return os << '"' << escape(id2string(src.get_value())) << '"';
209 else if(type == ID_floatbv)
210 return os << ieee_floatt(src);
211 else if(type == ID_pointer)
212 {
213 if(src.is_null_pointer())
214 return os << ID_NULL;
215 else if(
216 src.get_value() == "INVALID" || src.get_value().starts_with("INVALID-"))
217 {
218 return os << "INVALID-POINTER";
219 }
220 else
221 {
222 const auto &pointer_type = to_pointer_type(src.type());
223 const auto width = pointer_type.get_width();
224 auto int_value = bvrep2integer(src.get_value(), width, false);
225 return os << "pointer(0x" << integer2string(int_value, 16) << ", "
226 << format(pointer_type.base_type()) << ')';
227 }
228 }
229 else if(type == ID_c_enum_tag)
230 {
231 return os << string2integer(id2string(src.get_value()), 16);
232 }
233 else
234 return os << src.pretty();
235}
236
237std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
238{
239 os << expr.id();
240
241 for(const auto &s : expr.get_named_sub())
242 if(s.first != ID_type && s.first != ID_C_source_location)
243 os << ' ' << s.first << "=\"" << s.second.id() << '"';
244
245 if(expr.has_operands())
246 {
247 os << '(';
248 bool first = true;
249
250 for(const auto &op : expr.operands())
251 {
252 if(first)
253 first = false;
254 else
255 os << ", ";
256
257 os << format(op);
258 }
259
260 os << ')';
261 }
262
263 return os;
264}
265
267{
268public:
270 {
271 setup();
272 }
273
275 std::function<std::ostream &(std::ostream &, const exprt &)>;
276 using expr_mapt = std::unordered_map<irep_idt, formattert>;
277
279
281 const formattert &find_formatter(const exprt &);
282
283private:
285 void setup();
286
288};
289
290// The below generates textual output in a generic syntax
291// that is inspired by C/C++/Java, and is meant for debugging
292// purposes.
294{
295 auto multi_ary_expr =
296 [](std::ostream &os, const exprt &expr) -> std::ostream & {
297 return format_rec(os, to_multi_ary_expr(expr));
298 };
299
300 expr_map[ID_plus] = multi_ary_expr;
301 expr_map[ID_mult] = multi_ary_expr;
302 expr_map[ID_and] = multi_ary_expr;
303 expr_map[ID_or] = multi_ary_expr;
304 expr_map[ID_xor] = multi_ary_expr;
305
306 auto binary_infix_expr =
307 [](std::ostream &os, const exprt &expr) -> std::ostream & {
308 return format_rec(os, to_binary_expr(expr));
309 };
310
311 expr_map[ID_lt] = binary_infix_expr;
312 expr_map[ID_gt] = binary_infix_expr;
313 expr_map[ID_ge] = binary_infix_expr;
314 expr_map[ID_le] = binary_infix_expr;
315 expr_map[ID_div] = binary_infix_expr;
316 expr_map[ID_minus] = binary_infix_expr;
317 expr_map[ID_implies] = binary_infix_expr;
318 expr_map[ID_equal] = binary_infix_expr;
319 expr_map[ID_notequal] = binary_infix_expr;
320
321 auto binary_prefix_expr =
322 [](std::ostream &os, const exprt &expr) -> std::ostream & {
323 os << expr.id() << '(' << format(to_binary_expr(expr).op0()) << ", "
324 << format(to_binary_expr(expr).op1()) << ')';
325 return os;
326 };
327
328 expr_map[ID_ieee_float_equal] = binary_prefix_expr;
329 expr_map[ID_ieee_float_notequal] = binary_prefix_expr;
330
331 auto unary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
332 return format_rec(os, to_unary_expr(expr));
333 };
334
335 expr_map[ID_not] = unary_expr;
336 expr_map[ID_unary_minus] = unary_expr;
337
338 auto unary_with_parentheses_expr =
339 [](std::ostream &os, const exprt &expr) -> std::ostream & {
340 return os << expr.id() << '(' << format(to_unary_expr(expr).op()) << ')';
341 };
342
343 expr_map[ID_isnan] = unary_with_parentheses_expr;
344 expr_map[ID_isinf] = unary_with_parentheses_expr;
345 expr_map[ID_isfinite] = unary_with_parentheses_expr;
346 expr_map[ID_isnormal] = unary_with_parentheses_expr;
347
348 auto ternary_expr =
349 [](std::ostream &os, const exprt &expr) -> std::ostream & {
350 return format_rec(os, to_ternary_expr(expr));
351 };
352
353 expr_map[ID_floatbv_plus] = ternary_expr;
354 expr_map[ID_floatbv_minus] = ternary_expr;
355 expr_map[ID_floatbv_mult] = ternary_expr;
356 expr_map[ID_floatbv_div] = ternary_expr;
357 expr_map[ID_floatbv_mod] = ternary_expr;
358
359 expr_map[ID_constant] =
360 [](std::ostream &os, const exprt &expr) -> std::ostream & {
361 return format_rec(os, to_constant_expr(expr));
362 };
363
364 expr_map[ID_address_of] =
365 [](std::ostream &os, const exprt &expr) -> std::ostream & {
366 const auto &address_of = to_address_of_expr(expr);
367 return os << "address_of(" << format(address_of.object()) << ')';
368 };
369
370 expr_map[ID_annotated_pointer_constant] =
371 [](std::ostream &os, const exprt &expr) -> std::ostream & {
372 const auto &annotated_pointer = to_annotated_pointer_constant_expr(expr);
373 return os << format(annotated_pointer.symbolic_pointer());
374 };
375
376 expr_map[ID_typecast] =
377 [](std::ostream &os, const exprt &expr) -> std::ostream & {
378 return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
379 << format(expr.type()) << ')';
380 };
381
382 expr_map[ID_zero_extend] =
383 [](std::ostream &os, const exprt &expr) -> std::ostream & {
384 return os << "zero_extend(" << format(to_zero_extend_expr(expr).op())
385 << ", " << format(expr.type()) << ')';
386 };
387
388 expr_map[ID_floatbv_typecast] =
389 [](std::ostream &os, const exprt &expr) -> std::ostream & {
390 const auto &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
391 return os << "floatbv_typecast(" << format(floatbv_typecast_expr.op())
392 << ", " << format(floatbv_typecast_expr.type()) << ", "
393 << format(floatbv_typecast_expr.rounding_mode()) << ')';
394 };
395
396 auto byte_extract =
397 [](std::ostream &os, const exprt &expr) -> std::ostream & {
398 const auto &byte_extract_expr = to_byte_extract_expr(expr);
399 return os << expr.id() << '(' << format(byte_extract_expr.op()) << ", "
400 << format(byte_extract_expr.offset()) << ", "
401 << format(byte_extract_expr.type()) << ')';
402 };
403
404 expr_map[ID_byte_extract_little_endian] = byte_extract;
405 expr_map[ID_byte_extract_big_endian] = byte_extract;
406
407 auto byte_update = [](std::ostream &os, const exprt &expr) -> std::ostream & {
408 const auto &byte_update_expr = to_byte_update_expr(expr);
409 return os << expr.id() << '(' << format(byte_update_expr.op()) << ", "
410 << format(byte_update_expr.offset()) << ", "
411 << format(byte_update_expr.value()) << ", "
412 << format(byte_update_expr.type()) << ')';
413 };
414
415 expr_map[ID_byte_update_little_endian] = byte_update;
416 expr_map[ID_byte_update_big_endian] = byte_update;
417
418 expr_map[ID_member] =
419 [](std::ostream &os, const exprt &expr) -> std::ostream & {
420 return os << format(to_member_expr(expr).op()) << '.'
422 };
423
424 expr_map[ID_symbol] =
425 [](std::ostream &os, const exprt &expr) -> std::ostream & {
426 return os << to_symbol_expr(expr).get_identifier();
427 };
428
429 expr_map[ID_index] =
430 [](std::ostream &os, const exprt &expr) -> std::ostream & {
431 const auto &index_expr = to_index_expr(expr);
432 return os << format(index_expr.array()) << '[' << format(index_expr.index())
433 << ']';
434 };
435
436 expr_map[ID_type] =
437 [](std::ostream &os, const exprt &expr) -> std::ostream & {
438 return format_rec(os, expr.type());
439 };
440
441 expr_map[ID_forall] =
442 [](std::ostream &os, const exprt &expr) -> std::ostream & {
443 os << u8"\u2200 ";
444 bool first = true;
445 for(const auto &symbol : to_quantifier_expr(expr).variables())
446 {
447 if(first)
448 first = false;
449 else
450 os << ", ";
451 os << format(symbol) << " : " << format(symbol.type());
452 }
453 return os << " . " << format(to_quantifier_expr(expr).where());
454 };
455
456 expr_map[ID_exists] =
457 [](std::ostream &os, const exprt &expr) -> std::ostream & {
458 os << u8"\u2203 ";
459 bool first = true;
460 for(const auto &symbol : to_quantifier_expr(expr).variables())
461 {
462 if(first)
463 first = false;
464 else
465 os << ", ";
466 os << format(symbol) << " : " << format(symbol.type());
467 }
468 return os << " . " << format(to_quantifier_expr(expr).where());
469 };
470
471 expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
472 const auto &let_expr = to_let_expr(expr);
473
474 os << "LET ";
475
476 bool first = true;
477
478 const auto &values = let_expr.values();
479 auto values_it = values.begin();
480 for(auto &v : let_expr.variables())
481 {
482 if(first)
483 first = false;
484 else
485 os << ", ";
486
487 os << format(v) << " = " << format(*values_it);
488 ++values_it;
489 }
490
491 return os << " IN " << format(let_expr.where());
492 };
493
494 expr_map[ID_lambda] =
495 [](std::ostream &os, const exprt &expr) -> std::ostream & {
496 const auto &lambda_expr = to_lambda_expr(expr);
497
498 os << u8"\u03bb ";
499
500 bool first = true;
501
502 for(auto &v : lambda_expr.variables())
503 {
504 if(first)
505 first = false;
506 else
507 os << ", ";
508
509 os << format(v);
510 }
511
512 return os << " . " << format(lambda_expr.where());
513 };
514
515 auto compound = [](std::ostream &os, const exprt &expr) -> std::ostream & {
516 os << "{ ";
517
518 bool first = true;
519
520 for(const auto &op : expr.operands())
521 {
522 if(first)
523 first = false;
524 else
525 os << ", ";
526
527 os << format(op);
528 }
529
530 return os << " }";
531 };
532
533 expr_map[ID_array] = compound;
534 expr_map[ID_struct] = compound;
535
536 expr_map[ID_array_of] =
537 [](std::ostream &os, const exprt &expr) -> std::ostream & {
538 const auto &array_of_expr = to_array_of_expr(expr);
539 return os << "array_of(" << format(array_of_expr.what()) << ')';
540 };
541
542 expr_map[ID_if] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
543 const auto &if_expr = to_if_expr(expr);
544 return os << '(' << format(if_expr.cond()) << " ? "
545 << format(if_expr.true_case()) << " : "
546 << format(if_expr.false_case()) << ')';
547 };
548
549 expr_map[ID_string_constant] =
550 [](std::ostream &os, const exprt &expr) -> std::ostream & {
551 return os << '"' << expr.get_string(ID_value) << '"';
552 };
553
554 expr_map[ID_function_application] =
555 [](std::ostream &os, const exprt &expr) -> std::ostream & {
556 const auto &function_application_expr = to_function_application_expr(expr);
557 os << format(function_application_expr.function()) << '(';
558 bool first = true;
559 for(auto &argument : function_application_expr.arguments())
560 {
561 if(first)
562 first = false;
563 else
564 os << ", ";
565 os << format(argument);
566 }
567 os << ')';
568 return os;
569 };
570
571 expr_map[ID_dereference] =
572 [](std::ostream &os, const exprt &expr) -> std::ostream & {
573 const auto &dereference_expr = to_dereference_expr(expr);
574 os << '*';
575 if(dereference_expr.pointer().id() != ID_symbol)
576 os << '(' << format(dereference_expr.pointer()) << ')';
577 else
578 os << format(dereference_expr.pointer());
579 return os;
580 };
581
582 expr_map[ID_saturating_minus] =
583 [](std::ostream &os, const exprt &expr) -> std::ostream & {
584 const auto &saturating_minus = to_saturating_minus_expr(expr);
585 return os << "saturating-(" << format(saturating_minus.lhs()) << ", "
586 << format(saturating_minus.rhs()) << ')';
587 };
588
589 expr_map[ID_saturating_plus] =
590 [](std::ostream &os, const exprt &expr) -> std::ostream & {
591 const auto &saturating_plus = to_saturating_plus_expr(expr);
592 return os << "saturating+(" << format(saturating_plus.lhs()) << ", "
593 << format(saturating_plus.rhs()) << ')';
594 };
595
596 expr_map[ID_object_address] =
597 [](std::ostream &os, const exprt &expr) -> std::ostream & {
598 const auto &object_address_expr = to_object_address_expr(expr);
599 return os << u8"\u275d" << object_address_expr.object_identifier()
600 << u8"\u275e";
601 };
602
603 expr_map[ID_object_size] =
604 [](std::ostream &os, const exprt &expr) -> std::ostream & {
605 const auto &object_size_expr = to_object_size_expr(expr);
606 return os << "object_size(" << format(object_size_expr.op()) << ')';
607 };
608
609 expr_map[ID_pointer_offset] =
610 [](std::ostream &os, const exprt &expr) -> std::ostream & {
611 const auto &pointer_offset_expr = to_pointer_offset_expr(expr);
612 return os << "pointer_offset(" << format(pointer_offset_expr.op()) << ')';
613 };
614
615 expr_map[ID_field_address] =
616 [](std::ostream &os, const exprt &expr) -> std::ostream & {
617 const auto &field_address_expr = to_field_address_expr(expr);
618 return os << format(field_address_expr.base()) << u8".\u275d"
619 << field_address_expr.component_name() << u8"\u275e";
620 };
621
622 fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
623 return fallback_format_rec(os, expr);
624 };
625}
626
629{
630 auto m_it = expr_map.find(expr.id());
631 if(m_it == expr_map.end())
632 return fallback;
633 else
634 return m_it->second;
635}
636
638
640{
641 format_expr_config.expr_map[id] = std::move(formatter);
642}
643
644std::ostream &format_rec(std::ostream &os, const exprt &expr)
645{
646 auto &formatter = format_expr_config.find_formatter(expr);
647 return formatter(os, expr);
648}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
API to expression classes for bitvectors.
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_exprt.
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
uint64_t u8
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
A base class for binary expressions.
Definition std_expr.h:638
std::size_t get_width() const
Definition std_types.h:925
A constant literal expression.
Definition std_expr.h:2995
const irep_idt & get_value() const
Definition std_expr.h:3003
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
Base class for all expressions.
Definition expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void setup()
setup the expressions we can format
std::unordered_map< irep_idt, formattert > expr_mapt
std::function< std::ostream &(std::ostream &, const exprt &)> formattert
const formattert & find_formatter(const exprt &)
find the formatter for a given expression
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & id() const
Definition irep.h:388
named_subt & get_named_sub()
Definition irep.h:450
irep_idt get_component_name() const
Definition std_expr.h:2871
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
Definition std_expr.h:160
An expression with three operands.
Definition std_expr.h:67
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
static format_containert< T > format(const T &o)
Definition format.h:37
static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
We use the precendences that most readers expect (i.e., the ones you learn in primary school),...
format_expr_configt format_expr_config
const std::map< irep_idt, infix_opt > infix_map
void add_format_hook(irep_idt id, format_expr_configt::formattert formatter)
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
static std::ostream & format_rec(std::ostream &os, const multi_ary_exprt &src)
This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
API to expression classes for Pointers.
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition std_expr.h:116
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3333
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2455
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2941
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3050
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
const char * rep