cprover
Loading...
Searching...
No Matches
goto_convert_side_effect.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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/bitvector_expr.h>
16#include <util/c_types.h>
17#include <util/expr_util.h>
18#include <util/fresh_symbol.h>
20#include <util/std_expr.h>
21#include <util/symbol.h>
22
23#include <ansi-c/c_expr.h>
24
26{
27 for(const auto &op : expr.operands())
28 {
29 if(has_function_call(op))
30 return true;
31 }
32
33 if(expr.id()==ID_side_effect &&
34 expr.get(ID_statement)==ID_function_call)
35 return true;
36
37 return false;
38}
39
42 goto_programt &dest,
43 bool result_is_used,
44 bool address_taken,
45 const irep_idt &mode)
46{
47 const irep_idt statement=expr.get_statement();
48
49 optionalt<exprt> replacement_expr_opt;
50
51 if(statement==ID_assign)
52 {
53 auto &old_assignment = to_side_effect_expr_assign(expr);
54 exprt new_lhs = skip_typecast(old_assignment.lhs());
55
56 if(
57 result_is_used && !address_taken &&
58 assignment_lhs_needs_temporary(old_assignment.lhs()))
59 {
60 if(!old_assignment.rhs().is_constant())
61 make_temp_symbol(old_assignment.rhs(), "assign", dest, mode);
62
63 replacement_expr_opt =
64 typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
65 }
66
67 exprt new_rhs =
68 typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
69 code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
70 new_assignment.add_source_location() = expr.source_location();
71
72 convert_assign(new_assignment, dest, mode);
73 }
74 else if(statement==ID_assign_plus ||
75 statement==ID_assign_minus ||
76 statement==ID_assign_mult ||
77 statement==ID_assign_div ||
78 statement==ID_assign_mod ||
79 statement==ID_assign_shl ||
80 statement==ID_assign_ashr ||
81 statement==ID_assign_lshr ||
82 statement==ID_assign_bitand ||
83 statement==ID_assign_bitxor ||
84 statement==ID_assign_bitor)
85 {
87 expr.operands().size() == 2,
88 id2string(statement) + " expects two arguments",
90
91 irep_idt new_id;
92
93 if(statement==ID_assign_plus)
94 new_id=ID_plus;
95 else if(statement==ID_assign_minus)
96 new_id=ID_minus;
97 else if(statement==ID_assign_mult)
98 new_id=ID_mult;
99 else if(statement==ID_assign_div)
100 new_id=ID_div;
101 else if(statement==ID_assign_mod)
102 new_id=ID_mod;
103 else if(statement==ID_assign_shl)
104 new_id=ID_shl;
105 else if(statement==ID_assign_ashr)
106 new_id=ID_ashr;
107 else if(statement==ID_assign_lshr)
108 new_id=ID_lshr;
109 else if(statement==ID_assign_bitand)
110 new_id=ID_bitand;
111 else if(statement==ID_assign_bitxor)
112 new_id=ID_bitxor;
113 else if(statement==ID_assign_bitor)
114 new_id=ID_bitor;
115 else
116 {
118 }
119
120 const binary_exprt &binary_expr = to_binary_expr(expr);
121 exprt new_lhs = skip_typecast(binary_expr.op0());
122 const typet &op0_type = binary_expr.op0().type();
123
125 op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
126 op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
127
128 exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()};
130
131 if(
132 result_is_used && !address_taken &&
133 assignment_lhs_needs_temporary(binary_expr.op0()))
134 {
135 make_temp_symbol(rhs, "assign", dest, mode);
136 replacement_expr_opt =
138 }
139
140 rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
142 code_assignt assignment(new_lhs, rhs);
143 assignment.add_source_location()=expr.source_location();
144
145 convert(assignment, dest, mode);
146 }
147 else
149
150 // revert assignment in the expression to its LHS
151 if(replacement_expr_opt.has_value())
152 {
153 exprt new_lhs =
154 typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type());
155 expr.swap(new_lhs);
156 }
157 else if(result_is_used)
158 {
159 exprt lhs = to_binary_expr(expr).op0();
160 // assign_* statements can have an lhs operand with a different type than
161 // that of the overall expression, because of integer promotion (which may
162 // have introduced casts to the lhs).
163 if(expr.type() != lhs.type())
164 {
165 // Skip over those type casts, but also
166 // make sure the resulting expression has the same type as before.
168 lhs.id() == ID_typecast,
169 id2string(expr.id()) +
170 " expression with different operand type expected to have a "
171 "typecast");
173 to_typecast_expr(lhs).op().type() == expr.type(),
174 id2string(expr.id()) + " type mismatch in lhs operand");
175 lhs = to_typecast_expr(lhs).op();
176 }
177 expr.swap(lhs);
178 }
179 else
180 expr.make_nil();
181}
182
184 side_effect_exprt &expr,
185 goto_programt &dest,
186 bool result_is_used,
187 bool address_taken,
188 const irep_idt &mode)
189{
191 expr.operands().size() == 1,
192 "preincrement/predecrement must have one operand",
193 expr.find_source_location());
194
195 const irep_idt statement=expr.get_statement();
196
198 statement == ID_preincrement || statement == ID_predecrement,
199 "expects preincrement or predecrement");
200
201 const auto &op = to_unary_expr(expr).op();
202 const typet &op_type = op.type();
203
205 op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
206 op_type.id() != ID_c_bool && op_type.id() != ID_bool);
207
208 typet constant_type;
209
210 if(op_type.id() == ID_pointer)
211 constant_type = c_index_type();
212 else if(is_number(op_type))
213 constant_type = op_type;
214 else
215 {
217 }
218
219 exprt constant;
220
221 if(constant_type.id() == ID_complex)
222 {
223 exprt real = from_integer(1, to_complex_type(constant_type).subtype());
224 exprt imag = from_integer(0, to_complex_type(constant_type).subtype());
225 constant = complex_exprt(real, imag, to_complex_type(constant_type));
226 }
227 else
228 constant = from_integer(1, constant_type);
229
230 exprt rhs = binary_exprt{
231 op, statement == ID_preincrement ? ID_plus : ID_minus, std::move(constant)};
233
234 // Is there a typecast, e.g., for _Bool? If so, transform
235 // t1(op : t2) := op+1 --> op := t2(op+1)
236 exprt lhs;
237 if(op.id() == ID_typecast)
238 {
239 lhs = to_typecast_expr(op).op();
240 rhs = typecast_exprt(rhs, lhs.type());
241 }
242 else
243 {
244 lhs = op;
245 }
246
247 const bool cannot_use_lhs =
248 result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs);
249 if(cannot_use_lhs)
250 make_temp_symbol(rhs, "pre", dest, mode);
251
252 code_assignt assignment(lhs, rhs);
253 assignment.add_source_location()=expr.find_source_location();
254
255 convert(assignment, dest, mode);
256
257 if(result_is_used)
258 {
259 if(cannot_use_lhs)
260 {
261 auto tmp = typecast_exprt::conditional_cast(rhs, expr.type());
262 expr.swap(tmp);
263 }
264 else
265 {
266 // revert to argument of pre-inc/pre-dec
267 auto tmp = typecast_exprt::conditional_cast(lhs, expr.type());
268 expr.swap(tmp);
269 }
270 }
271 else
272 expr.make_nil();
273}
274
276 side_effect_exprt &expr,
277 goto_programt &dest,
278 const irep_idt &mode,
279 bool result_is_used)
280{
281 goto_programt tmp1, tmp2;
282
283 // we have ...(op++)...
284
286 expr.operands().size() == 1,
287 "postincrement/postdecrement must have one operand",
288 expr.find_source_location());
289
290 const irep_idt statement=expr.get_statement();
291
293 statement == ID_postincrement || statement == ID_postdecrement,
294 "expects postincrement or postdecrement");
295
296 const auto &op = to_unary_expr(expr).op();
297 const typet &op_type = op.type();
298
300 op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
301 op_type.id() != ID_c_bool && op_type.id() != ID_bool);
302
303 typet constant_type;
304
305 if(op_type.id() == ID_pointer)
306 constant_type = c_index_type();
307 else if(is_number(op_type))
308 constant_type = op_type;
309 else
310 {
312 }
313
314 exprt constant;
315
316 if(constant_type.id() == ID_complex)
317 {
318 exprt real = from_integer(1, to_complex_type(constant_type).subtype());
319 exprt imag = from_integer(0, to_complex_type(constant_type).subtype());
320 constant = complex_exprt(real, imag, to_complex_type(constant_type));
321 }
322 else
323 constant = from_integer(1, constant_type);
324
325 binary_exprt rhs{
326 op,
327 statement == ID_postincrement ? ID_plus : ID_minus,
328 std::move(constant)};
329 rhs.add_source_location() = expr.source_location();
330
331 code_assignt assignment(op, rhs);
332 assignment.add_source_location()=expr.find_source_location();
333
334 convert(assignment, tmp2, mode);
335
336 // fix up the expression, if needed
337
338 if(result_is_used)
339 {
340 exprt tmp = op;
341 std::string suffix = "post";
342 if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(tmp))
343 {
344 const irep_idt &base_name = ns.lookup(*sym_expr).base_name;
345 suffix += "_" + id2string(base_name);
346 }
347
348 make_temp_symbol(tmp, suffix, dest, mode);
349 expr.swap(tmp);
350 }
351 else
352 expr.make_nil();
353
354 dest.destructive_append(tmp1);
355 dest.destructive_append(tmp2);
356}
357
360 goto_programt &dest,
361 const irep_idt &mode,
362 bool result_is_used)
363{
364 if(!result_is_used)
365 {
366 code_function_callt call(expr.function(), expr.arguments());
368 convert_function_call(call, dest, mode);
369 expr.make_nil();
370 return;
371 }
372
373 // get name of function, if available
374 std::string new_base_name = "return_value";
375 irep_idt new_symbol_mode = mode;
376
377 if(expr.function().id() == ID_symbol)
378 {
379 const irep_idt &identifier =
381 const symbolt &symbol = ns.lookup(identifier);
382
383 new_base_name+='_';
384 new_base_name+=id2string(symbol.base_name);
385 new_symbol_mode = symbol.mode;
386 }
387
388 const symbolt &new_symbol = get_fresh_aux_symbol(
389 expr.type(),
391 new_base_name,
393 new_symbol_mode,
395
396 {
397 code_frontend_declt decl(new_symbol.symbol_expr());
398 decl.add_source_location()=new_symbol.location;
399 convert_frontend_decl(decl, dest, mode);
400 }
401
402 {
403 goto_programt tmp_program2;
405 new_symbol.symbol_expr(), expr.function(), expr.arguments());
406 call.add_source_location()=new_symbol.location;
407 convert_function_call(call, dest, mode);
408 }
409
410 static_cast<exprt &>(expr)=new_symbol.symbol_expr();
411}
412
414 const exprt &object,
415 exprt &dest)
416{
417 if(dest.id()=="new_object")
418 dest=object;
419 else
420 Forall_operands(it, dest)
421 replace_new_object(object, *it);
422}
423
425 side_effect_exprt &expr,
426 goto_programt &dest,
427 bool result_is_used)
428{
429 const symbolt &new_symbol = get_fresh_aux_symbol(
430 expr.type(),
432 "new_ptr",
434 ID_cpp,
436
437 code_frontend_declt decl(new_symbol.symbol_expr());
438 decl.add_source_location()=new_symbol.location;
439 convert_frontend_decl(decl, dest, ID_cpp);
440
441 const code_assignt call(new_symbol.symbol_expr(), expr);
442
443 if(result_is_used)
444 static_cast<exprt &>(expr)=new_symbol.symbol_expr();
445 else
446 expr.make_nil();
447
448 convert(call, dest, ID_cpp);
449}
450
452 side_effect_exprt &expr,
453 goto_programt &dest)
454{
455 DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
456
457 codet tmp(expr.get_statement());
459 tmp.copy_to_operands(to_unary_expr(expr).op());
460 tmp.set(ID_destructor, expr.find(ID_destructor));
461
462 convert_cpp_delete(tmp, dest);
463
464 expr.make_nil();
465}
466
468 side_effect_exprt &expr,
469 goto_programt &dest,
470 const irep_idt &mode,
471 bool result_is_used)
472{
473 if(result_is_used)
474 {
475 const symbolt &new_symbol = get_fresh_aux_symbol(
476 expr.type(),
478 "malloc_value",
479 expr.source_location(),
480 mode,
482
483 code_frontend_declt decl(new_symbol.symbol_expr());
484 decl.add_source_location()=new_symbol.location;
485 convert_frontend_decl(decl, dest, mode);
486
487 code_assignt call(new_symbol.symbol_expr(), expr);
489
490 static_cast<exprt &>(expr)=new_symbol.symbol_expr();
491
492 convert(call, dest, mode);
493 }
494 else
495 {
496 convert(code_expressiont(std::move(expr)), dest, mode);
497 }
498}
499
501 side_effect_exprt &expr,
502 goto_programt &dest)
503{
504 const irep_idt &mode = expr.get(ID_mode);
506 expr.operands().size() <= 1,
507 "temporary_object takes zero or one operands",
508 expr.find_source_location());
509
510 symbolt &new_symbol = new_tmp_symbol(
511 expr.type(), "obj", dest, expr.find_source_location(), mode);
512
513 if(expr.operands().size()==1)
514 {
515 const code_assignt assignment(
516 new_symbol.symbol_expr(), to_unary_expr(expr).op());
517
518 convert(assignment, dest, mode);
519 }
520
521 if(expr.find(ID_initializer).is_not_nil())
522 {
524 expr.operands().empty(),
525 "temporary_object takes zero operands",
526 expr.find_source_location());
527 exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
528 replace_new_object(new_symbol.symbol_expr(), initializer);
529
530 convert(to_code(initializer), dest, mode);
531 }
532
533 static_cast<exprt &>(expr)=new_symbol.symbol_expr();
534}
535
537 side_effect_exprt &expr,
538 goto_programt &dest,
539 const irep_idt &mode,
540 bool result_is_used)
541{
542 // This is a gcc extension of the form ({ ....; expr; })
543 // The value is that of the final expression.
544 // The expression is copied into a temporary before the
545 // scope is destroyed.
546
548
549 if(!result_is_used)
550 {
551 convert(code, dest, mode);
552 expr.make_nil();
553 return;
554 }
555
557 code.get_statement() == ID_block,
558 "statement_expression takes block as operand",
559 code.find_source_location());
560
562 !code.operands().empty(),
563 "statement_expression takes non-empty block as operand",
564 expr.find_source_location());
565
566 // get last statement from block, following labels
568
569 source_locationt source_location=last.find_source_location();
570
571 symbolt &new_symbol = new_tmp_symbol(
572 expr.type(), "statement_expression", dest, source_location, mode);
573
574 symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
575 tmp_symbol_expr.add_source_location()=source_location;
576
577 if(last.get(ID_statement)==ID_expression)
578 {
579 // we turn this into an assignment
581 last=code_assignt(tmp_symbol_expr, e);
582 last.add_source_location()=source_location;
583 }
584 else if(last.get(ID_statement)==ID_assign)
585 {
586 exprt e=to_code_assign(last).lhs();
587 code_assignt assignment(tmp_symbol_expr, e);
588 assignment.add_source_location()=source_location;
589 code.operands().push_back(assignment);
590 }
591 else
592 {
594 }
595
596 {
597 goto_programt tmp;
598 convert(code, tmp, mode);
599 dest.destructive_append(tmp);
600 }
601
602 static_cast<exprt &>(expr)=tmp_symbol_expr;
603}
604
607 goto_programt &dest,
608 bool result_is_used,
609 const irep_idt &mode)
610{
611 const irep_idt &statement = expr.get_statement();
612 const exprt &lhs = expr.lhs();
613 const exprt &rhs = expr.rhs();
614 const exprt &result = expr.result();
615
616 if(result.type().id() != ID_pointer)
617 {
618 // result of the arithmetic operation is _not_ used, just evaluate side
619 // effects
620 exprt tmp = result;
621 clean_expr(tmp, dest, mode, false);
622
623 // the is-there-an-overflow result may be used
624 if(result_is_used)
625 {
626 binary_overflow_exprt overflow_check{
628 statement,
630 overflow_check.add_source_location() = expr.source_location();
631 expr.swap(overflow_check);
632 }
633 else
634 expr.make_nil();
635 }
636 else
637 {
638 const typet &arith_type = to_pointer_type(result.type()).base_type();
639 irep_idt arithmetic_operation =
640 statement == ID_overflow_plus
641 ? ID_plus
642 : statement == ID_overflow_minus
643 ? ID_minus
644 : statement == ID_overflow_mult ? ID_mult : ID_nil;
645 CHECK_RETURN(arithmetic_operation != ID_nil);
646 exprt overflow_with_result = overflow_result_exprt{
647 typecast_exprt::conditional_cast(lhs, arith_type),
648 arithmetic_operation,
649 typecast_exprt::conditional_cast(rhs, arith_type)};
650 overflow_with_result.add_source_location() = expr.source_location();
651
652 if(result_is_used)
653 make_temp_symbol(overflow_with_result, "overflow_result", dest, mode);
654
655 const struct_typet::componentst &result_comps =
656 to_struct_type(overflow_with_result.type()).components();
657 CHECK_RETURN(result_comps.size() == 2);
658 code_assignt result_assignment{
661 member_exprt{overflow_with_result, result_comps[0]}, arith_type),
662 expr.source_location()};
663 convert_assign(result_assignment, dest, mode);
664
665 if(result_is_used)
666 {
667 member_exprt overflow_check{overflow_with_result, result_comps[1]};
668 overflow_check.add_source_location() = expr.source_location();
669
670 expr.swap(overflow_check);
671 }
672 else
673 expr.make_nil();
674 }
675}
676
678 side_effect_exprt &expr,
679 goto_programt &dest,
680 const irep_idt &mode,
681 bool result_is_used,
682 bool address_taken)
683{
684 const irep_idt &statement=expr.get_statement();
685
686 if(statement==ID_function_call)
688 to_side_effect_expr_function_call(expr), dest, mode, result_is_used);
689 else if(statement==ID_assign ||
690 statement==ID_assign_plus ||
691 statement==ID_assign_minus ||
692 statement==ID_assign_mult ||
693 statement==ID_assign_div ||
694 statement==ID_assign_bitor ||
695 statement==ID_assign_bitxor ||
696 statement==ID_assign_bitand ||
697 statement==ID_assign_lshr ||
698 statement==ID_assign_ashr ||
699 statement==ID_assign_shl ||
700 statement==ID_assign_mod)
701 remove_assignment(expr, dest, result_is_used, address_taken, mode);
702 else if(statement==ID_postincrement ||
703 statement==ID_postdecrement)
704 remove_post(expr, dest, mode, result_is_used);
705 else if(statement==ID_preincrement ||
706 statement==ID_predecrement)
707 remove_pre(expr, dest, result_is_used, address_taken, mode);
708 else if(statement==ID_cpp_new ||
709 statement==ID_cpp_new_array)
710 remove_cpp_new(expr, dest, result_is_used);
711 else if(statement==ID_cpp_delete ||
712 statement==ID_cpp_delete_array)
713 remove_cpp_delete(expr, dest);
714 else if(statement==ID_allocate)
715 remove_malloc(expr, dest, mode, result_is_used);
716 else if(statement==ID_temporary_object)
717 remove_temporary_object(expr, dest);
718 else if(statement==ID_statement_expression)
719 remove_statement_expression(expr, dest, mode, result_is_used);
720 else if(statement==ID_nondet)
721 {
722 // these are fine
723 }
724 else if(statement==ID_skip)
725 {
726 expr.make_nil();
727 }
728 else if(statement==ID_throw)
729 {
731 expr.find(ID_exception_list), expr.type(), expr.source_location()));
732 code.op0().operands().swap(expr.operands());
733 code.add_source_location() = expr.source_location();
735 std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
736
737 // the result can't be used, these are void
738 expr.make_nil();
739 }
740 else if(
741 statement == ID_overflow_plus || statement == ID_overflow_minus ||
742 statement == ID_overflow_mult)
743 {
745 to_side_effect_expr_overflow(expr), dest, result_is_used, mode);
746 }
747 else
748 {
750 }
751}
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
API to expression classes that are internal to the C frontend.
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
Definition c_expr.h:182
bitvector_typet c_index_type()
Definition c_types.cpp:16
A base class for binary expressions.
Definition std_expr.h:583
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A goto_instruction_codet representing an assignment in the program.
codet & find_last_statement()
Definition std_code.cpp:96
codet representation of an expression statement.
Definition std_code.h:1394
const exprt & expression() const
Definition std_code.h:1401
A codet representing the declaration of a local variable.
Definition std_code.h:347
goto_instruction_codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:125
const irep_idt & get_statement() const
Complex constructor from a pair of numbers.
Definition std_expr.h:1858
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
symbol_table_baset & symbol_table
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void remove_overflow(side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
static bool has_function_call(const exprt &expr)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
static void replace_new_object(const exprt &object, exprt &dest)
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
static bool assignment_lhs_needs_temporary(const exprt &lhs)
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
mstreamt & result() const
Definition message.h:409
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3026
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
const typet & base_type() const
The type of the data what we point to.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
exprt::operandst & arguments()
Definition std_code.h:1718
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition c_expr.h:117
A side_effect_exprt representation of a side effect that throws an exception.
Definition std_code.h:1757
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt mode
Language mode.
Definition symbol.h:49
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
#define Forall_operands(it, expr)
Definition expr.h:27
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
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 ...
Fresh auxiliary symbol creation.
Program Transformation.
const code_assignt & to_code_assign(const goto_instruction_codet &code)
@ THROW
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
nonstd::optional< T > optionalt
Definition optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#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:437
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition std_code.h:1669
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition std_code.h:1618
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
const codet & to_code(const exprt &expr)
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1102
Symbol table entry.