cprover
goto_convert_side_effect.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/arith_tools.h>
15 #include <util/cprover_prefix.h>
16 #include <util/expr_util.h>
17 #include <util/fresh_symbol.h>
18 #include <util/std_expr.h>
19 #include <util/symbol.h>
20 
21 #include <util/c_types.h>
22 
24 {
25  forall_operands(it, expr)
26  if(has_function_call(*it))
27  return true;
28 
29  if(expr.id()==ID_side_effect &&
30  expr.get(ID_statement)==ID_function_call)
31  return true;
32 
33  return false;
34 }
35 
37  side_effect_exprt &expr,
38  goto_programt &dest,
39  bool result_is_used,
40  const irep_idt &mode)
41 {
42  const irep_idt statement=expr.get_statement();
43 
44  if(statement==ID_assign)
45  {
46  exprt tmp=expr;
47  tmp.id(ID_code);
48  // just interpret as code
49  convert_assign(to_code_assign(to_code(tmp)), dest, mode);
50  }
51  else if(statement==ID_assign_plus ||
52  statement==ID_assign_minus ||
53  statement==ID_assign_mult ||
54  statement==ID_assign_div ||
55  statement==ID_assign_mod ||
56  statement==ID_assign_shl ||
57  statement==ID_assign_ashr ||
58  statement==ID_assign_lshr ||
59  statement==ID_assign_bitand ||
60  statement==ID_assign_bitxor ||
61  statement==ID_assign_bitor)
62  {
63  if(expr.operands().size()!=2)
64  {
66  error() << statement << " takes two arguments" << eom;
67  throw 0;
68  }
69 
70  irep_idt new_id;
71 
72  if(statement==ID_assign_plus)
73  new_id=ID_plus;
74  else if(statement==ID_assign_minus)
75  new_id=ID_minus;
76  else if(statement==ID_assign_mult)
77  new_id=ID_mult;
78  else if(statement==ID_assign_div)
79  new_id=ID_div;
80  else if(statement==ID_assign_mod)
81  new_id=ID_mod;
82  else if(statement==ID_assign_shl)
83  new_id=ID_shl;
84  else if(statement==ID_assign_ashr)
85  new_id=ID_ashr;
86  else if(statement==ID_assign_lshr)
87  new_id=ID_lshr;
88  else if(statement==ID_assign_bitand)
89  new_id=ID_bitand;
90  else if(statement==ID_assign_bitxor)
91  new_id=ID_bitxor;
92  else if(statement==ID_assign_bitor)
93  new_id=ID_bitor;
94  else
95  {
97  error() << "assignment `" << statement << "' not yet supported"
98  << eom;
99  throw 0;
100  }
101 
102  exprt rhs;
103 
104  const typet &op0_type=ns.follow(expr.op0().type());
105 
106  // C/C++ Booleans get very special treatment.
107  if(op0_type.id()==ID_c_bool)
108  {
109  binary_exprt tmp(expr.op0(), new_id, expr.op1(), expr.op1().type());
110  tmp.op0().make_typecast(expr.op1().type());
111  rhs=typecast_exprt(is_not_zero(tmp, ns), expr.op0().type());
112  }
113  else
114  {
115  rhs.id(new_id);
116  rhs.copy_to_operands(expr.op0(), expr.op1());
117  rhs.type()=expr.op0().type();
119  }
120 
121  code_assignt assignment(expr.op0(), rhs);
122  assignment.add_source_location()=expr.source_location();
123 
124  convert(assignment, dest, mode);
125  }
126  else
127  UNREACHABLE;
128 
129  // revert assignment in the expression to its LHS
130  if(result_is_used)
131  {
132  exprt lhs;
133  lhs.swap(expr.op0());
134  expr.swap(lhs);
135  }
136  else
137  expr.make_nil();
138 }
139 
141  side_effect_exprt &expr,
142  goto_programt &dest,
143  bool result_is_used,
144  const irep_idt &mode)
145 {
146  if(expr.operands().size()!=1)
147  {
149  error() << "preincrement/predecrement must have one operand" << eom;
150  throw 0;
151  }
152 
153  const irep_idt statement=expr.get_statement();
154 
155  assert(statement==ID_preincrement ||
156  statement==ID_predecrement);
157 
158  exprt rhs;
160 
161  if(statement==ID_preincrement)
162  rhs.id(ID_plus);
163  else
164  rhs.id(ID_minus);
165 
166  const typet &op_type=ns.follow(expr.op0().type());
167 
168  if(op_type.id()==ID_bool)
169  {
172  rhs.type()=signed_int_type();
173  rhs=is_not_zero(rhs, ns);
174  }
175  else if(op_type.id()==ID_c_bool)
176  {
179  rhs.type()=signed_int_type();
180  rhs=is_not_zero(rhs, ns);
181  rhs.make_typecast(op_type);
182  }
183  else if(op_type.id()==ID_c_enum ||
184  op_type.id()==ID_c_enum_tag)
185  {
188  rhs.type()=signed_int_type();
189  rhs.make_typecast(op_type);
190  }
191  else
192  {
193  typet constant_type;
194 
195  if(op_type.id()==ID_pointer)
196  constant_type=index_type();
197  else if(is_number(op_type) || op_type.id()==ID_c_bool)
198  constant_type=op_type;
199  else
200  {
202  error() << "no constant one of type " << op_type.pretty() << eom;
203  throw 0;
204  }
205 
206  exprt constant=from_integer(1, constant_type);
207 
208  rhs.copy_to_operands(expr.op0());
209  rhs.move_to_operands(constant);
210  rhs.type()=expr.op0().type();
211  }
212 
213  code_assignt assignment(expr.op0(), rhs);
214  assignment.add_source_location()=expr.find_source_location();
215 
216  convert(assignment, dest, mode);
217 
218  if(result_is_used)
219  {
220  // revert to argument of pre-inc/pre-dec
221  exprt tmp=expr.op0();
222  expr.swap(tmp);
223  }
224  else
225  expr.make_nil();
226 }
227 
229  side_effect_exprt &expr,
230  goto_programt &dest,
231  const irep_idt &mode,
232  bool result_is_used)
233 {
234  goto_programt tmp1, tmp2;
235 
236  // we have ...(op++)...
237 
238  if(expr.operands().size()!=1)
239  {
241  error() << "postincrement/postdecrement must have one operand"
242  << eom;
243  throw 0;
244  }
245 
246  const irep_idt statement=expr.get_statement();
247 
248  assert(statement==ID_postincrement ||
249  statement==ID_postdecrement);
250 
251  exprt rhs;
253 
254  if(statement==ID_postincrement)
255  rhs.id(ID_plus);
256  else
257  rhs.id(ID_minus);
258 
259  const typet &op_type=ns.follow(expr.op0().type());
260 
261  if(op_type.id()==ID_bool)
262  {
265  rhs.type()=signed_int_type();
266  rhs=is_not_zero(rhs, ns);
267  }
268  else if(op_type.id()==ID_c_bool)
269  {
272  rhs.type()=signed_int_type();
273  rhs=is_not_zero(rhs, ns);
274  rhs.make_typecast(op_type);
275  }
276  else if(op_type.id()==ID_c_enum ||
277  op_type.id()==ID_c_enum_tag)
278  {
281  rhs.type()=signed_int_type();
282  rhs.make_typecast(op_type);
283  }
284  else
285  {
286  typet constant_type;
287 
288  if(op_type.id()==ID_pointer)
289  constant_type=index_type();
290  else if(is_number(op_type) || op_type.id()==ID_c_bool)
291  constant_type=op_type;
292  else
293  {
295  error() << "no constant one of type " << op_type.pretty() << eom;
296  throw 0;
297  }
298 
299  exprt constant;
300 
301  if(constant_type.id()==ID_complex)
302  {
303  exprt real=from_integer(1, constant_type.subtype());
304  exprt imag=from_integer(0, constant_type.subtype());
305  constant=complex_exprt(real, imag, to_complex_type(constant_type));
306  }
307  else
308  constant=from_integer(1, constant_type);
309 
310  rhs.copy_to_operands(expr.op0());
311  rhs.move_to_operands(constant);
312  rhs.type()=expr.op0().type();
313  }
314 
315  code_assignt assignment(expr.op0(), rhs);
316  assignment.add_source_location()=expr.find_source_location();
317 
318  convert(assignment, tmp2, mode);
319 
320  // fix up the expression, if needed
321 
322  if(result_is_used)
323  {
324  exprt tmp=expr.op0();
325  make_temp_symbol(tmp, "post", dest, mode);
326  expr.swap(tmp);
327  }
328  else
329  expr.make_nil();
330 
331  dest.destructive_append(tmp1);
332  dest.destructive_append(tmp2);
333 }
334 
336  side_effect_exprt &expr,
337  goto_programt &dest,
338  const irep_idt &mode,
339  bool result_is_used)
340 {
341  if(!result_is_used)
342  {
343  assert(expr.operands().size()==2);
344  code_function_callt call;
345  call.function()=expr.op0();
346  call.arguments()=expr.op1().operands();
347  call.add_source_location()=expr.source_location();
348  call.lhs().make_nil();
349  convert_function_call(call, dest, mode);
350  expr.make_nil();
351  return;
352  }
353 
354  // get name of function, if available
355 
356  if(expr.id()!=ID_side_effect ||
357  expr.get(ID_statement)!=ID_function_call)
358  {
360  error() << "expected function call" << eom;
361  throw 0;
362  }
363 
364  if(expr.operands().empty())
365  {
367  error() << "function_call expects at least one operand" << eom;
368  throw 0;
369  }
370 
371  std::string new_base_name = "return_value";
372  irep_idt new_symbol_mode = mode;
373 
374  if(expr.op0().id()==ID_symbol)
375  {
376  const irep_idt &identifier = to_symbol_expr(expr.op0()).get_identifier();
377  const symbolt &symbol = ns.lookup(identifier);
378 
379  new_base_name+='_';
380  new_base_name+=id2string(symbol.base_name);
381  new_symbol_mode = symbol.mode;
382  }
383 
384  const symbolt &new_symbol = get_fresh_aux_symbol(
385  expr.type(),
387  new_base_name,
388  expr.find_source_location(),
389  new_symbol_mode,
390  symbol_table);
391 
392  {
393  code_declt decl;
394  decl.symbol()=new_symbol.symbol_expr();
395  decl.add_source_location()=new_symbol.location;
396  convert_decl(decl, dest, mode);
397  }
398 
399  {
400  goto_programt tmp_program2;
401  code_function_callt call;
402  call.lhs()=new_symbol.symbol_expr();
403  call.function()=expr.op0();
404  call.arguments()=expr.op1().operands();
405  call.add_source_location()=new_symbol.location;
406  convert_function_call(call, dest, mode);
407  }
408 
409  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
410 }
411 
413  const exprt &object,
414  exprt &dest)
415 {
416  if(dest.id()=="new_object")
417  dest=object;
418  else
419  Forall_operands(it, dest)
420  replace_new_object(object, *it);
421 }
422 
424  side_effect_exprt &expr,
425  goto_programt &dest,
426  bool result_is_used)
427 {
428  codet call;
429 
430  const symbolt &new_symbol = get_fresh_aux_symbol(
431  expr.type(),
433  "new_ptr",
434  expr.find_source_location(),
435  ID_cpp,
436  symbol_table);
437 
438  code_declt decl;
439  decl.symbol()=new_symbol.symbol_expr();
440  decl.add_source_location()=new_symbol.location;
441  convert_decl(decl, dest, ID_cpp);
442 
443  call=code_assignt(new_symbol.symbol_expr(), expr);
444 
445  if(result_is_used)
446  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
447  else
448  expr.make_nil();
449 
450  convert(call, dest, ID_cpp);
451 }
452 
454  side_effect_exprt &expr,
455  goto_programt &dest,
456  bool result_is_used)
457 {
458  assert(expr.operands().size()==1);
459 
460  codet tmp;
461 
462  tmp.set_statement(expr.get_statement());
463  tmp.add_source_location()=expr.source_location();
464  tmp.copy_to_operands(expr.op0());
465  tmp.set(ID_destructor, expr.find(ID_destructor));
466 
467  convert_cpp_delete(tmp, dest);
468 
469  expr.make_nil();
470 }
471 
473  side_effect_exprt &expr,
474  goto_programt &dest,
475  const irep_idt &mode,
476  bool result_is_used)
477 {
478  codet call;
479 
480  if(result_is_used)
481  {
482  const symbolt &new_symbol = get_fresh_aux_symbol(
483  expr.type(),
485  "malloc_value",
486  expr.source_location(),
487  mode,
488  symbol_table);
489 
490  code_declt decl(new_symbol.symbol_expr());
491  decl.add_source_location()=new_symbol.location;
492  convert_decl(decl, dest, mode);
493 
494  call=code_assignt(new_symbol.symbol_expr(), expr);
495  call.add_source_location()=expr.source_location();
496 
497  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
498  }
499  else
500  {
501  call=codet(ID_expression);
502  call.move_to_operands(expr);
503  }
504 
505  convert(call, dest, mode);
506 }
507 
509  side_effect_exprt &expr,
510  goto_programt &dest,
511  bool result_is_used)
512 {
513  const irep_idt &mode = expr.get(ID_mode);
514  if(expr.operands().size()!=1 &&
515  !expr.operands().empty())
516  {
518  error() << "temporary_object takes 0 or 1 operands" << eom;
519  throw 0;
520  }
521 
522  symbolt &new_symbol = new_tmp_symbol(
523  expr.type(), "obj", dest, expr.find_source_location(), mode);
524 
525  if(expr.operands().size()==1)
526  {
527  const code_assignt assignment(new_symbol.symbol_expr(), expr.op0());
528 
529  convert(assignment, dest, mode);
530  }
531 
532  if(expr.find(ID_initializer).is_not_nil())
533  {
534  assert(expr.operands().empty());
535  exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
536  replace_new_object(new_symbol.symbol_expr(), initializer);
537 
538  convert(to_code(initializer), dest, mode);
539  }
540 
541  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
542 }
543 
545  side_effect_exprt &expr,
546  goto_programt &dest,
547  const irep_idt &mode,
548  bool result_is_used)
549 {
550  // This is a gcc extension of the form ({ ....; expr; })
551  // The value is that of the final expression.
552  // The expression is copied into a temporary before the
553  // scope is destroyed.
554 
555  if(expr.operands().size()!=1)
556  {
558  error() << "statement_expression takes 1 operand" << eom;
559  throw 0;
560  }
561 
562  if(expr.op0().id()!=ID_code)
563  {
565  error() << "statement_expression takes code as operand" << eom;
566  throw 0;
567  }
568 
569  codet &code=to_code(expr.op0());
570 
571  if(!result_is_used)
572  {
573  convert(code, dest, mode);
574  expr.make_nil();
575  return;
576  }
577 
578  if(code.get_statement()!=ID_block)
579  {
581  error() << "statement_expression takes block as operand" << eom;
582  throw 0;
583  }
584 
585  if(code.operands().empty())
586  {
588  error() << "statement_expression takes non-empty block as operand"
589  << eom;
590  throw 0;
591  }
592 
593  // get last statement from block, following labels
595 
596  source_locationt source_location=last.find_source_location();
597 
598  symbolt &new_symbol = new_tmp_symbol(
599  expr.type(), "statement_expression", dest, source_location, mode);
600 
601  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
602  tmp_symbol_expr.add_source_location()=source_location;
603 
604  if(last.get(ID_statement)==ID_expression)
605  {
606  // we turn this into an assignment
608  last=code_assignt(tmp_symbol_expr, e);
609  last.add_source_location()=source_location;
610  }
611  else if(last.get(ID_statement)==ID_assign)
612  {
613  exprt e=to_code_assign(last).lhs();
614  code_assignt assignment(tmp_symbol_expr, e);
615  assignment.add_source_location()=source_location;
616  code.operands().push_back(assignment);
617  }
618  else
619  {
620  error() << "statement_expression expects expression as "
621  << "last statement, but got `"
622  << last.get(ID_statement) << "'" << eom;
623  throw 0;
624  }
625 
626  {
627  goto_programt tmp;
628  convert(code, tmp, mode);
629  dest.destructive_append(tmp);
630  }
631 
632  static_cast<exprt &>(expr)=tmp_symbol_expr;
633 }
634 
636  side_effect_exprt &expr,
637  goto_programt &dest,
638  const irep_idt &mode,
639  bool result_is_used)
640 {
641  const irep_idt &statement=expr.get_statement();
642 
643  if(statement==ID_function_call)
644  remove_function_call(expr, dest, mode, result_is_used);
645  else if(statement==ID_assign ||
646  statement==ID_assign_plus ||
647  statement==ID_assign_minus ||
648  statement==ID_assign_mult ||
649  statement==ID_assign_div ||
650  statement==ID_assign_bitor ||
651  statement==ID_assign_bitxor ||
652  statement==ID_assign_bitand ||
653  statement==ID_assign_lshr ||
654  statement==ID_assign_ashr ||
655  statement==ID_assign_shl ||
656  statement==ID_assign_mod)
657  remove_assignment(expr, dest, result_is_used, mode);
658  else if(statement==ID_postincrement ||
659  statement==ID_postdecrement)
660  remove_post(expr, dest, mode, result_is_used);
661  else if(statement==ID_preincrement ||
662  statement==ID_predecrement)
663  remove_pre(expr, dest, result_is_used, mode);
664  else if(statement==ID_cpp_new ||
665  statement==ID_cpp_new_array)
666  remove_cpp_new(expr, dest, result_is_used);
667  else if(statement==ID_cpp_delete ||
668  statement==ID_cpp_delete_array)
669  remove_cpp_delete(expr, dest, result_is_used);
670  else if(statement==ID_allocate)
671  remove_malloc(expr, dest, mode, result_is_used);
672  else if(statement==ID_temporary_object)
673  remove_temporary_object(expr, dest, result_is_used);
674  else if(statement==ID_statement_expression)
675  remove_statement_expression(expr, dest, mode, result_is_used);
676  else if(statement==ID_nondet)
677  {
678  // these are fine
679  }
680  else if(statement==ID_skip)
681  {
682  expr.make_nil();
683  }
684  else if(statement==ID_throw)
685  {
687  t->code=
688  code_expressiont(side_effect_expr_throwt(expr.find(ID_exception_list)));
689  t->code.op0().operands().swap(expr.operands());
690  t->code.add_source_location()=expr.source_location();
691  t->source_location=expr.source_location();
692 
693  // the result can't be used, these are void
694  expr.make_nil();
695  }
696  else
697  {
699  error() << "cannot remove side effect (" << statement << ")" << eom;
700  throw 0;
701  }
702 }
const irep_idt & get_statement() const
Definition: std_code.h:39
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
semantic type conversion
Definition: std_expr.h:2111
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
Symbol table entry.
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
irep_idt mode
Language mode.
Definition: symbol.h:52
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
exprt & symbol()
Definition: std_code.h:266
Deprecated expression utility functions.
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
Fresh auxiliary symbol creation.
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
An expression statement.
Definition: std_code.h:1188
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1222
A side effect that throws an exception.
Definition: std_code.h:1409
static bool has_function_call(const exprt &expr)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
argumentst & arguments()
Definition: std_code.h:860
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:84
std::string tmp_symbol_prefix
A generic base class for binary expressions.
Definition: std_expr.h:649
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:253
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
Program Transformation.
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
API to expression classes.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
codet & find_last_statement()
Definition: std_code.h:130
void convert_cpp_delete(const codet &code, goto_programt &dest)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
bool is_number(const typet &type)
Definition: type.cpp:25
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:848
void set_statement(const irep_idt &statement)
Definition: std_code.h:34
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const exprt & expression() const
Definition: std_code.h:1201
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1700
symbol_table_baset & symbol_table
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
A statement in a programming language.
Definition: std_code.h:21
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
const typet & subtype() const
Definition: type.h:33
An expression containing a side effect.
Definition: std_code.h:1238
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
static void replace_new_object(const exprt &object, exprt &dest)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
complex constructor from a pair of numbers
Definition: std_expr.h:1861
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const irep_idt & get_statement() const
Definition: std_code.h:1253