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/pointer_expr.h>
19 #include <util/simplify_expr.h>
20 #include <util/std_expr.h>
21 
22 #include <util/c_types.h>
23 
25  const exprt &expr,
26  goto_programt &dest,
27  const irep_idt &mode)
28 {
29  const source_locationt source_location=expr.find_source_location();
30 
31  symbolt &new_symbol = get_fresh_aux_symbol(
32  expr.type(),
34  "literal",
35  source_location,
36  mode,
37  symbol_table);
38  new_symbol.is_static_lifetime = lifetime != lifetimet::AUTOMATIC_LOCAL;
39  new_symbol.value=expr;
40 
41  // The value might depend on a variable, thus
42  // generate code for this.
43 
44  symbol_exprt result=new_symbol.symbol_expr();
45  result.add_source_location()=source_location;
46 
47  // The lifetime of compound literals is really that of
48  // the block they are in.
49  if(!new_symbol.is_static_lifetime)
50  copy(code_declt(result), DECL, dest);
51 
52  code_assignt code_assign(result, expr);
53  code_assign.add_source_location()=source_location;
54  convert(code_assign, dest, mode);
55 
56  // now create a 'dead' instruction
57  if(!new_symbol.is_static_lifetime)
58  {
59  code_deadt code_dead(result);
60  targets.destructor_stack.add(std::move(code_dead));
61  }
62 
63  return result;
64 }
65 
67 {
68  if(expr.id()==ID_dereference ||
69  expr.id()==ID_side_effect ||
70  expr.id()==ID_compound_literal ||
71  expr.id()==ID_comma)
72  return true;
73 
74  if(expr.id()==ID_index)
75  {
76  // Will usually clean index expressions because of possible
77  // memory violation in case of out-of-bounds indices.
78  // We do an exception for "string-lit"[0], which is safe.
79  if(to_index_expr(expr).array().id()==ID_string_constant &&
80  to_index_expr(expr).index().is_zero())
81  return false;
82 
83  return true;
84  }
85 
86  // We can't flatten quantified expressions by introducing new literals for
87  // conditional expressions. This is because the body of the quantified
88  // may refer to bound variables, which are not visible outside the scope
89  // of the quantifier.
90  //
91  // For example, the following transformation would not be valid:
92  //
93  // forall (i : int) (i == 0 || i > 10)
94  //
95  // transforming to
96  //
97  // g1 = (i == 0)
98  // g2 = (i > 10)
99  // forall (i : int) (g1 || g2)
100  if(expr.id()==ID_forall || expr.id()==ID_exists)
101  return false;
102 
103  forall_operands(it, expr)
104  if(needs_cleaning(*it))
105  return true;
106 
107  return false;
108 }
109 
112 {
113  PRECONDITION(expr.id() == ID_and || expr.id() == ID_or);
115  expr.is_boolean(),
116  expr.find_source_location(),
117  "'",
118  expr.id(),
119  "' must be Boolean, but got ",
121 
122  // re-write "a && b" into nested a?b:0
123  // re-write "a || b" into nested a?1:b
124 
125  exprt tmp;
126 
127  if(expr.id()==ID_and)
128  tmp=true_exprt();
129  else // ID_or
130  tmp=false_exprt();
131 
132  exprt::operandst &ops=expr.operands();
133 
134  // start with last one
135  for(exprt::operandst::reverse_iterator
136  it=ops.rbegin();
137  it!=ops.rend();
138  ++it)
139  {
140  exprt &op=*it;
141 
143  op.is_boolean(),
144  "boolean operators must have only boolean operands",
145  expr.find_source_location());
146 
147  if(expr.id()==ID_and)
148  {
149  if_exprt if_e(op, tmp, false_exprt());
150  tmp.swap(if_e);
151  }
152  else // ID_or
153  {
154  if_exprt if_e(op, true_exprt(), tmp);
155  tmp.swap(if_e);
156  }
157  }
158 
159  expr.swap(tmp);
160 }
161 
163  exprt &expr,
164  goto_programt &dest,
165  const irep_idt &mode,
166  bool result_is_used)
167 {
168  // this cleans:
169  // && || ?: comma (control-dependency)
170  // function calls
171  // object constructors like arrays, string constants, structs
172  // ++ -- (pre and post)
173  // compound assignments
174  // compound literals
175 
176  if(!needs_cleaning(expr))
177  return;
178 
179  if(expr.id()==ID_and || expr.id()==ID_or)
180  {
181  // rewrite into ?:
182  rewrite_boolean(expr);
183 
184  // recursive call
185  clean_expr(expr, dest, mode, result_is_used);
186  return;
187  }
188  else if(expr.id()==ID_if)
189  {
190  // first clean condition
191  clean_expr(to_if_expr(expr).cond(), dest, mode, true);
192 
193  // possibly done now
194  if(!needs_cleaning(to_if_expr(expr).true_case()) &&
195  !needs_cleaning(to_if_expr(expr).false_case()))
196  return;
197 
198  // copy expression
199  if_exprt if_expr=to_if_expr(expr);
200 
202  if_expr.cond().is_boolean(),
203  "condition for an 'if' must be boolean",
204  if_expr.find_source_location());
205 
206  const source_locationt source_location=expr.find_source_location();
207 
208  #if 0
209  // We do some constant-folding here, to mimic
210  // what typical compilers do.
211  {
212  exprt tmp_cond=if_expr.cond();
213  simplify(tmp_cond, ns);
214  if(tmp_cond.is_true())
215  {
216  clean_expr(if_expr.true_case(), dest, result_is_used);
217  expr=if_expr.true_case();
218  return;
219  }
220  else if(tmp_cond.is_false())
221  {
222  clean_expr(if_expr.false_case(), dest, result_is_used);
223  expr=if_expr.false_case();
224  return;
225  }
226  }
227  #endif
228 
229  goto_programt tmp_true;
230  clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used);
231 
232  goto_programt tmp_false;
233  clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used);
234 
235  if(result_is_used)
236  {
237  symbolt &new_symbol =
238  new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode);
239 
240  code_assignt assignment_true;
241  assignment_true.lhs()=new_symbol.symbol_expr();
242  assignment_true.rhs()=if_expr.true_case();
243  assignment_true.add_source_location()=source_location;
244  convert(assignment_true, tmp_true, mode);
245 
246  code_assignt assignment_false;
247  assignment_false.lhs()=new_symbol.symbol_expr();
248  assignment_false.rhs()=if_expr.false_case();
249  assignment_false.add_source_location()=source_location;
250  convert(assignment_false, tmp_false, mode);
251 
252  // overwrites expr
253  expr=new_symbol.symbol_expr();
254  }
255  else
256  {
257  // preserve the expressions for possible later checks
258  if(if_expr.true_case().is_not_nil())
259  {
260  // add a (void) type cast so that is_skip catches it in case the
261  // expression is just a constant
262  code_expressiont code_expression(
263  typecast_exprt(if_expr.true_case(), empty_typet()));
264  convert(code_expression, tmp_true, mode);
265  }
266 
267  if(if_expr.false_case().is_not_nil())
268  {
269  // add a (void) type cast so that is_skip catches it in case the
270  // expression is just a constant
271  code_expressiont code_expression(
272  typecast_exprt(if_expr.false_case(), empty_typet()));
273  convert(code_expression, tmp_false, mode);
274  }
275 
276  expr=nil_exprt();
277  }
278 
279  // generate guard for argument side-effects
281  if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
282 
283  return;
284  }
285  else if(expr.id()==ID_comma)
286  {
287  if(result_is_used)
288  {
289  exprt result;
290 
291  Forall_operands(it, expr)
292  {
293  bool last=(it==--expr.operands().end());
294 
295  // special treatment for last one
296  if(last)
297  {
298  result.swap(*it);
299  clean_expr(result, dest, mode, true);
300  }
301  else
302  {
303  clean_expr(*it, dest, mode, false);
304 
305  // remember these for later checks
306  if(it->is_not_nil())
307  convert(code_expressiont(*it), dest, mode);
308  }
309  }
310 
311  expr.swap(result);
312  }
313  else // result not used
314  {
315  Forall_operands(it, expr)
316  {
317  clean_expr(*it, dest, mode, false);
318 
319  // remember as expression statement for later checks
320  if(it->is_not_nil())
321  convert(code_expressiont(*it), dest, mode);
322  }
323 
324  expr=nil_exprt();
325  }
326 
327  return;
328  }
329  else if(expr.id()==ID_typecast)
330  {
331  typecast_exprt &typecast = to_typecast_expr(expr);
332 
333  // preserve 'result_is_used'
334  clean_expr(typecast.op(), dest, mode, result_is_used);
335 
336  if(typecast.op().is_nil())
337  expr.make_nil();
338 
339  return;
340  }
341  else if(expr.id()==ID_side_effect)
342  {
343  // some of the side-effects need special treatment!
344  const irep_idt statement=to_side_effect_expr(expr).get_statement();
345 
346  if(statement==ID_gcc_conditional_expression)
347  {
348  // need to do separately
349  remove_gcc_conditional_expression(expr, dest, mode);
350  return;
351  }
352  else if(statement==ID_statement_expression)
353  {
354  // need to do separately to prevent that
355  // the operands of expr get 'cleaned'
357  to_side_effect_expr(expr), dest, mode, result_is_used);
358  return;
359  }
360  else if(statement==ID_assign)
361  {
362  // we do a special treatment for x=f(...)
363  INVARIANT(
364  expr.operands().size() == 2,
365  "side-effect assignment expressions must have two operands");
366 
367  auto &side_effect_assign = to_side_effect_expr_assign(expr);
368 
369  if(
370  side_effect_assign.rhs().id() == ID_side_effect &&
371  to_side_effect_expr(side_effect_assign.rhs()).get_statement() ==
372  ID_function_call)
373  {
374  clean_expr(side_effect_assign.lhs(), dest, mode);
375  exprt lhs = side_effect_assign.lhs();
376 
377  const bool must_use_rhs = needs_cleaning(lhs);
378  if(must_use_rhs)
379  {
381  to_side_effect_expr_function_call(side_effect_assign.rhs()),
382  dest,
383  mode,
384  true);
385  }
386 
387  // turn into code
388  code_assignt assignment;
389  assignment.lhs()=lhs;
390  assignment.rhs() = side_effect_assign.rhs();
391  assignment.add_source_location()=expr.source_location();
392  convert_assign(assignment, dest, mode);
393 
394  if(result_is_used)
395  expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
396  else
397  expr.make_nil();
398  return;
399  }
400  }
401  }
402  else if(expr.id()==ID_forall || expr.id()==ID_exists)
403  {
405  !has_subexpr(expr, ID_side_effect),
406  "the front-end should check quantified expressions for side-effects");
407  }
408  else if(expr.id()==ID_address_of)
409  {
410  address_of_exprt &addr = to_address_of_expr(expr);
411  clean_expr_address_of(addr.object(), dest, mode);
412  return;
413  }
414 
415  // TODO: evaluation order
416 
417  Forall_operands(it, expr)
418  clean_expr(*it, dest, mode);
419 
420  if(expr.id()==ID_side_effect)
421  {
423  to_side_effect_expr(expr), dest, mode, result_is_used, false);
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, 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:1789
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:66
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2187
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:140
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:50
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:209
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:312
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:464
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:162
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:256
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:2087
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:1467
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:344
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:103
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:47
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2124
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:1819
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
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: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
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:111
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:179
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:269
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:522
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
exprt::op1
exprt & op1()
Definition: expr.h:106
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:24
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
irept::swap
void swap(irept &irep)
Definition: irep.h:452
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:2726
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:499
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:680
to_side_effect_expr_assign
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:2066
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1920
source_locationt
Definition: source_location.h:20
simplify_expr.h
irep_pretty_diagnosticst
Definition: irep.h:513
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:2114
DECL
@ DECL
Definition: goto_program.h:48
goto_convertt::targetst::destructor_stack
destructor_treet destructor_stack
Definition: goto_convert_class.h:375
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:1815
PRECONDITION_WITH_DIAGNOSTICS
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:465
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2104
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:74
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:591
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:49
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:237
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1243
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
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:2717
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:65
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:234
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
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842