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>
19 #include <util/std_expr.h>
20 #include <util/symbol.h>
21 
22 #include <util/c_types.h>
23 
25 {
26  forall_operands(it, expr)
27  if(has_function_call(*it))
28  return true;
29 
30  if(expr.id()==ID_side_effect &&
31  expr.get(ID_statement)==ID_function_call)
32  return true;
33 
34  return false;
35 }
36 
38  side_effect_exprt &expr,
39  goto_programt &dest,
40  bool result_is_used,
41  bool address_taken,
42  const irep_idt &mode)
43 {
44  const irep_idt statement=expr.get_statement();
45 
46  optionalt<exprt> replacement_expr_opt;
47 
48  if(statement==ID_assign)
49  {
50  auto &old_assignment = to_side_effect_expr_assign(expr);
51 
52  if(result_is_used && !address_taken && needs_cleaning(old_assignment.lhs()))
53  {
54  if(!old_assignment.rhs().is_constant())
55  make_temp_symbol(old_assignment.rhs(), "assign", dest, mode);
56 
57  replacement_expr_opt = old_assignment.rhs();
58  }
59 
60  exprt new_lhs = skip_typecast(old_assignment.lhs());
61  exprt new_rhs =
62  typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
63  code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
64  new_assignment.add_source_location() = expr.source_location();
65 
66  convert_assign(new_assignment, dest, mode);
67  }
68  else if(statement==ID_assign_plus ||
69  statement==ID_assign_minus ||
70  statement==ID_assign_mult ||
71  statement==ID_assign_div ||
72  statement==ID_assign_mod ||
73  statement==ID_assign_shl ||
74  statement==ID_assign_ashr ||
75  statement==ID_assign_lshr ||
76  statement==ID_assign_bitand ||
77  statement==ID_assign_bitxor ||
78  statement==ID_assign_bitor)
79  {
81  expr.operands().size() == 2,
82  id2string(statement) + " expects two arguments",
83  expr.find_source_location());
84 
85  irep_idt new_id;
86 
87  if(statement==ID_assign_plus)
88  new_id=ID_plus;
89  else if(statement==ID_assign_minus)
90  new_id=ID_minus;
91  else if(statement==ID_assign_mult)
92  new_id=ID_mult;
93  else if(statement==ID_assign_div)
94  new_id=ID_div;
95  else if(statement==ID_assign_mod)
96  new_id=ID_mod;
97  else if(statement==ID_assign_shl)
98  new_id=ID_shl;
99  else if(statement==ID_assign_ashr)
100  new_id=ID_ashr;
101  else if(statement==ID_assign_lshr)
102  new_id=ID_lshr;
103  else if(statement==ID_assign_bitand)
104  new_id=ID_bitand;
105  else if(statement==ID_assign_bitxor)
106  new_id=ID_bitxor;
107  else if(statement==ID_assign_bitor)
108  new_id=ID_bitor;
109  else
110  {
111  UNREACHABLE;
112  }
113 
114  exprt rhs;
115 
116  const typet &op0_type = to_binary_expr(expr).op0().type();
117 
118  PRECONDITION(
119  op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
120  op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
121 
122  rhs.id(new_id);
123  rhs.copy_to_operands(
124  to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
125  rhs.type() = to_binary_expr(expr).op0().type();
126  rhs.add_source_location() = expr.source_location();
127 
128  if(
129  result_is_used && !address_taken &&
130  needs_cleaning(to_binary_expr(expr).op0()))
131  {
132  make_temp_symbol(rhs, "assign", dest, mode);
133  replacement_expr_opt = rhs;
134  }
135 
136  exprt new_lhs = skip_typecast(to_binary_expr(expr).op0());
137  rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
138  rhs.add_source_location() = expr.source_location();
139  code_assignt assignment(new_lhs, rhs);
140  assignment.add_source_location()=expr.source_location();
141 
142  convert(assignment, dest, mode);
143  }
144  else
145  UNREACHABLE;
146 
147  // revert assignment in the expression to its LHS
148  if(replacement_expr_opt.has_value())
149  {
150  exprt new_lhs =
151  typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type());
152  expr.swap(new_lhs);
153  }
154  else if(result_is_used)
155  {
156  exprt lhs = to_binary_expr(expr).op0();
157  // assign_* statements can have an lhs operand with a different type than
158  // that of the overall expression, because of integer promotion (which may
159  // have introduced casts to the lhs).
160  if(expr.type() != lhs.type())
161  {
162  // Skip over those type casts, but also
163  // make sure the resulting expression has the same type as before.
165  lhs.id() == ID_typecast,
166  id2string(expr.id()) +
167  " expression with different operand type expected to have a "
168  "typecast");
170  to_typecast_expr(lhs).op().type() == expr.type(),
171  id2string(expr.id()) + " type mismatch in lhs operand");
172  lhs = to_typecast_expr(lhs).op();
173  }
174  expr.swap(lhs);
175  }
176  else
177  expr.make_nil();
178 }
179 
181  side_effect_exprt &expr,
182  goto_programt &dest,
183  bool result_is_used,
184  bool address_taken,
185  const irep_idt &mode)
186 {
188  expr.operands().size() == 1,
189  "preincrement/predecrement must have one operand",
190  expr.find_source_location());
191 
192  const irep_idt statement=expr.get_statement();
193 
195  statement == ID_preincrement || statement == ID_predecrement,
196  "expects preincrement or predecrement");
197 
198  exprt rhs;
200 
201  if(statement==ID_preincrement)
202  rhs.id(ID_plus);
203  else
204  rhs.id(ID_minus);
205 
206  const auto &op = to_unary_expr(expr).op();
207  const typet &op_type = op.type();
208 
209  PRECONDITION(
210  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
211  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
212 
213  typet constant_type;
214 
215  if(op_type.id() == ID_pointer)
216  constant_type = index_type();
217  else if(is_number(op_type))
218  constant_type = op_type;
219  else
220  {
221  UNREACHABLE;
222  }
223 
224  exprt constant;
225 
226  if(constant_type.id() == ID_complex)
227  {
228  exprt real = from_integer(1, constant_type.subtype());
229  exprt imag = from_integer(0, constant_type.subtype());
230  constant = complex_exprt(real, imag, to_complex_type(constant_type));
231  }
232  else
233  constant = from_integer(1, constant_type);
234 
235  rhs.add_to_operands(op, std::move(constant));
236  rhs.type() = op.type();
237 
238  const bool cannot_use_lhs =
239  result_is_used && !address_taken && needs_cleaning(op);
240  if(cannot_use_lhs)
241  make_temp_symbol(rhs, "pre", dest, mode);
242 
243  code_assignt assignment(op, rhs);
244  assignment.add_source_location()=expr.find_source_location();
245 
246  convert(assignment, dest, mode);
247 
248  if(result_is_used)
249  {
250  if(cannot_use_lhs)
251  expr.swap(rhs);
252  else
253  {
254  // revert to argument of pre-inc/pre-dec
255  exprt tmp = op;
256  expr.swap(tmp);
257  }
258  }
259  else
260  expr.make_nil();
261 }
262 
264  side_effect_exprt &expr,
265  goto_programt &dest,
266  const irep_idt &mode,
267  bool result_is_used)
268 {
269  goto_programt tmp1, tmp2;
270 
271  // we have ...(op++)...
272 
274  expr.operands().size() == 1,
275  "postincrement/postdecrement must have one operand",
276  expr.find_source_location());
277 
278  const irep_idt statement=expr.get_statement();
279 
281  statement == ID_postincrement || statement == ID_postdecrement,
282  "expects postincrement or postdecrement");
283 
284  exprt rhs;
286 
287  if(statement==ID_postincrement)
288  rhs.id(ID_plus);
289  else
290  rhs.id(ID_minus);
291 
292  const auto &op = to_unary_expr(expr).op();
293  const typet &op_type = op.type();
294 
295  PRECONDITION(
296  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
297  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
298 
299  typet constant_type;
300 
301  if(op_type.id() == ID_pointer)
302  constant_type = index_type();
303  else if(is_number(op_type))
304  constant_type = op_type;
305  else
306  {
307  UNREACHABLE;
308  }
309 
310  exprt constant;
311 
312  if(constant_type.id() == ID_complex)
313  {
314  exprt real = from_integer(1, constant_type.subtype());
315  exprt imag = from_integer(0, constant_type.subtype());
316  constant = complex_exprt(real, imag, to_complex_type(constant_type));
317  }
318  else
319  constant = from_integer(1, constant_type);
320 
321  rhs.add_to_operands(op, std::move(constant));
322  rhs.type() = op.type();
323 
324  code_assignt assignment(op, rhs);
325  assignment.add_source_location()=expr.find_source_location();
326 
327  convert(assignment, tmp2, mode);
328 
329  // fix up the expression, if needed
330 
331  if(result_is_used)
332  {
333  exprt tmp = op;
334  make_temp_symbol(tmp, "post", dest, mode);
335  expr.swap(tmp);
336  }
337  else
338  expr.make_nil();
339 
340  dest.destructive_append(tmp1);
341  dest.destructive_append(tmp2);
342 }
343 
346  goto_programt &dest,
347  const irep_idt &mode,
348  bool result_is_used)
349 {
350  if(!result_is_used)
351  {
352  code_function_callt call(expr.function(), expr.arguments());
353  call.add_source_location()=expr.source_location();
354  convert_function_call(call, dest, mode);
355  expr.make_nil();
356  return;
357  }
358 
359  // get name of function, if available
360  std::string new_base_name = "return_value";
361  irep_idt new_symbol_mode = mode;
362 
363  if(expr.function().id() == ID_symbol)
364  {
365  const irep_idt &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.function(), expr.arguments());
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(to_unary_expr(expr).op());
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  if(result_is_used)
460  {
461  const symbolt &new_symbol = get_fresh_aux_symbol(
462  expr.type(),
464  "malloc_value",
465  expr.source_location(),
466  mode,
467  symbol_table);
468 
469  code_declt decl(new_symbol.symbol_expr());
470  decl.add_source_location()=new_symbol.location;
471  convert_decl(decl, dest, mode);
472 
473  code_assignt call(new_symbol.symbol_expr(), expr);
474  call.add_source_location()=expr.source_location();
475 
476  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
477 
478  convert(call, dest, mode);
479  }
480  else
481  {
482  convert(code_expressiont(std::move(expr)), dest, mode);
483  }
484 }
485 
487  side_effect_exprt &expr,
488  goto_programt &dest)
489 {
490  const irep_idt &mode = expr.get(ID_mode);
492  expr.operands().size() <= 1,
493  "temporary_object takes zero or one operands",
494  expr.find_source_location());
495 
496  symbolt &new_symbol = new_tmp_symbol(
497  expr.type(), "obj", dest, expr.find_source_location(), mode);
498 
499  if(expr.operands().size()==1)
500  {
501  const code_assignt assignment(
502  new_symbol.symbol_expr(), to_unary_expr(expr).op());
503 
504  convert(assignment, dest, mode);
505  }
506 
507  if(expr.find(ID_initializer).is_not_nil())
508  {
510  expr.operands().empty(),
511  "temporary_object takes zero operands",
512  expr.find_source_location());
513  exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
514  replace_new_object(new_symbol.symbol_expr(), initializer);
515 
516  convert(to_code(initializer), dest, mode);
517  }
518 
519  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
520 }
521 
523  side_effect_exprt &expr,
524  goto_programt &dest,
525  const irep_idt &mode,
526  bool result_is_used)
527 {
528  // This is a gcc extension of the form ({ ....; expr; })
529  // The value is that of the final expression.
530  // The expression is copied into a temporary before the
531  // scope is destroyed.
532 
534 
535  if(!result_is_used)
536  {
537  convert(code, dest, mode);
538  expr.make_nil();
539  return;
540  }
541 
543  code.get_statement() == ID_block,
544  "statement_expression takes block as operand",
545  code.find_source_location());
546 
548  !code.operands().empty(),
549  "statement_expression takes non-empty block as operand",
550  expr.find_source_location());
551 
552  // get last statement from block, following labels
554 
555  source_locationt source_location=last.find_source_location();
556 
557  symbolt &new_symbol = new_tmp_symbol(
558  expr.type(), "statement_expression", dest, source_location, mode);
559 
560  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
561  tmp_symbol_expr.add_source_location()=source_location;
562 
563  if(last.get(ID_statement)==ID_expression)
564  {
565  // we turn this into an assignment
567  last=code_assignt(tmp_symbol_expr, e);
568  last.add_source_location()=source_location;
569  }
570  else if(last.get(ID_statement)==ID_assign)
571  {
572  exprt e=to_code_assign(last).lhs();
573  code_assignt assignment(tmp_symbol_expr, e);
574  assignment.add_source_location()=source_location;
575  code.operands().push_back(assignment);
576  }
577  else
578  {
579  UNREACHABLE;
580  }
581 
582  {
583  goto_programt tmp;
584  convert(code, tmp, mode);
585  dest.destructive_append(tmp);
586  }
587 
588  static_cast<exprt &>(expr)=tmp_symbol_expr;
589 }
590 
592  side_effect_exprt &expr,
593  goto_programt &dest,
594  const irep_idt &mode,
595  bool result_is_used,
596  bool address_taken)
597 {
598  const irep_idt &statement=expr.get_statement();
599 
600  if(statement==ID_function_call)
602  to_side_effect_expr_function_call(expr), dest, mode, result_is_used);
603  else if(statement==ID_assign ||
604  statement==ID_assign_plus ||
605  statement==ID_assign_minus ||
606  statement==ID_assign_mult ||
607  statement==ID_assign_div ||
608  statement==ID_assign_bitor ||
609  statement==ID_assign_bitxor ||
610  statement==ID_assign_bitand ||
611  statement==ID_assign_lshr ||
612  statement==ID_assign_ashr ||
613  statement==ID_assign_shl ||
614  statement==ID_assign_mod)
615  remove_assignment(expr, dest, result_is_used, address_taken, mode);
616  else if(statement==ID_postincrement ||
617  statement==ID_postdecrement)
618  remove_post(expr, dest, mode, result_is_used);
619  else if(statement==ID_preincrement ||
620  statement==ID_predecrement)
621  remove_pre(expr, dest, result_is_used, address_taken, mode);
622  else if(statement==ID_cpp_new ||
623  statement==ID_cpp_new_array)
624  remove_cpp_new(expr, dest, result_is_used);
625  else if(statement==ID_cpp_delete ||
626  statement==ID_cpp_delete_array)
627  remove_cpp_delete(expr, dest);
628  else if(statement==ID_allocate)
629  remove_malloc(expr, dest, mode, result_is_used);
630  else if(statement==ID_temporary_object)
631  remove_temporary_object(expr, dest);
632  else if(statement==ID_statement_expression)
633  remove_statement_expression(expr, dest, mode, result_is_used);
634  else if(statement==ID_nondet)
635  {
636  // these are fine
637  }
638  else if(statement==ID_skip)
639  {
640  expr.make_nil();
641  }
642  else if(statement==ID_throw)
643  {
645  expr.find(ID_exception_list), expr.type(), expr.source_location()));
646  code.op0().operands().swap(expr.operands());
647  code.add_source_location() = expr.source_location();
649  std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
650 
651  // the result can't be used, these are void
652  expr.make_nil();
653  }
654  else
655  {
656  UNREACHABLE;
657  }
658 }
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:133
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
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: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
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1876
typet::subtype
const typet & subtype() const
Definition: type.h:47
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:66
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:218
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2187
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:50
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
codet::op0
exprt & op0()
Definition: expr.h:103
goto_convertt::replace_new_object
static void replace_new_object(const exprt &object, exprt &dest)
Definition: goto_convert_side_effect.cpp:399
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
irept::make_nil
void make_nil()
Definition: irep.h:464
typet
The type of an expression, extends irept.
Definition: type.h:28
fresh_symbol.h
Fresh auxiliary symbol creation.
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:24
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:51
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
goto_convert_class.h
Program Transformation.
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
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
side_effect_expr_statement_expressiont::statement
codet & statement()
Definition: std_code.h:2098
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1829
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
to_side_effect_expr_statement_expression
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition: std_code.h:2117
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
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
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:438
mathematical_types.h
Mathematical types.
THROW
@ THROW
Definition: goto_program.h:51
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
goto_convertt::remove_assignment
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:37
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
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
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
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
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
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:452
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:407
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1622
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
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:263
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:609
cprover_prefix.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
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:486
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2166
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
goto_convertt::remove_pre
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:180
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
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
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2205
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:49
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:763
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1849
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:98
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:2156
exprt::operands
operandst & operands()
Definition: expr.h:96
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
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
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1898
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
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:1842