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