cprover
goto_clean_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_convert_class.h"
13 
14 #include <util/expr_util.h>
15 #include <util/fresh_symbol.h>
16 #include <util/pointer_expr.h>
17 #include <util/std_expr.h>
18 #include <util/symbol.h>
19 
21  const exprt &expr,
22  goto_programt &dest,
23  const irep_idt &mode)
24 {
25  const source_locationt source_location=expr.find_source_location();
26 
27  symbolt &new_symbol = get_fresh_aux_symbol(
28  expr.type(),
30  "literal",
31  source_location,
32  mode,
33  symbol_table);
34  new_symbol.is_static_lifetime = lifetime != lifetimet::AUTOMATIC_LOCAL;
35  new_symbol.value=expr;
36 
37  // The value might depend on a variable, thus
38  // generate code for this.
39 
40  symbol_exprt result=new_symbol.symbol_expr();
41  result.add_source_location()=source_location;
42 
43  // The lifetime of compound literals is really that of
44  // the block they are in.
45  if(!new_symbol.is_static_lifetime)
46  copy(code_declt(result), DECL, dest);
47 
48  code_assignt code_assign(result, expr);
49  code_assign.add_source_location()=source_location;
50  convert(code_assign, dest, mode);
51 
52  // now create a 'dead' instruction
53  if(!new_symbol.is_static_lifetime)
54  {
55  code_deadt code_dead(result);
56  targets.destructor_stack.add(std::move(code_dead));
57  }
58 
59  return result;
60 }
61 
63 {
64  if(expr.id()==ID_dereference ||
65  expr.id()==ID_side_effect ||
66  expr.id()==ID_compound_literal ||
67  expr.id()==ID_comma)
68  return true;
69 
70  if(expr.id()==ID_index)
71  {
72  // Will usually clean index expressions because of possible
73  // memory violation in case of out-of-bounds indices.
74  // We do an exception for "string-lit"[0], which is safe.
75  if(to_index_expr(expr).array().id()==ID_string_constant &&
76  to_index_expr(expr).index().is_zero())
77  return false;
78 
79  return true;
80  }
81 
82  // We can't flatten quantified expressions by introducing new literals for
83  // conditional expressions. This is because the body of the quantified
84  // may refer to bound variables, which are not visible outside the scope
85  // of the quantifier.
86  //
87  // For example, the following transformation would not be valid:
88  //
89  // forall (i : int) (i == 0 || i > 10)
90  //
91  // transforming to
92  //
93  // g1 = (i == 0)
94  // g2 = (i > 10)
95  // forall (i : int) (g1 || g2)
96  if(expr.id()==ID_forall || expr.id()==ID_exists)
97  return false;
98 
99  forall_operands(it, expr)
100  if(needs_cleaning(*it))
101  return true;
102 
103  return false;
104 }
105 
108 {
109  PRECONDITION(expr.id() == ID_and || expr.id() == ID_or);
111  expr.is_boolean(),
112  expr.find_source_location(),
113  "'",
114  expr.id(),
115  "' must be Boolean, but got ",
117 
118  // re-write "a && b" into nested a?b:0
119  // re-write "a || b" into nested a?1:b
120 
121  exprt tmp;
122 
123  if(expr.id()==ID_and)
124  tmp=true_exprt();
125  else // ID_or
126  tmp=false_exprt();
127 
128  exprt::operandst &ops=expr.operands();
129 
130  // start with last one
131  for(exprt::operandst::reverse_iterator
132  it=ops.rbegin();
133  it!=ops.rend();
134  ++it)
135  {
136  exprt &op=*it;
137 
139  op.is_boolean(),
140  "boolean operators must have only boolean operands",
141  expr.find_source_location());
142 
143  if(expr.id()==ID_and)
144  {
145  if_exprt if_e(op, tmp, false_exprt());
146  tmp.swap(if_e);
147  }
148  else // ID_or
149  {
150  if_exprt if_e(op, true_exprt(), tmp);
151  tmp.swap(if_e);
152  }
153  }
154 
155  expr.swap(tmp);
156 }
157 
159  exprt &expr,
160  goto_programt &dest,
161  const irep_idt &mode,
162  bool result_is_used)
163 {
164  // this cleans:
165  // && || ?: comma (control-dependency)
166  // function calls
167  // object constructors like arrays, string constants, structs
168  // ++ -- (pre and post)
169  // compound assignments
170  // compound literals
171 
172  if(!needs_cleaning(expr))
173  return;
174 
175  if(expr.id()==ID_and || expr.id()==ID_or)
176  {
177  // rewrite into ?:
178  rewrite_boolean(expr);
179 
180  // recursive call
181  clean_expr(expr, dest, mode, result_is_used);
182  return;
183  }
184  else if(expr.id()==ID_if)
185  {
186  // first clean condition
187  clean_expr(to_if_expr(expr).cond(), dest, mode, true);
188 
189  // possibly done now
190  if(!needs_cleaning(to_if_expr(expr).true_case()) &&
191  !needs_cleaning(to_if_expr(expr).false_case()))
192  return;
193 
194  // copy expression
195  if_exprt if_expr=to_if_expr(expr);
196 
198  if_expr.cond().is_boolean(),
199  "condition for an 'if' must be boolean",
200  if_expr.find_source_location());
201 
202  const source_locationt source_location=expr.find_source_location();
203 
204  #if 0
205  // We do some constant-folding here, to mimic
206  // what typical compilers do.
207  {
208  exprt tmp_cond=if_expr.cond();
209  simplify(tmp_cond, ns);
210  if(tmp_cond.is_true())
211  {
212  clean_expr(if_expr.true_case(), dest, result_is_used);
213  expr=if_expr.true_case();
214  return;
215  }
216  else if(tmp_cond.is_false())
217  {
218  clean_expr(if_expr.false_case(), dest, result_is_used);
219  expr=if_expr.false_case();
220  return;
221  }
222  }
223  #endif
224 
225  goto_programt tmp_true;
226  clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used);
227 
228  goto_programt tmp_false;
229  clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used);
230 
231  if(result_is_used)
232  {
233  symbolt &new_symbol =
234  new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode);
235 
236  code_assignt assignment_true;
237  assignment_true.lhs()=new_symbol.symbol_expr();
238  assignment_true.rhs()=if_expr.true_case();
239  assignment_true.add_source_location()=source_location;
240  convert(assignment_true, tmp_true, mode);
241 
242  code_assignt assignment_false;
243  assignment_false.lhs()=new_symbol.symbol_expr();
244  assignment_false.rhs()=if_expr.false_case();
245  assignment_false.add_source_location()=source_location;
246  convert(assignment_false, tmp_false, mode);
247 
248  // overwrites expr
249  expr=new_symbol.symbol_expr();
250  }
251  else
252  {
253  // preserve the expressions for possible later checks
254  if(if_expr.true_case().is_not_nil())
255  {
256  // add a (void) type cast so that is_skip catches it in case the
257  // expression is just a constant
258  code_expressiont code_expression(
259  typecast_exprt(if_expr.true_case(), empty_typet()));
260  convert(code_expression, tmp_true, mode);
261  }
262 
263  if(if_expr.false_case().is_not_nil())
264  {
265  // add a (void) type cast so that is_skip catches it in case the
266  // expression is just a constant
267  code_expressiont code_expression(
268  typecast_exprt(if_expr.false_case(), empty_typet()));
269  convert(code_expression, tmp_false, mode);
270  }
271 
272  expr=nil_exprt();
273  }
274 
275  // generate guard for argument side-effects
277  if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
278 
279  return;
280  }
281  else if(expr.id()==ID_comma)
282  {
283  if(result_is_used)
284  {
285  exprt result;
286 
287  Forall_operands(it, expr)
288  {
289  bool last=(it==--expr.operands().end());
290 
291  // special treatment for last one
292  if(last)
293  {
294  result.swap(*it);
295  clean_expr(result, dest, mode, true);
296  }
297  else
298  {
299  clean_expr(*it, dest, mode, false);
300 
301  // remember these for later checks
302  if(it->is_not_nil())
303  convert(code_expressiont(*it), dest, mode);
304  }
305  }
306 
307  expr.swap(result);
308  }
309  else // result not used
310  {
311  Forall_operands(it, expr)
312  {
313  clean_expr(*it, dest, mode, false);
314 
315  // remember as expression statement for later checks
316  if(it->is_not_nil())
317  convert(code_expressiont(*it), dest, mode);
318  }
319 
320  expr=nil_exprt();
321  }
322 
323  return;
324  }
325  else if(expr.id()==ID_typecast)
326  {
327  typecast_exprt &typecast = to_typecast_expr(expr);
328 
329  // preserve 'result_is_used'
330  clean_expr(typecast.op(), dest, mode, result_is_used);
331 
332  if(typecast.op().is_nil())
333  expr.make_nil();
334 
335  return;
336  }
337  else if(expr.id()==ID_side_effect)
338  {
339  // some of the side-effects need special treatment!
340  const irep_idt statement=to_side_effect_expr(expr).get_statement();
341 
342  if(statement==ID_gcc_conditional_expression)
343  {
344  // need to do separately
345  remove_gcc_conditional_expression(expr, dest, mode);
346  return;
347  }
348  else if(statement==ID_statement_expression)
349  {
350  // need to do separately to prevent that
351  // the operands of expr get 'cleaned'
353  to_side_effect_expr(expr), dest, mode, result_is_used);
354  return;
355  }
356  else if(statement==ID_assign)
357  {
358  // we do a special treatment for x=f(...)
359  INVARIANT(
360  expr.operands().size() == 2,
361  "side-effect assignment expressions must have two operands");
362 
363  auto &side_effect_assign = to_side_effect_expr_assign(expr);
364 
365  if(
366  side_effect_assign.rhs().id() == ID_side_effect &&
367  to_side_effect_expr(side_effect_assign.rhs()).get_statement() ==
368  ID_function_call)
369  {
370  clean_expr(side_effect_assign.lhs(), dest, mode);
371  exprt lhs = side_effect_assign.lhs();
372 
373  const bool must_use_rhs = needs_cleaning(lhs);
374  if(must_use_rhs)
375  {
377  to_side_effect_expr_function_call(side_effect_assign.rhs()),
378  dest,
379  mode,
380  true);
381  }
382 
383  // turn into code
384  code_assignt assignment;
385  assignment.lhs()=lhs;
386  assignment.rhs() = side_effect_assign.rhs();
387  assignment.add_source_location()=expr.source_location();
388  convert_assign(assignment, dest, mode);
389 
390  if(result_is_used)
391  expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
392  else
393  expr.make_nil();
394  return;
395  }
396  }
397  }
398  else if(expr.id()==ID_forall || expr.id()==ID_exists)
399  {
401  !has_subexpr(expr, ID_side_effect),
402  "the front-end should check quantified expressions for side-effects");
403  }
404  else if(expr.id()==ID_address_of)
405  {
406  address_of_exprt &addr = to_address_of_expr(expr);
407  clean_expr_address_of(addr.object(), dest, mode);
408  return;
409  }
410 
411  // TODO: evaluation order
412 
413  Forall_operands(it, expr)
414  clean_expr(*it, dest, mode);
415 
416  if(expr.id()==ID_side_effect)
417  {
419  to_side_effect_expr(expr), dest, mode, result_is_used, false);
420  }
421  else if(expr.id()==ID_compound_literal)
422  {
423  // This is simply replaced by the literal
425  expr.operands().size() == 1, "ID_compound_literal has a single operand");
426  expr = to_unary_expr(expr).op();
427  }
428 }
429 
431  exprt &expr,
432  goto_programt &dest,
433  const irep_idt &mode)
434 {
435  // The address of object constructors can be taken,
436  // which is re-written into the address of a variable.
437 
438  if(expr.id()==ID_compound_literal)
439  {
441  expr.operands().size() == 1, "ID_compound_literal has a single operand");
442  clean_expr(to_unary_expr(expr).op(), dest, mode);
443  expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode);
444  }
445  else if(expr.id()==ID_string_constant)
446  {
447  // Leave for now, but long-term these might become static symbols.
448  // LLVM appears to do precisely that.
449  }
450  else if(expr.id()==ID_index)
451  {
452  index_exprt &index_expr = to_index_expr(expr);
453  clean_expr_address_of(index_expr.array(), dest, mode);
454  clean_expr(index_expr.index(), dest, mode);
455  }
456  else if(expr.id()==ID_dereference)
457  {
458  dereference_exprt &deref_expr = to_dereference_expr(expr);
459  clean_expr(deref_expr.pointer(), dest, mode);
460  }
461  else if(expr.id()==ID_comma)
462  {
463  // Yes, one can take the address of a comma expression.
464  // Treatment is similar to clean_expr() above.
465 
466  exprt result;
467 
468  Forall_operands(it, expr)
469  {
470  bool last=(it==--expr.operands().end());
471 
472  // special treatment for last one
473  if(last)
474  result.swap(*it);
475  else
476  {
477  clean_expr(*it, dest, mode, false);
478 
479  // get any side-effects
480  if(it->is_not_nil())
481  convert(code_expressiont(*it), dest, mode);
482  }
483  }
484 
485  expr.swap(result);
486 
487  // do again
488  clean_expr_address_of(expr, dest, mode);
489  }
490  else if(expr.id() == ID_side_effect)
491  {
492  remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true);
493  }
494  else
495  Forall_operands(it, expr)
496  clean_expr_address_of(*it, dest, mode);
497 }
498 
500  exprt &expr,
501  goto_programt &dest,
502  const irep_idt &mode)
503 {
504  {
505  auto &binary_expr = to_binary_expr(expr);
506 
507  // first remove side-effects from condition
508  clean_expr(to_binary_expr(expr).op0(), dest, mode);
509 
510  // now we can copy op0 safely
511  if_exprt if_expr(
512  typecast_exprt::conditional_cast(binary_expr.op0(), bool_typet()),
513  binary_expr.op0(),
514  binary_expr.op1(),
515  expr.type());
516  if_expr.add_source_location() = expr.source_location();
517 
518  expr.swap(if_expr);
519  }
520 
521  // there might still be junk in expr.op2()
522  clean_expr(expr, dest, mode);
523 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:62
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:137
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:52
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
goto_convertt::convert
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
Definition: goto_convert.cpp:429
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:299
irept::make_nil
void make_nil()
Definition: irep.h:465
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:315
fresh_symbol.h
Fresh auxiliary symbol creation.
goto_convertt::clean_expr
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
Definition: goto_clean_expr.cpp:158
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
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
goto_convertt::remove_gcc_conditional_expression
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest, const irep_idt &mode)
Definition: goto_clean_expr.cpp:499
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:53
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
goto_convert_class.h
Program Transformation.
goto_convertt::generate_ifthenelse
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
Definition: goto_convert.cpp:1480
goto_convertt::remove_function_call
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:345
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:99
bool_typet
The Boolean type.
Definition: std_types.h:36
goto_convertt::clean_expr_address_of
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
Definition: goto_clean_expr.cpp:430
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
goto_convertt::new_tmp_symbol
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
Definition: goto_convert.cpp:1832
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
goto_convertt::targets
struct goto_convertt::targetst targets
destructor_treet::add
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
Definition: destructor_tree.cpp:11
messaget::result
mstreamt & result() const
Definition: message.h:409
empty_typet
The empty type.
Definition: std_types.h:51
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
goto_convertt::rewrite_boolean
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
Definition: goto_clean_expr.cpp:107
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:641
goto_convertt::remove_statement_expression
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:523
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2654
exprt::op1
exprt & op1()
Definition: expr.h:102
goto_convertt::make_compound_literal
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
Definition: goto_clean_expr.cpp:20
index_exprt::index
exprt & index()
Definition: std_expr.h:1354
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
irept::swap
void swap(irept &irep)
Definition: irep.h:453
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:497
goto_convertt::convert_assign
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:680
to_side_effect_expr_assign
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:2064
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1918
source_locationt
Definition: source_location.h:19
irep_pretty_diagnosticst
Definition: irep.h:514
expr_util.h
Deprecated expression utility functions.
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
DECL
@ DECL
Definition: goto_program.h:45
goto_convertt::targetst::destructor_stack
destructor_treet destructor_stack
Definition: goto_convert_class.h:381
symbolt
Symbol table entry.
Definition: symbol.h:28
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
PRECONDITION_WITH_DIAGNOSTICS
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2189
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_convertt::remove_side_effect
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
Definition: goto_convert_side_effect.cpp:690
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:51
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
exprt::operands
operandst & operands()
Definition: expr.h:92
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
std_expr.h
API to expression classes.
goto_convertt::lifetime
lifetimet lifetime
Definition: goto_convert_class.h:54
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1840