cprover
format_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expression Pretty Printing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "format_expr.h"
13 
14 #include "arith_tools.h"
15 #include "byte_operators.h"
16 #include "format_type.h"
17 #include "ieee_float.h"
18 #include "mathematical_expr.h"
19 #include "mp_arith.h"
20 #include "pointer_expr.h"
21 #include "prefix.h"
22 #include "std_code.h"
23 #include "string_utils.h"
24 
25 #include <map>
26 #include <ostream>
27 
28 // expressions that are rendered with infix operators
29 struct infix_opt
30 {
31  const char *rep;
32 };
33 
34 const std::map<irep_idt, infix_opt> infix_map = {
35  {ID_plus, {"+"}},
36  {ID_minus, {"-"}},
37  {ID_mult, {"*"}},
38  {ID_div, {"/"}},
39  {ID_equal, {"="}},
40  {ID_notequal, {u8"\u2260"}}, // /=, U+2260
41  {ID_and, {u8"\u2227"}}, // wedge, U+2227
42  {ID_or, {u8"\u2228"}}, // vee, U+2228
43  {ID_xor, {u8"\u2295"}}, // + in circle, U+2295
44  {ID_implies, {u8"\u21d2"}}, // =>, U+21D2
45  {ID_le, {u8"\u2264"}}, // <=, U+2264
46  {ID_ge, {u8"\u2265"}}, // >=, U+2265
47  {ID_lt, {"<"}},
48  {ID_gt, {">"}},
49 };
50 
54 static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
55 {
56  // no need for parentheses whenever the subexpression
57  // doesn't have operands
58  if(!sub_expr.has_operands())
59  return false;
60 
61  // no need if subexpression isn't an infix operator
62  if(infix_map.find(sub_expr.id()) == infix_map.end())
63  return false;
64 
65  // * and / bind stronger than + and -
66  if(
67  (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
68  (expr.id() == ID_plus || expr.id() == ID_minus))
69  return false;
70 
71  // ==, !=, <, <=, >, >= bind stronger than && and ||
72  if(
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))
77  return false;
78 
79  // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
80  if(
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))
85  {
86  return false;
87  }
88 
89  return true;
90 }
91 
94 static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
95 {
96  bool first = true;
97 
98  std::string operator_str = id2string(src.id()); // default
99 
100  if(src.id() == ID_equal && to_equal_expr(src).op0().type().id() == ID_bool)
101  {
102  operator_str = u8"\u21d4"; // <=>, U+21D4
103  }
104  else
105  {
106  auto infix_map_it = infix_map.find(src.id());
107  if(infix_map_it != infix_map.end())
108  operator_str = infix_map_it->second.rep;
109  }
110 
111  for(const auto &op : src.operands())
112  {
113  if(first)
114  first = false;
115  else
116  os << ' ' << operator_str << ' ';
117 
118  const bool need_parentheses = bracket_subexpression(op, src);
119 
120  if(need_parentheses)
121  os << '(';
122 
123  os << format(op);
124 
125  if(need_parentheses)
126  os << ')';
127  }
128 
129  return os;
130 }
131 
134 static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
135 {
136  return format_rec(os, to_multi_ary_expr(src));
137 }
138 
141 static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
142 {
143  if(src.id() == ID_not)
144  os << u8"\u00ac"; // neg, U+00AC
145  else if(src.id() == ID_unary_minus)
146  os << '-';
147  else if(src.id() == ID_count_leading_zeros)
148  os << "clz";
149  else if(src.id() == ID_count_trailing_zeros)
150  os << "ctz";
151  else
152  return os << src.pretty();
153 
154  if(src.op().has_operands())
155  return os << '(' << format(src.op()) << ')';
156  else
157  return os << format(src.op());
158 }
159 
161 static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
162 {
163  auto type = src.type().id();
164 
165  if(type == ID_bool)
166  {
167  if(src.is_true())
168  return os << "true";
169  else if(src.is_false())
170  return os << "false";
171  else
172  return os << src.pretty();
173  }
174  else if(
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)
179  return os << src.get_value();
180  else if(type == ID_string)
181  return os << '"' << escape(id2string(src.get_value())) << '"';
182  else if(type == ID_floatbv)
183  return os << ieee_floatt(src);
184  else if(type == ID_pointer)
185  {
186  if(src.is_zero())
187  return os << ID_NULL;
188  else if(has_prefix(id2string(src.get_value()), "INVALID-"))
189  {
190  return os << "INVALID-POINTER";
191  }
192  else if(src.operands().size() == 1)
193  {
194  const auto &unary_expr = to_unary_expr(src);
195  const auto &pointer_type = to_pointer_type(src.type());
196  return os << "pointer(" << format(unary_expr.op()) << ", "
197  << format(pointer_type.subtype()) << ')';
198  }
199  else
200  {
201  const auto &pointer_type = to_pointer_type(src.type());
202  const auto width = pointer_type.get_width();
203  auto int_value = bvrep2integer(src.get_value(), width, false);
204  return os << "pointer(0x" << integer2string(int_value, 16) << ", "
205  << format(pointer_type.subtype()) << ')';
206  }
207  }
208  else
209  return os << src.pretty();
210 }
211 
212 std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
213 {
214  os << expr.id();
215 
216  for(const auto &s : expr.get_named_sub())
217  if(s.first != ID_type)
218  os << ' ' << s.first << "=\"" << s.second.id() << '"';
219 
220  if(expr.has_operands())
221  {
222  os << '(';
223  bool first = true;
224 
225  for(const auto &op : expr.operands())
226  {
227  if(first)
228  first = false;
229  else
230  os << ", ";
231 
232  os << format(op);
233  }
234 
235  os << ')';
236  }
237 
238  return os;
239 }
240 
242 {
243 public:
245  {
246  setup();
247  }
248 
249  using formattert =
250  std::function<std::ostream &(std::ostream &, const exprt &)>;
251  using expr_mapt = std::unordered_map<irep_idt, formattert>;
252 
254 
256  const formattert &find_formatter(const exprt &);
257 
258 private:
260  void setup();
261 
263 };
264 
265 // The below generates textual output in a generic syntax
266 // that is inspired by C/C++/Java, and is meant for debugging
267 // purposes.
269 {
270  auto multi_ary_expr =
271  [](std::ostream &os, const exprt &expr) -> std::ostream & {
272  return format_rec(os, to_multi_ary_expr(expr));
273  };
274 
275  expr_map[ID_plus] = multi_ary_expr;
276  expr_map[ID_mult] = multi_ary_expr;
277  expr_map[ID_and] = multi_ary_expr;
278  expr_map[ID_or] = multi_ary_expr;
279  expr_map[ID_xor] = multi_ary_expr;
280 
281  auto binary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
282  return format_rec(os, to_binary_expr(expr));
283  };
284 
285  expr_map[ID_lt] = binary_expr;
286  expr_map[ID_gt] = binary_expr;
287  expr_map[ID_ge] = binary_expr;
288  expr_map[ID_le] = binary_expr;
289  expr_map[ID_div] = binary_expr;
290  expr_map[ID_minus] = binary_expr;
291  expr_map[ID_implies] = binary_expr;
292  expr_map[ID_equal] = binary_expr;
293  expr_map[ID_notequal] = binary_expr;
294 
295  auto unary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
296  return format_rec(os, to_unary_expr(expr));
297  };
298 
299  expr_map[ID_not] = unary_expr;
300  expr_map[ID_unary_minus] = unary_expr;
301 
302  expr_map[ID_constant] =
303  [](std::ostream &os, const exprt &expr) -> std::ostream & {
304  return format_rec(os, to_constant_expr(expr));
305  };
306 
307  expr_map[ID_typecast] =
308  [](std::ostream &os, const exprt &expr) -> std::ostream & {
309  return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
310  << format(expr.type()) << ')';
311  };
312 
313  auto byte_extract =
314  [](std::ostream &os, const exprt &expr) -> std::ostream & {
315  const auto &byte_extract_expr = to_byte_extract_expr(expr);
316  return os << expr.id() << '(' << format(byte_extract_expr.op()) << ", "
317  << format(byte_extract_expr.offset()) << ", "
318  << format(byte_extract_expr.type()) << ')';
319  };
320 
321  expr_map[ID_byte_extract_little_endian] = byte_extract;
322  expr_map[ID_byte_extract_big_endian] = byte_extract;
323 
324  auto byte_update = [](std::ostream &os, const exprt &expr) -> std::ostream & {
325  const auto &byte_update_expr = to_byte_update_expr(expr);
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()) << ')';
330  };
331 
332  expr_map[ID_byte_update_little_endian] = byte_update;
333  expr_map[ID_byte_update_big_endian] = byte_update;
334 
335  expr_map[ID_member] =
336  [](std::ostream &os, const exprt &expr) -> std::ostream & {
337  return os << format(to_member_expr(expr).op()) << '.'
339  };
340 
341  expr_map[ID_symbol] =
342  [](std::ostream &os, const exprt &expr) -> std::ostream & {
343  return os << to_symbol_expr(expr).get_identifier();
344  };
345 
346  expr_map[ID_index] =
347  [](std::ostream &os, const exprt &expr) -> std::ostream & {
348  const auto &index_expr = to_index_expr(expr);
349  return os << format(index_expr.array()) << '[' << format(index_expr.index())
350  << ']';
351  };
352 
353  expr_map[ID_type] =
354  [](std::ostream &os, const exprt &expr) -> std::ostream & {
355  return format_rec(os, expr.type());
356  };
357 
358  expr_map[ID_forall] =
359  [](std::ostream &os, const exprt &expr) -> std::ostream & {
360  return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
361  << " : " << format(to_quantifier_expr(expr).symbol().type())
362  << " . " << format(to_quantifier_expr(expr).where());
363  };
364 
365  expr_map[ID_exists] =
366  [](std::ostream &os, const exprt &expr) -> std::ostream & {
367  return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
368  << " : " << format(to_quantifier_expr(expr).symbol().type())
369  << " . " << format(to_quantifier_expr(expr).where());
370  };
371 
372  expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
373  return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
374  << format(to_let_expr(expr).value()) << " IN "
375  << format(to_let_expr(expr).where());
376  };
377 
378  expr_map[ID_lambda] =
379  [](std::ostream &os, const exprt &expr) -> std::ostream & {
380  const auto &lambda_expr = to_lambda_expr(expr);
381 
382  os << u8"\u03bb ";
383 
384  bool first = true;
385 
386  for(auto &v : lambda_expr.variables())
387  {
388  if(first)
389  first = false;
390  else
391  os << ", ";
392 
393  os << format(v);
394  }
395 
396  return os << " . " << format(lambda_expr.where());
397  };
398 
399  auto compound = [](std::ostream &os, const exprt &expr) -> std::ostream & {
400  os << "{ ";
401 
402  bool first = true;
403 
404  for(const auto &op : expr.operands())
405  {
406  if(first)
407  first = false;
408  else
409  os << ", ";
410 
411  os << format(op);
412  }
413 
414  return os << " }";
415  };
416 
417  expr_map[ID_array] = compound;
418  expr_map[ID_struct] = compound;
419 
420  expr_map[ID_if] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
421  const auto &if_expr = to_if_expr(expr);
422  return os << '(' << format(if_expr.cond()) << " ? "
423  << format(if_expr.true_case()) << " : "
424  << format(if_expr.false_case()) << ')';
425  };
426 
427  expr_map[ID_code] =
428  [](std::ostream &os, const exprt &expr) -> std::ostream & {
429  const auto &code = to_code(expr);
430  const irep_idt &statement = code.get_statement();
431 
432  if(statement == ID_assign)
433  return os << format(to_code_assign(code).lhs()) << " = "
434  << format(to_code_assign(code).rhs()) << ';';
435  else if(statement == ID_block)
436  {
437  os << '{';
438  for(const auto &s : to_code_block(code).statements())
439  os << ' ' << format(s);
440  return os << " }";
441  }
442  else if(statement == ID_dead)
443  {
444  return os << "dead " << format(to_code_dead(code).symbol()) << ";";
445  }
446  else if(const auto decl = expr_try_dynamic_cast<code_declt>(code))
447  {
448  const auto &declaration_symb = decl->symbol();
449  os << "decl " << format(declaration_symb.type()) << " "
450  << format(declaration_symb);
451  if(const optionalt<exprt> initial_value = decl->initial_value())
452  os << " = " << format(*initial_value);
453  return os << ";";
454  }
455  else if(statement == ID_function_call)
456  {
457  const auto &func_call = to_code_function_call(code);
458  os << to_symbol_expr(func_call.function()).get_identifier() << "(";
459 
460  // Join all our arguments together.
461  join_strings(
462  os,
463  func_call.arguments().begin(),
464  func_call.arguments().end(),
465  ", ",
466  [](const exprt &expr) { return format(expr); });
467 
468  return os << ");";
469  }
470  else
471  return fallback_format_rec(os, expr);
472  };
473 
474  expr_map[ID_string_constant] =
475  [](std::ostream &os, const exprt &expr) -> std::ostream & {
476  return os << '"' << expr.get_string(ID_value) << '"';
477  };
478 
479  expr_map[ID_function_application] =
480  [](std::ostream &os, const exprt &expr) -> std::ostream & {
481  const auto &function_application_expr = to_function_application_expr(expr);
482  os << format(function_application_expr.function()) << '(';
483  bool first = true;
484  for(auto &argument : function_application_expr.arguments())
485  {
486  if(first)
487  first = false;
488  else
489  os << ", ";
490  os << format(argument);
491  }
492  os << ')';
493  return os;
494  };
495 
496  expr_map[ID_dereference] =
497  [](std::ostream &os, const exprt &expr) -> std::ostream & {
498  const auto &dereference_expr = to_dereference_expr(expr);
499  os << '*';
500  if(dereference_expr.pointer().id() != ID_symbol)
501  os << '(' << format(dereference_expr.pointer()) << ')';
502  else
503  os << format(dereference_expr.pointer());
504  return os;
505  };
506 
507  fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
508  return fallback_format_rec(os, expr);
509  };
510 }
511 
514 {
515  auto m_it = expr_map.find(expr.id());
516  if(m_it == expr_map.end())
517  return fallback;
518  else
519  return m_it->second;
520 }
521 
523 
524 std::ostream &format_rec(std::ostream &os, const exprt &expr)
525 {
526  auto &formatter = format_expr_config.find_formatter(expr);
527  return formatter(os, expr);
528 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ieee_floatt
Definition: ieee_float.h:117
format
static format_containert< T > format(const T &o)
Definition: format.h:37
format_expr_configt::fallback
formattert fallback
Definition: format_expr.cpp:262
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_lambda_expr
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Definition: mathematical_expr.h:446
infix_map
const std::map< irep_idt, infix_opt > infix_map
Definition: format_expr.cpp:34
arith_tools.h
mp_arith.h
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
string_utils.h
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
u8
uint64_t u8
Definition: bytecode_info.h:58
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
infix_opt::rep
const char * rep
Definition: format_expr.cpp:31
format_rec
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.
Definition: format_expr.cpp:94
prefix.h
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
format_expr_configt::expr_map
expr_mapt expr_map
Definition: format_expr.cpp:253
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
format_expr_configt
Definition: format_expr.cpp:242
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
infix_opt
Definition: format_expr.cpp:30
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:469
fallback_format_rec
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
Definition: format_expr.cpp:212
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:117
join_strings
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.
Definition: string_utils.h:62
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:549
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3043
format_expr_config
format_expr_configt format_expr_config
Definition: format_expr.cpp:522
pointer_expr.h
API to expression classes for Pointers.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
format_expr_configt::find_formatter
const formattert & find_formatter(const exprt &)
find the formatter for a given expression
Definition: format_expr.cpp:513
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
bracket_subexpression
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),...
Definition: format_expr.cpp:54
format_expr.h
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:314
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
ieee_float.h
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2627
exprt::operands
operandst & operands()
Definition: expr.h:92
format_expr_configt::format_expr_configt
format_expr_configt()
Definition: format_expr.cpp:244
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
format_expr_configt::setup
void setup()
setup the expressions we can format
Definition: format_expr.cpp:268
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:242
format_type.h
format_expr_configt::expr_mapt
std::unordered_map< irep_idt, formattert > expr_mapt
Definition: format_expr.cpp:251
format_expr_configt::formattert
std::function< std::ostream &(std::ostream &, const exprt &)> formattert
Definition: format_expr.cpp:250
escape
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
Definition: string_utils.cpp:138
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103