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