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/expr_util.h>
16 #include <util/std_expr.h>
17 #include <util/rename.h>
18 #include <util/cprover_prefix.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 {
41  const irep_idt statement=expr.get_statement();
42 
43  if(statement==ID_assign)
44  {
45  exprt tmp=expr;
46  tmp.id(ID_code);
47  // just interpret as code
49  }
50  else if(statement==ID_assign_plus ||
51  statement==ID_assign_minus ||
52  statement==ID_assign_mult ||
53  statement==ID_assign_div ||
54  statement==ID_assign_mod ||
55  statement==ID_assign_shl ||
56  statement==ID_assign_ashr ||
57  statement==ID_assign_lshr ||
58  statement==ID_assign_bitand ||
59  statement==ID_assign_bitxor ||
60  statement==ID_assign_bitor)
61  {
62  if(expr.operands().size()!=2)
63  {
65  error() << statement << " takes two arguments" << eom;
66  throw 0;
67  }
68 
69  irep_idt new_id;
70 
71  if(statement==ID_assign_plus)
72  new_id=ID_plus;
73  else if(statement==ID_assign_minus)
74  new_id=ID_minus;
75  else if(statement==ID_assign_mult)
76  new_id=ID_mult;
77  else if(statement==ID_assign_div)
78  new_id=ID_div;
79  else if(statement==ID_assign_mod)
80  new_id=ID_mod;
81  else if(statement==ID_assign_shl)
82  new_id=ID_shl;
83  else if(statement==ID_assign_ashr)
84  new_id=ID_ashr;
85  else if(statement==ID_assign_lshr)
86  new_id=ID_lshr;
87  else if(statement==ID_assign_bitand)
88  new_id=ID_bitand;
89  else if(statement==ID_assign_bitxor)
90  new_id=ID_bitxor;
91  else if(statement==ID_assign_bitor)
92  new_id=ID_bitor;
93  else
94  {
96  error() << "assignment `" << statement << "' not yet supported"
97  << eom;
98  throw 0;
99  }
100 
101  exprt rhs;
102 
103  const typet &op0_type=ns.follow(expr.op0().type());
104 
105  // C/C++ Booleans get very special treatment.
106  if(op0_type.id()==ID_c_bool)
107  {
108  binary_exprt tmp(expr.op0(), new_id, expr.op1(), expr.op1().type());
109  tmp.op0().make_typecast(expr.op1().type());
110  rhs=typecast_exprt(is_not_zero(tmp, ns), expr.op0().type());
111  }
112  else
113  {
114  rhs.id(new_id);
115  rhs.copy_to_operands(expr.op0(), expr.op1());
116  rhs.type()=expr.op0().type();
118  }
119 
120  code_assignt assignment(expr.op0(), rhs);
121  assignment.add_source_location()=expr.source_location();
122 
123  convert(assignment, dest);
124  }
125  else
126  assert(false);
127 
128  // revert assignment in the expression to its LHS
129  if(result_is_used)
130  {
131  exprt lhs;
132  lhs.swap(expr.op0());
133  expr.swap(lhs);
134  }
135  else
136  expr.make_nil();
137 }
138 
140  side_effect_exprt &expr,
141  goto_programt &dest,
142  bool result_is_used)
143 {
144  if(expr.operands().size()!=1)
145  {
147  error() << "preincrement/predecrement must have one operand" << eom;
148  throw 0;
149  }
150 
151  const irep_idt statement=expr.get_statement();
152 
153  assert(statement==ID_preincrement ||
154  statement==ID_predecrement);
155 
156  exprt rhs;
158 
159  if(statement==ID_preincrement)
160  rhs.id(ID_plus);
161  else
162  rhs.id(ID_minus);
163 
164  const typet &op_type=ns.follow(expr.op0().type());
165 
166  if(op_type.id()==ID_bool)
167  {
170  rhs.type()=signed_int_type();
171  rhs=is_not_zero(rhs, ns);
172  }
173  else if(op_type.id()==ID_c_bool)
174  {
177  rhs.type()=signed_int_type();
178  rhs=is_not_zero(rhs, ns);
179  rhs.make_typecast(op_type);
180  }
181  else if(op_type.id()==ID_c_enum ||
182  op_type.id()==ID_c_enum_tag)
183  {
186  rhs.type()=signed_int_type();
187  rhs.make_typecast(op_type);
188  }
189  else
190  {
191  typet constant_type;
192 
193  if(op_type.id()==ID_pointer)
194  constant_type=index_type();
195  else if(is_number(op_type) || op_type.id()==ID_c_bool)
196  constant_type=op_type;
197  else
198  {
200  error() << "no constant one of type " << op_type.pretty() << eom;
201  throw 0;
202  }
203 
204  exprt constant=from_integer(1, constant_type);
205 
206  rhs.copy_to_operands(expr.op0());
207  rhs.move_to_operands(constant);
208  rhs.type()=expr.op0().type();
209  }
210 
211  code_assignt assignment(expr.op0(), rhs);
212  assignment.add_source_location()=expr.find_source_location();
213 
214  convert(assignment, dest);
215 
216  if(result_is_used)
217  {
218  // revert to argument of pre-inc/pre-dec
219  exprt tmp=expr.op0();
220  expr.swap(tmp);
221  }
222  else
223  expr.make_nil();
224 }
225 
227  side_effect_exprt &expr,
228  goto_programt &dest,
229  bool result_is_used)
230 {
231  goto_programt tmp1, tmp2;
232 
233  // we have ...(op++)...
234 
235  if(expr.operands().size()!=1)
236  {
238  error() << "postincrement/postdecrement must have one operand"
239  << eom;
240  throw 0;
241  }
242 
243  const irep_idt statement=expr.get_statement();
244 
245  assert(statement==ID_postincrement ||
246  statement==ID_postdecrement);
247 
248  exprt rhs;
250 
251  if(statement==ID_postincrement)
252  rhs.id(ID_plus);
253  else
254  rhs.id(ID_minus);
255 
256  const typet &op_type=ns.follow(expr.op0().type());
257 
258  if(op_type.id()==ID_bool)
259  {
262  rhs.type()=signed_int_type();
263  rhs=is_not_zero(rhs, ns);
264  }
265  else if(op_type.id()==ID_c_bool)
266  {
269  rhs.type()=signed_int_type();
270  rhs=is_not_zero(rhs, ns);
271  rhs.make_typecast(op_type);
272  }
273  else if(op_type.id()==ID_c_enum ||
274  op_type.id()==ID_c_enum_tag)
275  {
278  rhs.type()=signed_int_type();
279  rhs.make_typecast(op_type);
280  }
281  else
282  {
283  typet constant_type;
284 
285  if(op_type.id()==ID_pointer)
286  constant_type=index_type();
287  else if(is_number(op_type) || op_type.id()==ID_c_bool)
288  constant_type=op_type;
289  else
290  {
292  error() << "no constant one of type " << op_type.pretty() << eom;
293  throw 0;
294  }
295 
296  exprt constant;
297 
298  if(constant_type.id()==ID_complex)
299  {
300  exprt real=from_integer(1, constant_type.subtype());
301  exprt imag=from_integer(0, constant_type.subtype());
302  constant=complex_exprt(real, imag, to_complex_type(constant_type));
303  }
304  else
305  constant=from_integer(1, constant_type);
306 
307  rhs.copy_to_operands(expr.op0());
308  rhs.move_to_operands(constant);
309  rhs.type()=expr.op0().type();
310  }
311 
312  code_assignt assignment(expr.op0(), rhs);
313  assignment.add_source_location()=expr.find_source_location();
314 
315  convert(assignment, tmp2);
316 
317  // fix up the expression, if needed
318 
319  if(result_is_used)
320  {
321  exprt tmp=expr.op0();
322  make_temp_symbol(tmp, "post", dest);
323  expr.swap(tmp);
324  }
325  else
326  expr.make_nil();
327 
328  dest.destructive_append(tmp1);
329  dest.destructive_append(tmp2);
330 }
331 
333  side_effect_exprt &expr,
334  goto_programt &dest,
335  bool result_is_used)
336 {
337  if(!result_is_used)
338  {
339  assert(expr.operands().size()==2);
340  code_function_callt call;
341  call.function()=expr.op0();
342  call.arguments()=expr.op1().operands();
343  call.add_source_location()=expr.source_location();
344  call.lhs().make_nil();
345  convert_function_call(call, dest);
346  expr.make_nil();
347  return;
348  }
349 
350  auxiliary_symbolt new_symbol;
351 
352  new_symbol.base_name="return_value";
353  new_symbol.type=expr.type();
354  new_symbol.location=expr.find_source_location();
355 
356  // get name of function, if available
357 
358  if(expr.id()!=ID_side_effect ||
359  expr.get(ID_statement)!=ID_function_call)
360  {
362  error() << "expected function call" << eom;
363  throw 0;
364  }
365 
366  if(expr.operands().empty())
367  {
369  error() << "function_call expects at least one operand" << eom;
370  throw 0;
371  }
372 
373  if(expr.op0().id()==ID_symbol)
374  {
375  const irep_idt &identifier=expr.op0().get(ID_identifier);
376  const symbolt &symbol=lookup(identifier);
377 
378  std::string new_base_name=id2string(new_symbol.base_name);
379 
380  new_base_name+='_';
381  new_base_name+=id2string(symbol.base_name);
382  new_base_name+="$"+std::to_string(++temporary_counter);
383 
384  new_symbol.base_name=new_base_name;
385  new_symbol.mode=symbol.mode;
386  }
387 
388  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
389 
390  new_name(new_symbol);
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);
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);
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  auxiliary_symbolt new_symbol;
431 
432  new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter);
433  new_symbol.type=expr.type();
434  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
435 
436  new_name(new_symbol);
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);
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);
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  bool result_is_used)
476 {
477  codet call;
478 
479  if(result_is_used)
480  {
481  auxiliary_symbolt new_symbol;
482 
483  new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter);
484  new_symbol.type=expr.type();
485  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
486  new_symbol.location=expr.source_location();
487 
488  new_name(new_symbol);
489 
490  code_declt decl;
491  decl.symbol()=new_symbol.symbol_expr();
492  decl.add_source_location()=new_symbol.location;
493  convert_decl(decl, dest);
494 
495  call=code_assignt(new_symbol.symbol_expr(), expr);
496  call.add_source_location()=expr.source_location();
497 
498  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
499  }
500  else
501  {
502  call=codet(ID_expression);
503  call.move_to_operands(expr);
504  }
505 
506  convert(call, dest);
507 }
508 
510  side_effect_exprt &expr,
511  goto_programt &dest,
512  bool result_is_used)
513 {
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=
523  new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location());
524 
525  new_symbol.mode=expr.get(ID_mode);
526 
527  if(expr.operands().size()==1)
528  {
529  codet assignment(ID_assign);
530  assignment.reserve_operands(2);
531  assignment.copy_to_operands(new_symbol.symbol_expr());
532  assignment.move_to_operands(expr.op0());
533 
534  convert(assignment, dest);
535  }
536 
537  if(expr.find(ID_initializer).is_not_nil())
538  {
539  assert(expr.operands().empty());
540  exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
541  replace_new_object(new_symbol.symbol_expr(), initializer);
542 
543  convert(to_code(initializer), dest);
544  }
545 
546  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
547 }
548 
550  side_effect_exprt &expr,
551  goto_programt &dest,
552  bool result_is_used)
553 {
554  // This is a gcc extension of the form ({ ....; expr; })
555  // The value is that of the final expression.
556  // The expression is copied into a temporary before the
557  // scope is destroyed.
558 
559  if(expr.operands().size()!=1)
560  {
562  error() << "statement_expression takes 1 operand" << eom;
563  throw 0;
564  }
565 
566  if(expr.op0().id()!=ID_code)
567  {
569  error() << "statement_expression takes code as operand" << eom;
570  throw 0;
571  }
572 
573  codet &code=to_code(expr.op0());
574 
575  if(!result_is_used)
576  {
577  convert(code, dest);
578  expr.make_nil();
579  return;
580  }
581 
582  if(code.get_statement()!=ID_block)
583  {
585  error() << "statement_expression takes block as operand" << eom;
586  throw 0;
587  }
588 
589  if(code.operands().empty())
590  {
592  error() << "statement_expression takes non-empty block as operand"
593  << eom;
594  throw 0;
595  }
596 
597  // get last statement from block, following labels
599 
600  source_locationt source_location=last.find_source_location();
601 
602  symbolt &new_symbol=
603  new_tmp_symbol(expr.type(), "statement_expression", dest, source_location);
604 
605  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
606  tmp_symbol_expr.add_source_location()=source_location;
607 
608  if(last.get(ID_statement)==ID_expression)
609  {
610  // we turn this into an assignment
612  last=code_assignt(tmp_symbol_expr, e);
613  last.add_source_location()=source_location;
614  }
615  else if(last.get(ID_statement)==ID_assign)
616  {
617  exprt e=to_code_assign(last).lhs();
618  code_assignt assignment(tmp_symbol_expr, e);
619  assignment.add_source_location()=source_location;
620  code.operands().push_back(assignment);
621  }
622  else
623  {
624  error() << "statement_expression expects expression as "
625  << "last statement, but got `"
626  << last.get(ID_statement) << "'" << eom;
627  throw 0;
628  }
629 
630  {
631  goto_programt tmp;
632  convert(code, tmp);
633  dest.destructive_append(tmp);
634  }
635 
636  static_cast<exprt &>(expr)=tmp_symbol_expr;
637 }
638 
640  side_effect_exprt &expr,
641  goto_programt &dest)
642 {
643  // we only get here for ID_push_catch, which is only used for Java
645 
646  // the result can't be used, these are void
647  expr.make_nil();
648 }
649 
651  side_effect_exprt &expr,
652  goto_programt &dest,
653  bool result_is_used)
654 {
655  const irep_idt &statement=expr.get_statement();
656 
657  if(statement==ID_function_call)
658  remove_function_call(expr, dest, result_is_used);
659  else if(statement==ID_assign ||
660  statement==ID_assign_plus ||
661  statement==ID_assign_minus ||
662  statement==ID_assign_mult ||
663  statement==ID_assign_div ||
664  statement==ID_assign_bitor ||
665  statement==ID_assign_bitxor ||
666  statement==ID_assign_bitand ||
667  statement==ID_assign_lshr ||
668  statement==ID_assign_ashr ||
669  statement==ID_assign_shl ||
670  statement==ID_assign_mod)
671  remove_assignment(expr, dest, result_is_used);
672  else if(statement==ID_postincrement ||
673  statement==ID_postdecrement)
674  remove_post(expr, dest, result_is_used);
675  else if(statement==ID_preincrement ||
676  statement==ID_predecrement)
677  remove_pre(expr, dest, result_is_used);
678  else if(statement==ID_cpp_new ||
679  statement==ID_cpp_new_array)
680  remove_cpp_new(expr, dest, result_is_used);
681  else if(statement==ID_cpp_delete ||
682  statement==ID_cpp_delete_array)
683  remove_cpp_delete(expr, dest, result_is_used);
684  else if(statement==ID_malloc)
685  remove_malloc(expr, dest, result_is_used);
686  else if(statement==ID_temporary_object)
687  remove_temporary_object(expr, dest, result_is_used);
688  else if(statement==ID_statement_expression)
689  remove_statement_expression(expr, dest, result_is_used);
690  else if(statement==ID_nondet)
691  {
692  // these are fine
693  }
694  else if(statement==ID_skip)
695  {
696  expr.make_nil();
697  }
698  else if(statement==ID_throw)
699  {
701  t->code=
702  code_expressiont(side_effect_expr_throwt(expr.find(ID_exception_list)));
703  t->code.op0().operands().swap(expr.operands());
704  t->code.add_source_location()=expr.source_location();
705  t->source_location=expr.source_location();
706 
707  // the result can't be used, these are void
708  expr.make_nil();
709  }
710  else if(statement==ID_push_catch)
711  remove_push_catch(expr, dest);
712  else
713  {
715  error() << "cannot remove side effect (" << statement << ")" << eom;
716  throw 0;
717  }
718 }
const irep_idt & get_statement() const
Definition: std_code.h:37
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
Symbol table entry.
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
exprt & op0()
Definition: expr.h:84
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
void remove_push_catch(side_effect_exprt &expr, goto_programt &dest)
irep_idt mode
Language mode.
Definition: symbol.h:55
exprt & symbol()
Definition: std_code.h:205
Deprecated expression utility functions.
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
void convert_assign(const code_assignt &code, goto_programt &dest)
typet & type()
Definition: expr.h:60
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
An expression statement.
Definition: std_code.h:957
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:981
A side effect that throws an exception.
Definition: std_code.h:1100
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
static bool has_function_call(const exprt &expr)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
argumentst & arguments()
Definition: std_code.h:689
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:91
std::string tmp_symbol_prefix
A generic base class for binary expressions.
Definition: std_expr.h:471
A declaration of a local variable.
Definition: std_code.h:192
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
Program Transformation.
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
bitvector_typet index_type()
Definition: c_types.cpp:15
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
codet & find_last_statement()
Definition: std_code.h:94
void convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_function_call(const code_function_callt &code, goto_programt &dest)
void remove_post(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void convert_java_try_catch(const codet &code, goto_programt &dest)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
bool is_number(const typet &type)
Definition: type.cpp:24
void convert_decl(const code_declt &code, goto_programt &dest)
void new_name(symbolt &symbol)
exprt & function()
Definition: std_code.h:677
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
Definition: expr.h:46
const symbolt & lookup(const irep_idt &identifier)
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const source_locationt & source_location() const
Definition: expr.h:142
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &)
const exprt & expression() const
Definition: std_code.h:970
unsigned temporary_counter
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1629
A statement in a programming language.
Definition: std_code.h:19
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
const typet & subtype() const
Definition: type.h:31
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:90
static void replace_new_object(const exprt &object, exprt &dest)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
complex constructor from a pair of numbers
Definition: std_expr.h:1504
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
const irep_idt & get_statement() const
Definition: std_code.h:1012