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  {
64  expr.operands().size() == 2,
65  id2string(statement) + " expects two arguments",
66  expr.find_source_location());
67 
68  irep_idt new_id;
69 
70  if(statement==ID_assign_plus)
71  new_id=ID_plus;
72  else if(statement==ID_assign_minus)
73  new_id=ID_minus;
74  else if(statement==ID_assign_mult)
75  new_id=ID_mult;
76  else if(statement==ID_assign_div)
77  new_id=ID_div;
78  else if(statement==ID_assign_mod)
79  new_id=ID_mod;
80  else if(statement==ID_assign_shl)
81  new_id=ID_shl;
82  else if(statement==ID_assign_ashr)
83  new_id=ID_ashr;
84  else if(statement==ID_assign_lshr)
85  new_id=ID_lshr;
86  else if(statement==ID_assign_bitand)
87  new_id=ID_bitand;
88  else if(statement==ID_assign_bitxor)
89  new_id=ID_bitxor;
90  else if(statement==ID_assign_bitor)
91  new_id=ID_bitor;
92  else
93  {
95  }
96 
97  exprt rhs;
98 
99  const typet &op0_type=ns.follow(expr.op0().type());
100 
101  if(op0_type.id()==ID_c_bool)
102  {
103  // C/C++ Booleans get very special treatment.
104  binary_exprt tmp(expr.op0(), new_id, expr.op1(), expr.op1().type());
105  tmp.op0().make_typecast(expr.op1().type());
106  rhs=typecast_exprt(is_not_zero(tmp, ns), expr.op0().type());
107  }
108  else if(op0_type.id() == ID_c_enum_tag)
109  {
110  // We convert c_enums to their underlying type, do the
111  // operation, and then convert back
112  const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(op0_type));
113  auto underlying_type = to_c_enum_type(enum_type).subtype();
114  auto op0 = typecast_exprt(expr.op0(), underlying_type);
115  auto op1 = typecast_exprt(expr.op1(), underlying_type);
116  binary_exprt tmp(op0, new_id, op1, underlying_type);
117  rhs = typecast_exprt(tmp, expr.op0().type());
118  }
119  else
120  {
121  rhs.id(new_id);
122  rhs.copy_to_operands(expr.op0(), expr.op1());
123  rhs.type()=expr.op0().type();
125  }
126 
127  code_assignt assignment(expr.op0(), rhs);
128  assignment.add_source_location()=expr.source_location();
129 
130  convert(assignment, dest, mode);
131  }
132  else
133  UNREACHABLE;
134 
135  // revert assignment in the expression to its LHS
136  if(result_is_used)
137  {
138  exprt lhs;
139  lhs.swap(expr.op0());
140  expr.swap(lhs);
141  }
142  else
143  expr.make_nil();
144 }
145 
147  side_effect_exprt &expr,
148  goto_programt &dest,
149  bool result_is_used,
150  const irep_idt &mode)
151 {
153  expr.operands().size() == 1,
154  "preincrement/predecrement must have one operand",
155  expr.find_source_location());
156 
157  const irep_idt statement=expr.get_statement();
158 
160  statement == ID_preincrement || statement == ID_predecrement,
161  "expects preincrement or predecrement");
162 
163  exprt rhs;
165 
166  if(statement==ID_preincrement)
167  rhs.id(ID_plus);
168  else
169  rhs.id(ID_minus);
170 
171  const typet &op_type=ns.follow(expr.op0().type());
172 
173  if(op_type.id()==ID_bool)
174  {
177  rhs.type()=signed_int_type();
178  rhs=is_not_zero(rhs, ns);
179  }
180  else if(op_type.id()==ID_c_bool)
181  {
184  rhs.type()=signed_int_type();
185  rhs=is_not_zero(rhs, ns);
186  rhs.make_typecast(op_type);
187  }
188  else if(op_type.id()==ID_c_enum ||
189  op_type.id()==ID_c_enum_tag)
190  {
193  rhs.type()=signed_int_type();
194  rhs.make_typecast(op_type);
195  }
196  else
197  {
198  typet constant_type;
199 
200  if(op_type.id()==ID_pointer)
201  constant_type=index_type();
202  else if(is_number(op_type) || op_type.id()==ID_c_bool)
203  constant_type=op_type;
204  else
205  {
206  UNREACHABLE;
207  }
208 
209  exprt constant=from_integer(1, constant_type);
210 
211  rhs.copy_to_operands(expr.op0());
212  rhs.move_to_operands(constant);
213  rhs.type()=expr.op0().type();
214  }
215 
216  code_assignt assignment(expr.op0(), rhs);
217  assignment.add_source_location()=expr.find_source_location();
218 
219  convert(assignment, dest, mode);
220 
221  if(result_is_used)
222  {
223  // revert to argument of pre-inc/pre-dec
224  exprt tmp=expr.op0();
225  expr.swap(tmp);
226  }
227  else
228  expr.make_nil();
229 }
230 
232  side_effect_exprt &expr,
233  goto_programt &dest,
234  const irep_idt &mode,
235  bool result_is_used)
236 {
237  goto_programt tmp1, tmp2;
238 
239  // we have ...(op++)...
240 
242  expr.operands().size() == 1,
243  "postincrement/postdecrement must have one operand",
244  expr.find_source_location());
245 
246  const irep_idt statement=expr.get_statement();
247 
249  statement == ID_postincrement || statement == ID_postdecrement,
250  "expects postincrement or postdecrement");
251 
252  exprt rhs;
254 
255  if(statement==ID_postincrement)
256  rhs.id(ID_plus);
257  else
258  rhs.id(ID_minus);
259 
260  const typet &op_type=ns.follow(expr.op0().type());
261 
262  if(op_type.id()==ID_bool)
263  {
266  rhs.type()=signed_int_type();
267  rhs=is_not_zero(rhs, ns);
268  }
269  else if(op_type.id()==ID_c_bool)
270  {
273  rhs.type()=signed_int_type();
274  rhs=is_not_zero(rhs, ns);
275  rhs.make_typecast(op_type);
276  }
277  else if(op_type.id()==ID_c_enum ||
278  op_type.id()==ID_c_enum_tag)
279  {
282  rhs.type()=signed_int_type();
283  rhs.make_typecast(op_type);
284  }
285  else
286  {
287  typet constant_type;
288 
289  if(op_type.id()==ID_pointer)
290  constant_type=index_type();
291  else if(is_number(op_type) || op_type.id()==ID_c_bool)
292  constant_type=op_type;
293  else
294  {
295  UNREACHABLE;
296  }
297 
298  exprt constant;
299 
300  if(constant_type.id()==ID_complex)
301  {
302  exprt real=from_integer(1, constant_type.subtype());
303  exprt imag=from_integer(0, constant_type.subtype());
304  constant=complex_exprt(real, imag, to_complex_type(constant_type));
305  }
306  else
307  constant=from_integer(1, constant_type);
308 
309  rhs.copy_to_operands(expr.op0());
310  rhs.move_to_operands(constant);
311  rhs.type()=expr.op0().type();
312  }
313 
314  code_assignt assignment(expr.op0(), rhs);
315  assignment.add_source_location()=expr.find_source_location();
316 
317  convert(assignment, tmp2, mode);
318 
319  // fix up the expression, if needed
320 
321  if(result_is_used)
322  {
323  exprt tmp=expr.op0();
324  make_temp_symbol(tmp, "post", dest, mode);
325  expr.swap(tmp);
326  }
327  else
328  expr.make_nil();
329 
330  dest.destructive_append(tmp1);
331  dest.destructive_append(tmp2);
332 }
333 
335  side_effect_exprt &expr,
336  goto_programt &dest,
337  const irep_idt &mode,
338  bool result_is_used)
339 {
341  expr.operands().size() == 2,
342  "function_call expects two operands",
343  expr.find_source_location());
344 
345  if(!result_is_used)
346  {
347  code_function_callt call(expr.op0(), expr.op1().operands());
348  call.add_source_location()=expr.source_location();
349  convert_function_call(call, dest, mode);
350  expr.make_nil();
351  return;
352  }
353 
354  // get name of function, if available
355 
357  expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
358  "expects function call",
359  expr.find_source_location());
360 
361  std::string new_base_name = "return_value";
362  irep_idt new_symbol_mode = mode;
363 
364  if(expr.op0().id()==ID_symbol)
365  {
366  const irep_idt &identifier = to_symbol_expr(expr.op0()).get_identifier();
367  const symbolt &symbol = ns.lookup(identifier);
368 
369  new_base_name+='_';
370  new_base_name+=id2string(symbol.base_name);
371  new_symbol_mode = symbol.mode;
372  }
373 
374  const symbolt &new_symbol = get_fresh_aux_symbol(
375  expr.type(),
377  new_base_name,
378  expr.find_source_location(),
379  new_symbol_mode,
380  symbol_table);
381 
382  {
383  code_declt decl(new_symbol.symbol_expr());
384  decl.add_source_location()=new_symbol.location;
385  convert_decl(decl, dest, mode);
386  }
387 
388  {
389  goto_programt tmp_program2;
390  code_function_callt call(
391  new_symbol.symbol_expr(), expr.op0(), expr.op1().operands());
392  call.add_source_location()=new_symbol.location;
393  convert_function_call(call, dest, mode);
394  }
395 
396  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
397 }
398 
400  const exprt &object,
401  exprt &dest)
402 {
403  if(dest.id()=="new_object")
404  dest=object;
405  else
406  Forall_operands(it, dest)
407  replace_new_object(object, *it);
408 }
409 
411  side_effect_exprt &expr,
412  goto_programt &dest,
413  bool result_is_used)
414 {
415  const symbolt &new_symbol = get_fresh_aux_symbol(
416  expr.type(),
418  "new_ptr",
419  expr.find_source_location(),
420  ID_cpp,
421  symbol_table);
422 
423  code_declt decl(new_symbol.symbol_expr());
424  decl.add_source_location()=new_symbol.location;
425  convert_decl(decl, dest, ID_cpp);
426 
427  const code_assignt call(new_symbol.symbol_expr(), expr);
428 
429  if(result_is_used)
430  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
431  else
432  expr.make_nil();
433 
434  convert(call, dest, ID_cpp);
435 }
436 
438  side_effect_exprt &expr,
439  goto_programt &dest)
440 {
441  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
442 
443  codet tmp(expr.get_statement());
445  tmp.copy_to_operands(expr.op0());
446  tmp.set(ID_destructor, expr.find(ID_destructor));
447 
448  convert_cpp_delete(tmp, dest);
449 
450  expr.make_nil();
451 }
452 
454  side_effect_exprt &expr,
455  goto_programt &dest,
456  const irep_idt &mode,
457  bool result_is_used)
458 {
459  codet call;
460 
461  if(result_is_used)
462  {
463  const symbolt &new_symbol = get_fresh_aux_symbol(
464  expr.type(),
466  "malloc_value",
467  expr.source_location(),
468  mode,
469  symbol_table);
470 
471  code_declt decl(new_symbol.symbol_expr());
472  decl.add_source_location()=new_symbol.location;
473  convert_decl(decl, dest, mode);
474 
475  call=code_assignt(new_symbol.symbol_expr(), expr);
476  call.add_source_location()=expr.source_location();
477 
478  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
479  }
480  else
481  {
482  call=codet(ID_expression);
483  call.move_to_operands(expr);
484  }
485 
486  convert(call, dest, mode);
487 }
488 
490  side_effect_exprt &expr,
491  goto_programt &dest)
492 {
493  const irep_idt &mode = expr.get(ID_mode);
495  expr.operands().size() <= 1,
496  "temporary_object takes zero or one operands",
497  expr.find_source_location());
498 
499  symbolt &new_symbol = new_tmp_symbol(
500  expr.type(), "obj", dest, expr.find_source_location(), mode);
501 
502  if(expr.operands().size()==1)
503  {
504  const code_assignt assignment(new_symbol.symbol_expr(), expr.op0());
505 
506  convert(assignment, dest, mode);
507  }
508 
509  if(expr.find(ID_initializer).is_not_nil())
510  {
512  expr.operands().empty(),
513  "temporary_object takes zero operands",
514  expr.find_source_location());
515  exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
516  replace_new_object(new_symbol.symbol_expr(), initializer);
517 
518  convert(to_code(initializer), dest, mode);
519  }
520 
521  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
522 }
523 
525  side_effect_exprt &expr,
526  goto_programt &dest,
527  const irep_idt &mode,
528  bool result_is_used)
529 {
530  // This is a gcc extension of the form ({ ....; expr; })
531  // The value is that of the final expression.
532  // The expression is copied into a temporary before the
533  // scope is destroyed.
534 
536  expr.operands().size() == 1,
537  "statement_expression takes one operand",
538  expr.find_source_location());
539 
541  expr.op0().id() == ID_code,
542  "statement_expression takes code as operand",
543  expr.find_source_location());
544 
545  codet &code=to_code(expr.op0());
546 
547  if(!result_is_used)
548  {
549  convert(code, dest, mode);
550  expr.make_nil();
551  return;
552  }
553 
555  code.get_statement() == ID_block,
556  "statement_expression takes block as operand",
557  code.find_source_location());
558 
560  !code.operands().empty(),
561  "statement_expression takes non-empty block as operand",
562  expr.find_source_location());
563 
564  // get last statement from block, following labels
566 
567  source_locationt source_location=last.find_source_location();
568 
569  symbolt &new_symbol = new_tmp_symbol(
570  expr.type(), "statement_expression", dest, source_location, mode);
571 
572  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
573  tmp_symbol_expr.add_source_location()=source_location;
574 
575  if(last.get(ID_statement)==ID_expression)
576  {
577  // we turn this into an assignment
579  last=code_assignt(tmp_symbol_expr, e);
580  last.add_source_location()=source_location;
581  }
582  else if(last.get(ID_statement)==ID_assign)
583  {
584  exprt e=to_code_assign(last).lhs();
585  code_assignt assignment(tmp_symbol_expr, e);
586  assignment.add_source_location()=source_location;
587  code.operands().push_back(assignment);
588  }
589  else
590  {
591  UNREACHABLE;
592  }
593 
594  {
595  goto_programt tmp;
596  convert(code, tmp, mode);
597  dest.destructive_append(tmp);
598  }
599 
600  static_cast<exprt &>(expr)=tmp_symbol_expr;
601 }
602 
604  side_effect_exprt &expr,
605  goto_programt &dest,
606  const irep_idt &mode,
607  bool result_is_used)
608 {
609  const irep_idt &statement=expr.get_statement();
610 
611  if(statement==ID_function_call)
612  remove_function_call(expr, dest, mode, result_is_used);
613  else if(statement==ID_assign ||
614  statement==ID_assign_plus ||
615  statement==ID_assign_minus ||
616  statement==ID_assign_mult ||
617  statement==ID_assign_div ||
618  statement==ID_assign_bitor ||
619  statement==ID_assign_bitxor ||
620  statement==ID_assign_bitand ||
621  statement==ID_assign_lshr ||
622  statement==ID_assign_ashr ||
623  statement==ID_assign_shl ||
624  statement==ID_assign_mod)
625  remove_assignment(expr, dest, result_is_used, mode);
626  else if(statement==ID_postincrement ||
627  statement==ID_postdecrement)
628  remove_post(expr, dest, mode, result_is_used);
629  else if(statement==ID_preincrement ||
630  statement==ID_predecrement)
631  remove_pre(expr, dest, result_is_used, mode);
632  else if(statement==ID_cpp_new ||
633  statement==ID_cpp_new_array)
634  remove_cpp_new(expr, dest, result_is_used);
635  else if(statement==ID_cpp_delete ||
636  statement==ID_cpp_delete_array)
637  remove_cpp_delete(expr, dest);
638  else if(statement==ID_allocate)
639  remove_malloc(expr, dest, mode, result_is_used);
640  else if(statement==ID_temporary_object)
641  remove_temporary_object(expr, dest);
642  else if(statement==ID_statement_expression)
643  remove_statement_expression(expr, dest, mode, result_is_used);
644  else if(statement==ID_nondet)
645  {
646  // these are fine
647  }
648  else if(statement==ID_skip)
649  {
650  expr.make_nil();
651  }
652  else if(statement==ID_throw)
653  {
655  t->code = code_expressiont(
657  expr.find(ID_exception_list), expr.type(), expr.source_location()));
658  t->code.op0().operands().swap(expr.operands());
659  t->code.add_source_location()=expr.source_location();
660  t->source_location=expr.source_location();
661 
662  // the result can't be used, these are void
663  expr.make_nil();
664  }
665  else
666  {
667  UNREACHABLE;
668  }
669 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
goto_convertt::convert_function_call
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_function_call.cpp:24
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
goto_convertt::remove_function_call
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:334
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1539
typet::subtype
const typet & subtype() const
Definition: type.h:38
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:48
arith_tools.h
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
goto_convertt::replace_new_object
static void replace_new_object(const exprt &object, exprt &dest)
Definition: goto_convert_side_effect.cpp:399
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:485
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:425
irept::make_nil
void make_nil()
Definition: irep.h:315
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
typet
The type of an expression, extends irept.
Definition: type.h:27
fresh_symbol.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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Definition: fresh_symbol.cpp:30
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_convertt::has_function_call
static bool has_function_call(const exprt &expr)
Definition: goto_convert_side_effect.cpp:23
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:49
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
goto_convert_class.h
goto_convertt::remove_pre
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:146
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:738
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
exprt::op0
exprt & op0()
Definition: expr.h:84
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:603
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1838
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
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:1887
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
THROW
Definition: goto_program.h:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
INVARIANT_WITH_DIAGNOSTICS
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:414
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
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:229
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:524
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
goto_convertt::remove_malloc
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:453
exprt::op1
exprt & op1()
Definition: expr.h:87
goto_convertt::remove_cpp_new
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
Definition: goto_convert_side_effect.cpp:410
irept::swap
void swap(irept &irep)
Definition: irep.h:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:259
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1962
goto_convertt::remove_cpp_delete
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:437
goto_convertt::remove_post
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:231
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:605
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:671
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1586
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
source_locationt
Definition: source_location.h:20
expr_util.h
Deprecated expression utility functions.
goto_convertt::remove_temporary_object
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:489
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:98
goto_convertt::remove_assignment
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:36
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1792
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:47
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:788
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1518
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:112
exprt::operands
operandst & operands()
Definition: expr.h:78
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
std_expr.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1504
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
goto_convertt::make_temp_symbol
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
Definition: goto_convert.cpp:1910