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  const irep_idt &mode)
42 {
43  const irep_idt statement=expr.get_statement();
44 
45  if(statement==ID_assign)
46  {
47  auto &old_assignment = to_side_effect_expr_assign(expr);
48  exprt new_lhs = skip_typecast(old_assignment.lhs());
49  exprt new_rhs =
50  typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
51  code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
52  new_assignment.add_source_location() = expr.source_location();
53 
54  convert_assign(new_assignment, dest, mode);
55  }
56  else if(statement==ID_assign_plus ||
57  statement==ID_assign_minus ||
58  statement==ID_assign_mult ||
59  statement==ID_assign_div ||
60  statement==ID_assign_mod ||
61  statement==ID_assign_shl ||
62  statement==ID_assign_ashr ||
63  statement==ID_assign_lshr ||
64  statement==ID_assign_bitand ||
65  statement==ID_assign_bitxor ||
66  statement==ID_assign_bitor)
67  {
69  expr.operands().size() == 2,
70  id2string(statement) + " expects two arguments",
71  expr.find_source_location());
72 
73  irep_idt new_id;
74 
75  if(statement==ID_assign_plus)
76  new_id=ID_plus;
77  else if(statement==ID_assign_minus)
78  new_id=ID_minus;
79  else if(statement==ID_assign_mult)
80  new_id=ID_mult;
81  else if(statement==ID_assign_div)
82  new_id=ID_div;
83  else if(statement==ID_assign_mod)
84  new_id=ID_mod;
85  else if(statement==ID_assign_shl)
86  new_id=ID_shl;
87  else if(statement==ID_assign_ashr)
88  new_id=ID_ashr;
89  else if(statement==ID_assign_lshr)
90  new_id=ID_lshr;
91  else if(statement==ID_assign_bitand)
92  new_id=ID_bitand;
93  else if(statement==ID_assign_bitxor)
94  new_id=ID_bitxor;
95  else if(statement==ID_assign_bitor)
96  new_id=ID_bitor;
97  else
98  {
100  }
101 
102  exprt rhs;
103 
104  const typet &op0_type = to_binary_expr(expr).op0().type();
105 
106  PRECONDITION(
107  op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
108  op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
109 
110  rhs.id(new_id);
111  rhs.copy_to_operands(
112  to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
113  rhs.type() = to_binary_expr(expr).op0().type();
114  rhs.add_source_location() = expr.source_location();
115 
116  exprt new_lhs = skip_typecast(to_binary_expr(expr).op0());
117  rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
118  rhs.add_source_location() = expr.source_location();
119 
120  code_assignt assignment(new_lhs, rhs);
121  assignment.add_source_location()=expr.source_location();
122 
123  convert(assignment, dest, mode);
124  }
125  else
126  UNREACHABLE;
127 
128  // revert assignment in the expression to its LHS
129  if(result_is_used)
130  {
131  exprt lhs;
132  lhs.swap(to_binary_expr(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  const irep_idt &mode)
144 {
146  expr.operands().size() == 1,
147  "preincrement/predecrement must have one operand",
148  expr.find_source_location());
149 
150  const irep_idt statement=expr.get_statement();
151 
153  statement == ID_preincrement || statement == ID_predecrement,
154  "expects preincrement or 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 auto &op = to_unary_expr(expr).op();
165  const typet &op_type = op.type();
166 
167  PRECONDITION(
168  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
169  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
170 
171  typet constant_type;
172 
173  if(op_type.id() == ID_pointer)
174  constant_type = index_type();
175  else if(is_number(op_type))
176  constant_type = op_type;
177  else
178  {
179  UNREACHABLE;
180  }
181 
182  exprt constant;
183 
184  if(constant_type.id() == ID_complex)
185  {
186  exprt real = from_integer(1, constant_type.subtype());
187  exprt imag = from_integer(0, constant_type.subtype());
188  constant = complex_exprt(real, imag, to_complex_type(constant_type));
189  }
190  else
191  constant = from_integer(1, constant_type);
192 
193  rhs.add_to_operands(op, std::move(constant));
194  rhs.type() = op.type();
195 
196  code_assignt assignment(op, rhs);
197  assignment.add_source_location()=expr.find_source_location();
198 
199  convert(assignment, dest, mode);
200 
201  if(result_is_used)
202  {
203  // revert to argument of pre-inc/pre-dec
204  exprt tmp = op;
205  expr.swap(tmp);
206  }
207  else
208  expr.make_nil();
209 }
210 
212  side_effect_exprt &expr,
213  goto_programt &dest,
214  const irep_idt &mode,
215  bool result_is_used)
216 {
217  goto_programt tmp1, tmp2;
218 
219  // we have ...(op++)...
220 
222  expr.operands().size() == 1,
223  "postincrement/postdecrement must have one operand",
224  expr.find_source_location());
225 
226  const irep_idt statement=expr.get_statement();
227 
229  statement == ID_postincrement || statement == ID_postdecrement,
230  "expects postincrement or postdecrement");
231 
232  exprt rhs;
234 
235  if(statement==ID_postincrement)
236  rhs.id(ID_plus);
237  else
238  rhs.id(ID_minus);
239 
240  const auto &op = to_unary_expr(expr).op();
241  const typet &op_type = op.type();
242 
243  PRECONDITION(
244  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
245  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
246 
247  typet constant_type;
248 
249  if(op_type.id() == ID_pointer)
250  constant_type = index_type();
251  else if(is_number(op_type))
252  constant_type = op_type;
253  else
254  {
255  UNREACHABLE;
256  }
257 
258  exprt constant;
259 
260  if(constant_type.id() == ID_complex)
261  {
262  exprt real = from_integer(1, constant_type.subtype());
263  exprt imag = from_integer(0, constant_type.subtype());
264  constant = complex_exprt(real, imag, to_complex_type(constant_type));
265  }
266  else
267  constant = from_integer(1, constant_type);
268 
269  rhs.add_to_operands(op, std::move(constant));
270  rhs.type() = op.type();
271 
272  code_assignt assignment(op, rhs);
273  assignment.add_source_location()=expr.find_source_location();
274 
275  convert(assignment, tmp2, mode);
276 
277  // fix up the expression, if needed
278 
279  if(result_is_used)
280  {
281  exprt tmp = op;
282  make_temp_symbol(tmp, "post", dest, mode);
283  expr.swap(tmp);
284  }
285  else
286  expr.make_nil();
287 
288  dest.destructive_append(tmp1);
289  dest.destructive_append(tmp2);
290 }
291 
294  goto_programt &dest,
295  const irep_idt &mode,
296  bool result_is_used)
297 {
298  if(!result_is_used)
299  {
300  code_function_callt call(expr.function(), expr.arguments());
301  call.add_source_location()=expr.source_location();
302  convert_function_call(call, dest, mode);
303  expr.make_nil();
304  return;
305  }
306 
307  // get name of function, if available
308  std::string new_base_name = "return_value";
309  irep_idt new_symbol_mode = mode;
310 
311  if(expr.function().id() == ID_symbol)
312  {
313  const irep_idt &identifier =
315  const symbolt &symbol = ns.lookup(identifier);
316 
317  new_base_name+='_';
318  new_base_name+=id2string(symbol.base_name);
319  new_symbol_mode = symbol.mode;
320  }
321 
322  const symbolt &new_symbol = get_fresh_aux_symbol(
323  expr.type(),
325  new_base_name,
326  expr.find_source_location(),
327  new_symbol_mode,
328  symbol_table);
329 
330  {
331  code_declt decl(new_symbol.symbol_expr());
332  decl.add_source_location()=new_symbol.location;
333  convert_decl(decl, dest, mode);
334  }
335 
336  {
337  goto_programt tmp_program2;
338  code_function_callt call(
339  new_symbol.symbol_expr(), expr.function(), expr.arguments());
340  call.add_source_location()=new_symbol.location;
341  convert_function_call(call, dest, mode);
342  }
343 
344  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
345 }
346 
348  const exprt &object,
349  exprt &dest)
350 {
351  if(dest.id()=="new_object")
352  dest=object;
353  else
354  Forall_operands(it, dest)
355  replace_new_object(object, *it);
356 }
357 
359  side_effect_exprt &expr,
360  goto_programt &dest,
361  bool result_is_used)
362 {
363  const symbolt &new_symbol = get_fresh_aux_symbol(
364  expr.type(),
366  "new_ptr",
367  expr.find_source_location(),
368  ID_cpp,
369  symbol_table);
370 
371  code_declt decl(new_symbol.symbol_expr());
372  decl.add_source_location()=new_symbol.location;
373  convert_decl(decl, dest, ID_cpp);
374 
375  const code_assignt call(new_symbol.symbol_expr(), expr);
376 
377  if(result_is_used)
378  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
379  else
380  expr.make_nil();
381 
382  convert(call, dest, ID_cpp);
383 }
384 
386  side_effect_exprt &expr,
387  goto_programt &dest)
388 {
389  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
390 
391  codet tmp(expr.get_statement());
393  tmp.copy_to_operands(to_unary_expr(expr).op());
394  tmp.set(ID_destructor, expr.find(ID_destructor));
395 
396  convert_cpp_delete(tmp, dest);
397 
398  expr.make_nil();
399 }
400 
402  side_effect_exprt &expr,
403  goto_programt &dest,
404  const irep_idt &mode,
405  bool result_is_used)
406 {
407  if(result_is_used)
408  {
409  const symbolt &new_symbol = get_fresh_aux_symbol(
410  expr.type(),
412  "malloc_value",
413  expr.source_location(),
414  mode,
415  symbol_table);
416 
417  code_declt decl(new_symbol.symbol_expr());
418  decl.add_source_location()=new_symbol.location;
419  convert_decl(decl, dest, mode);
420 
421  code_assignt call(new_symbol.symbol_expr(), expr);
422  call.add_source_location()=expr.source_location();
423 
424  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
425 
426  convert(call, dest, mode);
427  }
428  else
429  {
430  convert(code_expressiont(std::move(expr)), dest, mode);
431  }
432 }
433 
435  side_effect_exprt &expr,
436  goto_programt &dest)
437 {
438  const irep_idt &mode = expr.get(ID_mode);
440  expr.operands().size() <= 1,
441  "temporary_object takes zero or one operands",
442  expr.find_source_location());
443 
444  symbolt &new_symbol = new_tmp_symbol(
445  expr.type(), "obj", dest, expr.find_source_location(), mode);
446 
447  if(expr.operands().size()==1)
448  {
449  const code_assignt assignment(
450  new_symbol.symbol_expr(), to_unary_expr(expr).op());
451 
452  convert(assignment, dest, mode);
453  }
454 
455  if(expr.find(ID_initializer).is_not_nil())
456  {
458  expr.operands().empty(),
459  "temporary_object takes zero operands",
460  expr.find_source_location());
461  exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
462  replace_new_object(new_symbol.symbol_expr(), initializer);
463 
464  convert(to_code(initializer), dest, mode);
465  }
466 
467  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
468 }
469 
471  side_effect_exprt &expr,
472  goto_programt &dest,
473  const irep_idt &mode,
474  bool result_is_used)
475 {
476  // This is a gcc extension of the form ({ ....; expr; })
477  // The value is that of the final expression.
478  // The expression is copied into a temporary before the
479  // scope is destroyed.
480 
482 
483  if(!result_is_used)
484  {
485  convert(code, dest, mode);
486  expr.make_nil();
487  return;
488  }
489 
491  code.get_statement() == ID_block,
492  "statement_expression takes block as operand",
493  code.find_source_location());
494 
496  !code.operands().empty(),
497  "statement_expression takes non-empty block as operand",
498  expr.find_source_location());
499 
500  // get last statement from block, following labels
502 
503  source_locationt source_location=last.find_source_location();
504 
505  symbolt &new_symbol = new_tmp_symbol(
506  expr.type(), "statement_expression", dest, source_location, mode);
507 
508  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
509  tmp_symbol_expr.add_source_location()=source_location;
510 
511  if(last.get(ID_statement)==ID_expression)
512  {
513  // we turn this into an assignment
515  last=code_assignt(tmp_symbol_expr, e);
516  last.add_source_location()=source_location;
517  }
518  else if(last.get(ID_statement)==ID_assign)
519  {
520  exprt e=to_code_assign(last).lhs();
521  code_assignt assignment(tmp_symbol_expr, e);
522  assignment.add_source_location()=source_location;
523  code.operands().push_back(assignment);
524  }
525  else
526  {
527  UNREACHABLE;
528  }
529 
530  {
531  goto_programt tmp;
532  convert(code, tmp, mode);
533  dest.destructive_append(tmp);
534  }
535 
536  static_cast<exprt &>(expr)=tmp_symbol_expr;
537 }
538 
540  side_effect_exprt &expr,
541  goto_programt &dest,
542  const irep_idt &mode,
543  bool result_is_used)
544 {
545  const irep_idt &statement=expr.get_statement();
546 
547  if(statement==ID_function_call)
549  to_side_effect_expr_function_call(expr), dest, mode, result_is_used);
550  else if(statement==ID_assign ||
551  statement==ID_assign_plus ||
552  statement==ID_assign_minus ||
553  statement==ID_assign_mult ||
554  statement==ID_assign_div ||
555  statement==ID_assign_bitor ||
556  statement==ID_assign_bitxor ||
557  statement==ID_assign_bitand ||
558  statement==ID_assign_lshr ||
559  statement==ID_assign_ashr ||
560  statement==ID_assign_shl ||
561  statement==ID_assign_mod)
562  remove_assignment(expr, dest, result_is_used, mode);
563  else if(statement==ID_postincrement ||
564  statement==ID_postdecrement)
565  remove_post(expr, dest, mode, result_is_used);
566  else if(statement==ID_preincrement ||
567  statement==ID_predecrement)
568  remove_pre(expr, dest, result_is_used, mode);
569  else if(statement==ID_cpp_new ||
570  statement==ID_cpp_new_array)
571  remove_cpp_new(expr, dest, result_is_used);
572  else if(statement==ID_cpp_delete ||
573  statement==ID_cpp_delete_array)
574  remove_cpp_delete(expr, dest);
575  else if(statement==ID_allocate)
576  remove_malloc(expr, dest, mode, result_is_used);
577  else if(statement==ID_temporary_object)
578  remove_temporary_object(expr, dest);
579  else if(statement==ID_statement_expression)
580  remove_statement_expression(expr, dest, mode, result_is_used);
581  else if(statement==ID_nondet)
582  {
583  // these are fine
584  }
585  else if(statement==ID_skip)
586  {
587  expr.make_nil();
588  }
589  else if(statement==ID_throw)
590  {
592  expr.find(ID_exception_list), expr.type(), expr.source_location()));
593  code.op0().operands().swap(expr.operands());
594  code.add_source_location() = expr.source_location();
596  std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
597 
598  // the result can't be used, these are void
599  expr.make_nil();
600  }
601  else
602  {
603  UNREACHABLE;
604  }
605 }
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:150
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:2021
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1844
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2182
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
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:102
goto_convertt::replace_new_object
static void replace_new_object(const exprt &object, exprt &dest)
Definition: goto_convert_side_effect.cpp:347
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:426
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
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:2117
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:686
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:139
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:292
side_effect_expr_statement_expressiont::statement
codet & statement()
Definition: std_code.h:2075
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
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:539
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:2094
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:1802
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:678
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:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
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:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
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:231
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
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:470
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:401
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:358
irept::swap
void swap(irept &irep)
Definition: irep.h:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1672
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
goto_convertt::remove_cpp_delete
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:385
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:211
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:606
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:672
to_side_effect_expr_assign
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:2043
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
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:434
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
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:37
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
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:2161
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:157
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2200
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:755
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1817
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:97
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:2151
exprt::operands
operandst & operands()
Definition: expr.h:95
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
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:179
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
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:1866
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
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:1825