cprover
goto_convert.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.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/cprover_prefix.h>
18#include <util/expr_util.h>
19#include <util/fresh_symbol.h>
20#include <util/pointer_expr.h>
21#include <util/prefix.h>
22#include <util/simplify_expr.h>
23#include <util/std_expr.h>
25#include <util/symbol_table.h>
27
28#include "goto_convert_class.h"
29#include "destructor.h"
30#include "remove_skip.h"
31
32static bool is_empty(const goto_programt &goto_program)
33{
34 forall_goto_program_instructions(it, goto_program)
35 if(!is_skip(goto_program, it))
36 return false;
37
38 return true;
39}
40
44{
45 std::map<irep_idt, goto_programt::targett> label_targets;
46
47 // in the first pass collect the labels and the corresponding targets
49 {
50 if(!it->labels.empty())
51 {
52 for(auto label : it->labels)
53 // record the label and the corresponding target
54 label_targets.insert(std::make_pair(label, it));
55 }
56 }
57
58 // in the second pass set the targets
59 for(auto &instruction : dest.instructions)
60 {
61 if(
62 instruction.is_catch() &&
63 instruction.get_code().get_statement() == ID_push_catch)
64 {
65 // Populate `targets` with a GOTO instruction target per
66 // exception handler if it isn't already populated.
67 // (Java handlers, for example, need this finish step; C++
68 // handlers will already be populated by now)
69
70 if(instruction.targets.empty())
71 {
72 bool handler_added=true;
73 const code_push_catcht::exception_listt &handler_list =
74 to_code_push_catch(instruction.get_code()).exception_list();
75
76 for(const auto &handler : handler_list)
77 {
78 // some handlers may not have been converted (if there was no
79 // exception to be caught); in such a situation we abort
80 if(label_targets.find(handler.get_label())==label_targets.end())
81 {
82 handler_added=false;
83 break;
84 }
85 }
86
87 if(!handler_added)
88 continue;
89
90 for(const auto &handler : handler_list)
91 instruction.targets.push_back(label_targets.at(handler.get_label()));
92 }
93 }
94 }
95}
96
97/******************************************************************* \
98
99Function: goto_convertt::finish_gotos
100
101 Inputs:
102
103 Outputs:
104
105 Purpose:
106
107\*******************************************************************/
108
110{
111 for(const auto &g_it : targets.gotos)
112 {
113 goto_programt::instructiont &i=*(g_it.first);
114
115 if(i.is_start_thread())
116 {
117 const irep_idt &goto_label = i.get_code().get(ID_destination);
118
119 labelst::const_iterator l_it=
120 targets.labels.find(goto_label);
121
122 if(l_it == targets.labels.end())
123 {
125 "goto label \'" + id2string(goto_label) + "\' not found",
127 }
128
129 i.targets.push_back(l_it->second.first);
130 }
131 else if(i.is_incomplete_goto())
132 {
133 const irep_idt &goto_label = i.get_code().get(ID_destination);
134
135 labelst::const_iterator l_it=targets.labels.find(goto_label);
136
137 if(l_it == targets.labels.end())
138 {
140 "goto label \'" + id2string(goto_label) + "\' not found",
142 }
143
144 i.complete_goto(l_it->second.first);
145
146 node_indext label_target = l_it->second.second;
147 node_indext goto_target = g_it.second;
148
149 // Compare the currently-live variables on the path of the GOTO and label.
150 // We want to work out what variables should die during the jump.
151 ancestry_resultt intersection_result =
153 goto_target, label_target);
154
155 bool not_prefix =
156 intersection_result.right_depth_below_common_ancestor != 0;
157
158 // If our goto had no variables of note, just skip
159 if(goto_target != 0)
160 {
161 // If the goto recorded a destructor stack, execute as much as is
162 // appropriate for however many automatic variables leave scope.
163 // We don't currently handle variables *entering* scope, which
164 // is illegal for C++ non-pod types and impossible in Java in any case.
165 if(not_prefix)
166 {
168 debug() << "encountered goto '" << goto_label
169 << "' that enters one or more lexical blocks; "
170 << "omitting constructors and destructors" << eom;
171 }
172 else
173 {
175 debug() << "adding goto-destructor code on jump to '" << goto_label
176 << "'" << eom;
177
178 node_indext end_destruct = intersection_result.common_ancestor;
179 goto_programt destructor_code;
181 i.source_location(),
182 destructor_code,
183 mode,
184 end_destruct,
185 goto_target);
186 dest.destructive_insert(g_it.first, destructor_code);
187
188 // This should leave iterators intact, as long as
189 // goto_programt::instructionst is std::list.
190 }
191 }
192 }
193 else
194 {
196 }
197 }
198
199 targets.gotos.clear();
200}
201
203{
204 for(auto &g_it : targets.computed_gotos)
205 {
208 const exprt pointer = destination.pointer();
209
210 // remember the expression for later checks
211 i =
213
214 // insert huge case-split
215 for(const auto &label : targets.labels)
216 {
217 exprt label_expr(ID_label, empty_typet());
218 label_expr.set(ID_identifier, label.first);
219
220 const equal_exprt guard(pointer, address_of_exprt(label_expr));
221
222 goto_program.insert_after(
223 g_it,
225 label.second.first, guard, i.source_location()));
226 }
227 }
228
229 targets.computed_gotos.clear();
230}
231
236{
237 // We cannot use a set of targets, as target iterators
238 // cannot be compared at this stage.
239
240 // collect targets: reset marking
241 for(auto &i : dest.instructions)
243
244 // mark the goto targets
245 unsigned cnt = 0;
246 for(const auto &i : dest.instructions)
247 if(i.is_goto())
248 i.get_target()->target_number = (++cnt);
249
250 for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
251 {
252 if(!it->is_goto())
253 continue;
254
255 auto it_goto_y = std::next(it);
256
257 if(
258 it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
259 !it_goto_y->get_condition().is_true() || it_goto_y->is_target())
260 {
261 continue;
262 }
263
264 auto it_z = std::next(it_goto_y);
265
266 if(it_z == dest.instructions.end())
267 continue;
268
269 // cannot compare iterators, so compare target number instead
270 if(it->get_target()->target_number == it_z->target_number)
271 {
272 it->set_target(it_goto_y->get_target());
273 it->condition_nonconst() = boolean_negate(it->condition());
274 it_goto_y->turn_into_skip();
275 }
276 }
277}
278
280 const codet &code,
281 goto_programt &dest,
282 const irep_idt &mode)
283{
284 goto_convert_rec(code, dest, mode);
285}
286
288 const codet &code,
289 goto_programt &dest,
290 const irep_idt &mode)
291{
292 convert(code, dest, mode);
293
294 finish_gotos(dest, mode);
298}
299
301 const codet &code,
303 goto_programt &dest)
304{
306 code, code.source_location(), type, nil_exprt(), {}));
307}
308
310 const code_labelt &code,
311 goto_programt &dest,
312 const irep_idt &mode)
313{
314 // grab the label
315 const irep_idt &label=code.get_label();
316
317 goto_programt tmp;
318
319 // magic thread creation label.
320 // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
321 // that can be executed in parallel, i.e, a new thread.
322 if(has_prefix(id2string(label), CPROVER_PREFIX "ASYNC_"))
323 {
324 // the body of the thread is expected to be
325 // in the operand.
327 to_code_label(code).code().is_not_nil(),
328 "code() in magic thread creation label is null");
329
330 // replace the magic thread creation label with a
331 // thread block (START_THREAD...END_THREAD).
332 code_blockt thread_body;
333 thread_body.add(to_code_label(code).code());
334 thread_body.add_source_location()=code.source_location();
335 generate_thread_block(thread_body, dest, mode);
336 }
337 else
338 {
339 convert(to_code_label(code).code(), tmp, mode);
340
341 goto_programt::targett target=tmp.instructions.begin();
342 dest.destructive_append(tmp);
343
344 targets.labels.insert(
345 {label, {target, targets.destructor_stack.get_current_node()}});
346 target->labels.push_front(label);
347 }
348}
349
351 const codet &,
353{
354 // ignore for now
355}
356
358 const code_switch_caset &code,
359 goto_programt &dest,
360 const irep_idt &mode)
361{
362 goto_programt tmp;
363 convert(code.code(), tmp, mode);
364
365 goto_programt::targett target=tmp.instructions.begin();
366 dest.destructive_append(tmp);
367
368 // is a default target given?
369
370 if(code.is_default())
371 targets.set_default(target);
372 else
373 {
374 // cases?
375
376 cases_mapt::iterator cases_entry=targets.cases_map.find(target);
377 if(cases_entry==targets.cases_map.end())
378 {
379 targets.cases.push_back(std::make_pair(target, caset()));
380 cases_entry=targets.cases_map.insert(std::make_pair(
381 target, --targets.cases.end())).first;
382 }
383
384 exprt::operandst &case_op_dest=cases_entry->second->second;
385 case_op_dest.push_back(code.case_op());
386 }
387}
388
390 const code_gcc_switch_case_ranget &code,
391 goto_programt &dest,
392 const irep_idt &mode)
393{
394 const auto lb = numeric_cast<mp_integer>(code.lower());
395 const auto ub = numeric_cast<mp_integer>(code.upper());
396
398 lb.has_value() && ub.has_value(),
399 "GCC's switch-case-range statement requires constant bounds",
400 code.find_source_location());
401
402 if(*lb > *ub)
403 {
405 warning() << "GCC's switch-case-range statement with empty case range"
406 << eom;
407 }
408
409 goto_programt tmp;
410 convert(code.code(), tmp, mode);
411
412 goto_programt::targett target = tmp.instructions.begin();
413 dest.destructive_append(tmp);
414
415 cases_mapt::iterator cases_entry = targets.cases_map.find(target);
416 if(cases_entry == targets.cases_map.end())
417 {
418 targets.cases.push_back({target, caset()});
419 cases_entry =
420 targets.cases_map.insert({target, --targets.cases.end()}).first;
421 }
422
423 // create a skeleton for case_guard
424 cases_entry->second->second.push_back(
426 binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}});
427}
428
431 const codet &code,
432 goto_programt &dest,
433 const irep_idt &mode)
434{
435 const irep_idt &statement=code.get_statement();
436
437 if(statement==ID_block)
438 convert_block(to_code_block(code), dest, mode);
439 else if(statement==ID_decl)
441 else if(statement==ID_decl_type)
442 convert_decl_type(code, dest);
443 else if(statement==ID_expression)
444 convert_expression(to_code_expression(code), dest, mode);
445 else if(statement==ID_assign)
446 convert_assign(to_code_assign(code), dest, mode);
447 else if(statement==ID_assert)
448 convert_assert(to_code_assert(code), dest, mode);
449 else if(statement==ID_assume)
450 convert_assume(to_code_assume(code), dest, mode);
451 else if(statement==ID_function_call)
453 else if(statement==ID_label)
454 convert_label(to_code_label(code), dest, mode);
455 else if(statement==ID_gcc_local_label)
456 convert_gcc_local_label(code, dest);
457 else if(statement==ID_switch_case)
458 convert_switch_case(to_code_switch_case(code), dest, mode);
459 else if(statement==ID_gcc_switch_case_range)
461 to_code_gcc_switch_case_range(code), dest, mode);
462 else if(statement==ID_for)
463 convert_for(to_code_for(code), dest, mode);
464 else if(statement==ID_while)
465 convert_while(to_code_while(code), dest, mode);
466 else if(statement==ID_dowhile)
467 convert_dowhile(to_code_dowhile(code), dest, mode);
468 else if(statement==ID_switch)
469 convert_switch(to_code_switch(code), dest, mode);
470 else if(statement==ID_break)
471 convert_break(to_code_break(code), dest, mode);
472 else if(statement==ID_return)
473 convert_return(to_code_frontend_return(code), dest, mode);
474 else if(statement==ID_continue)
475 convert_continue(to_code_continue(code), dest, mode);
476 else if(statement==ID_goto)
477 convert_goto(to_code_goto(code), dest);
478 else if(statement==ID_gcc_computed_goto)
479 convert_gcc_computed_goto(code, dest);
480 else if(statement==ID_skip)
481 convert_skip(code, dest);
482 else if(statement==ID_ifthenelse)
483 convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
484 else if(statement==ID_start_thread)
485 convert_start_thread(code, dest);
486 else if(statement==ID_end_thread)
487 convert_end_thread(code, dest);
488 else if(statement==ID_atomic_begin)
489 convert_atomic_begin(code, dest);
490 else if(statement==ID_atomic_end)
491 convert_atomic_end(code, dest);
492 else if(statement==ID_cpp_delete ||
493 statement=="cpp_delete[]")
494 convert_cpp_delete(code, dest);
495 else if(statement==ID_msc_try_except)
496 convert_msc_try_except(code, dest, mode);
497 else if(statement==ID_msc_try_finally)
498 convert_msc_try_finally(code, dest, mode);
499 else if(statement==ID_msc_leave)
500 convert_msc_leave(code, dest, mode);
501 else if(statement==ID_try_catch) // C++ try/catch
502 convert_try_catch(code, dest, mode);
503 else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
504 convert_CPROVER_try_catch(code, dest, mode);
505 else if(statement==ID_CPROVER_throw) // CPROVER-homemade
506 convert_CPROVER_throw(code, dest, mode);
507 else if(statement==ID_CPROVER_try_finally)
508 convert_CPROVER_try_finally(code, dest, mode);
509 else if(statement==ID_asm)
510 convert_asm(to_code_asm(code), dest);
511 else if(statement==ID_static_assert)
512 {
513 PRECONDITION(code.operands().size() == 2);
514 exprt assertion =
516 simplify(assertion, ns);
518 !assertion.is_false(),
519 "static assertion " + id2string(get_string_constant(code.op1())),
520 code.op0().find_source_location());
521 }
522 else if(statement==ID_dead)
523 copy(code, DEAD, dest);
524 else if(statement==ID_decl_block)
525 {
526 forall_operands(it, code)
527 convert(to_code(*it), dest, mode);
528 }
529 else if(statement==ID_push_catch ||
530 statement==ID_pop_catch ||
531 statement==ID_exception_landingpad)
532 copy(code, CATCH, dest);
533 else
534 copy(code, OTHER, dest);
535
536 // make sure dest is never empty
537 if(dest.instructions.empty())
538 {
540 }
541}
542
544 const code_blockt &code,
545 goto_programt &dest,
546 const irep_idt &mode)
547{
548 const source_locationt &end_location=code.end_location();
549
550 // this saves the index of the destructor stack
551 node_indext old_stack_top =
553
554 // now convert block
555 for(const auto &b_code : code.statements())
556 convert(b_code, dest, mode);
557
558 // see if we need to do any destructors -- may have been processed
559 // in a prior break/continue/return already, don't create dead code
560 if(
561 !dest.empty() && dest.instructions.back().is_goto() &&
562 dest.instructions.back().get_condition().is_true())
563 {
564 // don't do destructors when we are unreachable
565 }
566 else
567 unwind_destructor_stack(end_location, dest, mode, old_stack_top);
568
569 // Set the current node of our destructor stack back to before the block.
571}
572
574 const code_expressiont &code,
575 goto_programt &dest,
576 const irep_idt &mode)
577{
578 exprt expr = code.expression();
579
580 if(expr.id()==ID_if)
581 {
582 // We do a special treatment for c?t:f
583 // by compiling to if(c) t; else f;
584 const if_exprt &if_expr=to_if_expr(expr);
585 code_ifthenelset tmp_code(
586 if_expr.cond(),
587 code_expressiont(if_expr.true_case()),
588 code_expressiont(if_expr.false_case()));
589 tmp_code.add_source_location()=expr.source_location();
592 convert_ifthenelse(tmp_code, dest, mode);
593 }
594 else
595 {
596 clean_expr(expr, dest, mode, false); // result _not_ used
597
598 // Any residual expression?
599 // We keep it to add checks later.
600 if(expr.is_not_nil())
601 {
602 codet tmp=code;
603 tmp.op0()=expr;
605 copy(tmp, OTHER, dest);
606 }
607 }
608}
609
611 const code_frontend_declt &code,
612 goto_programt &dest,
613 const irep_idt &mode)
614{
615 const irep_idt &identifier = code.get_identifier();
616
617 const symbolt &symbol = ns.lookup(identifier);
618
619 if(symbol.is_static_lifetime ||
620 symbol.type.id()==ID_code)
621 return; // this is a SKIP!
622
623 if(code.operands().size()==1)
624 {
625 copy(code, DECL, dest);
626 }
627 else
628 {
629 // this is expected to go away
630 exprt initializer;
631
632 codet tmp=code;
633 initializer=code.op1();
634 tmp.operands().resize(1);
635
636 // Break up into decl and assignment.
637 // Decl must be visible before initializer.
638 copy(tmp, DECL, dest);
639
640 clean_expr(initializer, dest, mode);
641
642 if(initializer.is_not_nil())
643 {
644 code_assignt assign(code.op0(), initializer);
645 assign.add_source_location() = tmp.source_location();
646
647 convert_assign(assign, dest, mode);
648 }
649 }
650
651 // now create a 'dead' instruction -- will be added after the
652 // destructor created below as unwind_destructor_stack pops off the
653 // top of the destructor stack
654 const symbol_exprt symbol_expr(symbol.name, symbol.type);
655
656 {
657 code_deadt code_dead(symbol_expr);
658 targets.destructor_stack.add(code_dead);
659 }
660
661 // do destructor
662 code_function_callt destructor=get_destructor(ns, symbol.type);
663
664 if(destructor.is_not_nil())
665 {
666 // add "this"
667 address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
668 destructor.arguments().push_back(this_expr);
669
670 targets.destructor_stack.add(destructor);
671 }
672}
673
675 const codet &,
677{
678 // we remove these
679}
680
682 const code_assignt &code,
683 goto_programt &dest,
684 const irep_idt &mode)
685{
686 exprt lhs=code.lhs(),
687 rhs=code.rhs();
688
689 clean_expr(lhs, dest, mode);
690
691 if(rhs.id()==ID_side_effect &&
692 rhs.get(ID_statement)==ID_function_call)
693 {
694 const auto &rhs_function_call = to_side_effect_expr_function_call(rhs);
695
697 rhs.operands().size() == 2,
698 "function_call sideeffect takes two operands",
699 rhs.find_source_location());
700
701 Forall_operands(it, rhs)
702 clean_expr(*it, dest, mode);
703
705 lhs,
706 rhs_function_call.function(),
707 rhs_function_call.arguments(),
708 dest,
709 mode);
710 }
711 else if(rhs.id()==ID_side_effect &&
712 (rhs.get(ID_statement)==ID_cpp_new ||
713 rhs.get(ID_statement)==ID_cpp_new_array))
714 {
715 Forall_operands(it, rhs)
716 clean_expr(*it, dest, mode);
717
718 // TODO: This should be done in a separate pass
719 do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
720 }
721 else if(
722 rhs.id() == ID_side_effect &&
723 (rhs.get(ID_statement) == ID_assign ||
724 rhs.get(ID_statement) == ID_postincrement ||
725 rhs.get(ID_statement) == ID_preincrement ||
726 rhs.get(ID_statement) == ID_statement_expression ||
727 rhs.get(ID_statement) == ID_gcc_conditional_expression))
728 {
729 // handle above side effects
730 clean_expr(rhs, dest, mode);
731
732 code_assignt new_assign(code);
733 new_assign.lhs() = lhs;
734 new_assign.rhs() = rhs;
735
736 copy(new_assign, ASSIGN, dest);
737 }
738 else if(rhs.id() == ID_side_effect)
739 {
740 // preserve side effects that will be handled at later stages,
741 // such as allocate, new operators of other languages, e.g. java, etc
742 Forall_operands(it, rhs)
743 clean_expr(*it, dest, mode);
744
745 code_assignt new_assign(code);
746 new_assign.lhs()=lhs;
747 new_assign.rhs()=rhs;
748
749 copy(new_assign, ASSIGN, dest);
750 }
751 else
752 {
753 // do everything else
754 clean_expr(rhs, dest, mode);
755
756 code_assignt new_assign(code);
757 new_assign.lhs()=lhs;
758 new_assign.rhs()=rhs;
759
760 copy(new_assign, ASSIGN, dest);
761 }
762}
763
765 const codet &code,
766 goto_programt &dest)
767{
769 code.operands().size() == 1,
770 "cpp_delete statement takes one operand",
771 code.find_source_location());
772
773 exprt tmp_op=code.op0();
774
775 clean_expr(tmp_op, dest, ID_cpp);
776
777 // we call the destructor, and then free
778 const exprt &destructor=
779 static_cast<const exprt &>(code.find(ID_destructor));
780
781 irep_idt delete_identifier;
782
783 if(code.get_statement()==ID_cpp_delete_array)
784 delete_identifier="__delete_array";
785 else if(code.get_statement()==ID_cpp_delete)
786 delete_identifier="__delete";
787 else
789
790 if(destructor.is_not_nil())
791 {
792 if(code.get_statement()==ID_cpp_delete_array)
793 {
794 // build loop
795 }
796 else if(code.get_statement()==ID_cpp_delete)
797 {
798 // just one object
799 const dereference_exprt deref_op(tmp_op);
800
801 codet tmp_code=to_code(destructor);
802 replace_new_object(deref_op, tmp_code);
803 convert(tmp_code, dest, ID_cpp);
804 }
805 else
807 }
808
809 // now do "free"
810 exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
811
813 to_code_type(delete_symbol.type()).parameters().size() == 1,
814 "delete statement takes 1 parameter");
815
816 typet arg_type=
817 to_code_type(delete_symbol.type()).parameters().front().type();
818
819 code_function_callt delete_call(
820 delete_symbol, {typecast_exprt(tmp_op, arg_type)});
821 delete_call.add_source_location()=code.source_location();
822
823 convert(delete_call, dest, ID_cpp);
824}
825
827 const code_assertt &code,
828 goto_programt &dest,
829 const irep_idt &mode)
830{
831 exprt cond=code.assertion();
832
833 clean_expr(cond, dest, mode);
834
837 t->source_location_nonconst().set(ID_property, ID_assertion);
838 t->source_location_nonconst().set("user-provided", true);
839}
840
842 const codet &code,
843 goto_programt &dest)
844{
846 code, code.source_location(), SKIP, nil_exprt(), {}));
847}
848
850 const code_assumet &code,
851 goto_programt &dest,
852 const irep_idt &mode)
853{
854 exprt op=code.assumption();
855
856 clean_expr(op, dest, mode);
857
859}
860
862 const codet &code,
864 const irep_idt &mode)
865{
866 auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
867 if(assigns.is_not_nil())
868 {
869 PRECONDITION(loop->is_goto());
870 loop->guard.add(ID_C_spec_assigns).swap(assigns.op());
871 }
872
873 auto invariant =
874 static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
875 if(!invariant.is_nil())
876 {
877 if(has_subexpr(invariant, ID_side_effect))
878 {
880 "Loop invariant is not side-effect free.", code.find_source_location());
881 }
882
883 PRECONDITION(loop->is_goto());
884 loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
885 }
886
887 auto decreases_clause =
888 static_cast<const exprt &>(code.find(ID_C_spec_decreases));
889 if(!decreases_clause.is_nil())
890 {
891 if(has_subexpr(decreases_clause, ID_side_effect))
892 {
894 "Decreases clause is not side-effect free.",
895 code.find_source_location());
896 }
897
898 PRECONDITION(loop->is_goto());
899 loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
900 }
901}
902
904 const code_fort &code,
905 goto_programt &dest,
906 const irep_idt &mode)
907{
908 // turn for(A; c; B) { P } into
909 // A; while(c) { P; B; }
910 //-----------------------------
911 // A;
912 // u: sideeffects in c
913 // v: if(!c) goto z;
914 // w: P;
915 // x: B; <-- continue target
916 // y: goto u;
917 // z: ; <-- break target
918
919 // A;
920 if(code.init().is_not_nil())
921 convert(to_code(code.init()), dest, mode);
922
923 exprt cond=code.cond();
924
925 goto_programt sideeffects;
926 clean_expr(cond, sideeffects, mode);
927
928 // save break/continue targets
929 break_continue_targetst old_targets(targets);
930
931 // do the u label
932 goto_programt::targett u=sideeffects.instructions.begin();
933
934 // do the v label
935 goto_programt tmp_v;
937
938 // do the z label
939 goto_programt tmp_z;
942
943 // do the x label
944 goto_programt tmp_x;
945
946 if(code.iter().is_nil())
947 {
949 }
950 else
951 {
952 exprt tmp_B=code.iter();
953
954 clean_expr(tmp_B, tmp_x, mode, false);
955
956 if(tmp_x.instructions.empty())
958 }
959
960 // optimize the v label
961 if(sideeffects.instructions.empty())
962 u=v;
963
964 // set the targets
966 targets.set_continue(tmp_x.instructions.begin());
967
968 // v: if(!c) goto z;
969 *v =
971
972 // do the w label
973 goto_programt tmp_w;
974 convert(code.body(), tmp_w, mode);
975
976 // y: goto u;
977 goto_programt tmp_y;
978 goto_programt::targett y = tmp_y.add(
980
981 // assigns clause, loop invariant and decreases clause
982 convert_loop_contracts(code, y, mode);
983
984 dest.destructive_append(sideeffects);
985 dest.destructive_append(tmp_v);
986 dest.destructive_append(tmp_w);
987 dest.destructive_append(tmp_x);
988 dest.destructive_append(tmp_y);
989 dest.destructive_append(tmp_z);
990
991 // restore break/continue
992 old_targets.restore(targets);
993}
994
996 const code_whilet &code,
997 goto_programt &dest,
998 const irep_idt &mode)
999{
1000 const exprt &cond=code.cond();
1001 const source_locationt &source_location=code.source_location();
1002
1003 // while(c) P;
1004 //--------------------
1005 // v: sideeffects in c
1006 // if(!c) goto z;
1007 // x: P;
1008 // y: goto v; <-- continue target
1009 // z: ; <-- break target
1010
1011 // save break/continue targets
1012 break_continue_targetst old_targets(targets);
1013
1014 // do the z label
1015 goto_programt tmp_z;
1017 tmp_z.add(goto_programt::make_skip(source_location));
1018
1019 goto_programt tmp_branch;
1021 boolean_negate(cond), z, source_location, tmp_branch, mode);
1022
1023 // do the v label
1024 goto_programt::targett v=tmp_branch.instructions.begin();
1025
1026 // y: goto v;
1027 goto_programt tmp_y;
1028 goto_programt::targett y = tmp_y.add(
1030
1031 // set the targets
1032 targets.set_break(z);
1034
1035 // do the x label
1036 goto_programt tmp_x;
1037 convert(code.body(), tmp_x, mode);
1038
1039 // assigns clause, loop invariant and decreases clause
1040 convert_loop_contracts(code, y, mode);
1041
1042 dest.destructive_append(tmp_branch);
1043 dest.destructive_append(tmp_x);
1044 dest.destructive_append(tmp_y);
1045 dest.destructive_append(tmp_z);
1046
1047 // restore break/continue
1048 old_targets.restore(targets);
1049}
1050
1052 const code_dowhilet &code,
1053 goto_programt &dest,
1054 const irep_idt &mode)
1055{
1057 code.operands().size() == 2,
1058 "dowhile takes two operands",
1059 code.find_source_location());
1060
1061 // save source location
1062 source_locationt condition_location=code.cond().find_source_location();
1063
1064 exprt cond=code.cond();
1065
1066 goto_programt sideeffects;
1067 clean_expr(cond, sideeffects, mode);
1068
1069 // do P while(c);
1070 //--------------------
1071 // w: P;
1072 // x: sideeffects in c <-- continue target
1073 // y: if(c) goto w;
1074 // z: ; <-- break target
1075
1076 // save break/continue targets
1077 break_continue_targetst old_targets(targets);
1078
1079 // do the y label
1080 goto_programt tmp_y;
1082 tmp_y.add(goto_programt::make_incomplete_goto(cond, condition_location));
1083
1084 // do the z label
1085 goto_programt tmp_z;
1088
1089 // do the x label
1091 if(sideeffects.instructions.empty())
1092 x=y;
1093 else
1094 x=sideeffects.instructions.begin();
1095
1096 // set the targets
1097 targets.set_break(z);
1099
1100 // do the w label
1101 goto_programt tmp_w;
1102 convert(code.body(), tmp_w, mode);
1103 goto_programt::targett w=tmp_w.instructions.begin();
1104
1105 // y: if(c) goto w;
1106 y->complete_goto(w);
1107
1108 // assigns_clause, loop invariant and decreases clause
1109 convert_loop_contracts(code, y, mode);
1110
1111 dest.destructive_append(tmp_w);
1112 dest.destructive_append(sideeffects);
1113 dest.destructive_append(tmp_y);
1114 dest.destructive_append(tmp_z);
1115
1116 // restore break/continue targets
1117 old_targets.restore(targets);
1118}
1119
1121 const exprt &value,
1122 const exprt::operandst &case_op)
1123{
1124 PRECONDITION(!case_op.empty());
1125
1126 exprt::operandst disjuncts;
1127 disjuncts.reserve(case_op.size());
1128
1129 for(const auto &op : case_op)
1130 {
1131 // could be a skeleton generated by convert_gcc_switch_case_range
1132 if(op.id() == ID_and)
1133 {
1134 const binary_exprt &and_expr = to_binary_expr(op);
1135 PRECONDITION(to_binary_expr(and_expr.op0()).op1().is_nil());
1136 PRECONDITION(to_binary_expr(and_expr.op1()).op0().is_nil());
1137 binary_exprt skeleton = and_expr;
1138 to_binary_expr(skeleton.op0()).op1() = value;
1139 to_binary_expr(skeleton.op1()).op0() = value;
1140 disjuncts.push_back(skeleton);
1141 }
1142 else
1143 disjuncts.push_back(equal_exprt(value, op));
1144 }
1145
1146 return disjunction(disjuncts);
1147}
1148
1150 const code_switcht &code,
1151 goto_programt &dest,
1152 const irep_idt &mode)
1153{
1154 // switch(v) {
1155 // case x: Px;
1156 // case y: Py;
1157 // ...
1158 // default: Pd;
1159 // }
1160 // --------------------
1161 // location
1162 // x: if(v==x) goto X;
1163 // y: if(v==y) goto Y;
1164 // goto d;
1165 // X: Px;
1166 // Y: Py;
1167 // d: Pd;
1168 // z: ;
1169
1170 // we first add a 'location' node for the switch statement,
1171 // which would otherwise not be recorded
1173
1174 // get the location of the end of the body, but
1175 // default to location of switch, if none
1176 source_locationt body_end_location=
1177 code.body().get_statement()==ID_block?
1179 code.source_location();
1180
1181 // do the value we switch over
1182 exprt argument=code.value();
1183
1184 goto_programt sideeffects;
1185 clean_expr(argument, sideeffects, mode);
1186
1187 // Avoid potential performance penalties caused by evaluating the value
1188 // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't
1189 // necessarily the right check here, and we may need to introduce a different
1190 // way of identifying the class of non-trivial expressions that warrant
1191 // introduction of a temporary.
1192 if(needs_cleaning(argument))
1193 {
1194 symbolt &new_symbol = new_tmp_symbol(
1195 argument.type(),
1196 "switch_value",
1197 sideeffects,
1198 code.source_location(),
1199 mode);
1200
1201 code_assignt copy_value{
1202 new_symbol.symbol_expr(), argument, code.source_location()};
1203 convert(copy_value, sideeffects, mode);
1204
1205 argument = new_symbol.symbol_expr();
1206 }
1207
1208 // save break/default/cases targets
1209 break_switch_targetst old_targets(targets);
1210
1211 // do the z label
1212 goto_programt tmp_z;
1214 tmp_z.add(goto_programt::make_skip(body_end_location));
1215
1216 // set the new targets -- continue stays as is
1217 targets.set_break(z);
1219 targets.cases.clear();
1220 targets.cases_map.clear();
1221
1222 goto_programt tmp;
1223 convert(code.body(), tmp, mode);
1224
1225 goto_programt tmp_cases;
1226
1227 // The case number represents which case this corresponds to in the sequence
1228 // of case statements.
1229 //
1230 // switch (x)
1231 // {
1232 // case 2: // case_number 1
1233 // ...;
1234 // case 3: // case_number 2
1235 // ...;
1236 // case 10: // case_number 3
1237 // ...;
1238 // }
1239 size_t case_number=1;
1240 for(auto &case_pair : targets.cases)
1241 {
1242 const caset &case_ops=case_pair.second;
1243
1244 if (case_ops.empty())
1245 continue;
1246
1247 exprt guard_expr=case_guard(argument, case_ops);
1248
1249 source_locationt source_location=case_ops.front().find_source_location();
1250 source_location.set_case_number(std::to_string(case_number));
1251 case_number++;
1252 guard_expr.add_source_location()=source_location;
1253
1254 tmp_cases.add(goto_programt::make_goto(
1255 case_pair.first, std::move(guard_expr), source_location));
1256 }
1257
1258 tmp_cases.add(goto_programt::make_goto(
1259 targets.default_target, targets.default_target->source_location()));
1260
1261 dest.destructive_append(sideeffects);
1262 dest.destructive_append(tmp_cases);
1263 dest.destructive_append(tmp);
1264 dest.destructive_append(tmp_z);
1265
1266 // restore old targets
1267 old_targets.restore(targets);
1268}
1269
1271 const code_breakt &code,
1272 goto_programt &dest,
1273 const irep_idt &mode)
1274{
1276 targets.break_set, "break without target", code.find_source_location());
1277
1278 // need to process destructor stack
1280 code.source_location(), dest, mode, targets.break_stack_node);
1281
1282 // add goto
1283 dest.add(
1285}
1286
1288 const code_frontend_returnt &code,
1289 goto_programt &dest,
1290 const irep_idt &mode)
1291{
1292 if(!targets.return_set)
1293 {
1295 "return without target", code.find_source_location());
1296 }
1297
1299 code.operands().empty() || code.operands().size() == 1,
1300 "return takes none or one operand",
1301 code.find_source_location());
1302
1303 code_frontend_returnt new_code(code);
1304
1305 if(new_code.has_return_value())
1306 {
1307 bool result_is_used=
1308 new_code.return_value().type().id()!=ID_empty;
1309
1310 goto_programt sideeffects;
1311 clean_expr(new_code.return_value(), sideeffects, mode, result_is_used);
1312 dest.destructive_append(sideeffects);
1313
1314 // remove void-typed return value
1315 if(!result_is_used)
1316 new_code.return_value().make_nil();
1317 }
1318
1320 {
1322 new_code.has_return_value(),
1323 "function must return value",
1324 new_code.find_source_location());
1325
1326 // Now add a 'set return value' instruction to set the return value.
1328 new_code.return_value(), new_code.source_location()));
1329 }
1330 else
1331 {
1333 !new_code.has_return_value() ||
1334 new_code.return_value().type().id() == ID_empty,
1335 "function must not return value",
1336 code.find_source_location());
1337 }
1338
1339 // Need to process _entire_ destructor stack.
1340 unwind_destructor_stack(code.source_location(), dest, mode);
1341
1342 // add goto to end-of-function
1345}
1346
1348 const code_continuet &code,
1349 goto_programt &dest,
1350 const irep_idt &mode)
1351{
1354 "continue without target",
1355 code.find_source_location());
1356
1357 // need to process destructor stack
1359 code.source_location(), dest, mode, targets.continue_stack_node);
1360
1361 // add goto
1362 dest.add(
1364}
1365
1367{
1368 // this instruction will be completed during post-processing
1371
1372 // remember it to do the target later
1374}
1375
1377 const codet &code,
1378 goto_programt &dest)
1379{
1380 // this instruction will turn into OTHER during post-processing
1382 code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
1383
1384 // remember it to do this later
1385 targets.computed_gotos.push_back(t);
1386}
1387
1389 const codet &code,
1390 goto_programt &dest)
1391{
1393 code, code.source_location(), START_THREAD, nil_exprt(), {}));
1394
1395 // remember it to do target later
1396 targets.gotos.emplace_back(
1397 start_thread, targets.destructor_stack.get_current_node());
1398}
1399
1401 const codet &code,
1402 goto_programt &dest)
1403{
1405 code.operands().empty(),
1406 "end_thread expects no operands",
1407 code.find_source_location());
1408
1409 copy(code, END_THREAD, dest);
1410}
1411
1413 const codet &code,
1414 goto_programt &dest)
1415{
1417 code.operands().empty(),
1418 "atomic_begin expects no operands",
1419 code.find_source_location());
1420
1421 copy(code, ATOMIC_BEGIN, dest);
1422}
1423
1425 const codet &code,
1426 goto_programt &dest)
1427{
1429 code.operands().empty(),
1430 ": atomic_end expects no operands",
1431 code.find_source_location());
1432
1433 copy(code, ATOMIC_END, dest);
1434}
1435
1437 const code_ifthenelset &code,
1438 goto_programt &dest,
1439 const irep_idt &mode)
1440{
1441 DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
1442
1443 bool has_else=
1444 !code.else_case().is_nil();
1445
1446 const source_locationt &source_location=code.source_location();
1447
1448 // We do a bit of special treatment for && in the condition
1449 // in case cleaning would be needed otherwise.
1450 if(
1451 code.cond().id() == ID_and && code.cond().operands().size() == 2 &&
1452 (needs_cleaning(to_binary_expr(code.cond()).op0()) ||
1453 needs_cleaning(to_binary_expr(code.cond()).op1())) &&
1454 !has_else)
1455 {
1456 // if(a && b) XX --> if(a) if(b) XX
1457 code_ifthenelset new_if1(
1458 to_binary_expr(code.cond()).op1(), code.then_case());
1459 new_if1.add_source_location() = source_location;
1460 code_ifthenelset new_if0(
1461 to_binary_expr(code.cond()).op0(), std::move(new_if1));
1462 new_if0.add_source_location() = source_location;
1463 return convert_ifthenelse(new_if0, dest, mode);
1464 }
1465
1466 // convert 'then'-branch
1467 goto_programt tmp_then;
1468 convert(code.then_case(), tmp_then, mode);
1469
1470 goto_programt tmp_else;
1471
1472 if(has_else)
1473 convert(code.else_case(), tmp_else, mode);
1474
1475 exprt tmp_guard=code.cond();
1476 clean_expr(tmp_guard, dest, mode);
1477
1479 tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1480}
1481
1483 const exprt &expr,
1484 const irep_idt &id,
1485 std::list<exprt> &dest)
1486{
1487 if(expr.id()!=id)
1488 {
1489 dest.push_back(expr);
1490 }
1491 else
1492 {
1493 // left-to-right is important
1494 forall_operands(it, expr)
1495 collect_operands(*it, id, dest);
1496 }
1497}
1498
1502static inline bool is_size_one(const goto_programt &g)
1503{
1504 return (!g.instructions.empty()) &&
1505 ++g.instructions.begin()==g.instructions.end();
1506}
1507
1510 const exprt &guard,
1511 goto_programt &true_case,
1512 goto_programt &false_case,
1513 const source_locationt &source_location,
1514 goto_programt &dest,
1515 const irep_idt &mode)
1516{
1517 if(is_empty(true_case) &&
1518 is_empty(false_case))
1519 {
1520 // hmpf. Useless branch.
1521 goto_programt tmp_z;
1523 dest.add(goto_programt::make_goto(z, guard, source_location));
1524 dest.destructive_append(tmp_z);
1525 return;
1526 }
1527
1528 // do guarded assertions directly
1529 if(
1530 is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1531 true_case.instructions.back().get_condition().is_false() &&
1532 true_case.instructions.back().labels.empty())
1533 {
1534 // The above conjunction deliberately excludes the instance
1535 // if(some) { label: assert(false); }
1536 true_case.instructions.back().set_condition(boolean_negate(guard));
1537 dest.destructive_append(true_case);
1538 true_case.instructions.clear();
1539 if(
1540 is_empty(false_case) ||
1541 (is_size_one(false_case) &&
1542 is_skip(false_case, false_case.instructions.begin())))
1543 return;
1544 }
1545
1546 // similarly, do guarded assertions directly
1547 if(
1548 is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1549 false_case.instructions.back().get_condition().is_false() &&
1550 false_case.instructions.back().labels.empty())
1551 {
1552 // The above conjunction deliberately excludes the instance
1553 // if(some) ... else { label: assert(false); }
1554 false_case.instructions.back().set_condition(guard);
1555 dest.destructive_append(false_case);
1556 false_case.instructions.clear();
1557 if(
1558 is_empty(true_case) ||
1559 (is_size_one(true_case) &&
1560 is_skip(true_case, true_case.instructions.begin())))
1561 return;
1562 }
1563
1564 // a special case for C libraries that use
1565 // (void)((cond) || (assert(0),0))
1566 if(
1567 is_empty(false_case) && true_case.instructions.size() == 2 &&
1568 true_case.instructions.front().is_assert() &&
1569 true_case.instructions.front().get_condition().is_false() &&
1570 true_case.instructions.front().labels.empty() &&
1571 true_case.instructions.back().labels.empty())
1572 {
1573 true_case.instructions.front().set_condition(boolean_negate(guard));
1574 true_case.instructions.erase(--true_case.instructions.end());
1575 dest.destructive_append(true_case);
1576 true_case.instructions.clear();
1577
1578 return;
1579 }
1580
1581 // Flip around if no 'true' case code.
1582 if(is_empty(true_case))
1583 return generate_ifthenelse(
1584 boolean_negate(guard),
1585 false_case,
1586 true_case,
1587 source_location,
1588 dest,
1589 mode);
1590
1591 bool has_else=!is_empty(false_case);
1592
1593 // if(c) P;
1594 //--------------------
1595 // v: if(!c) goto z;
1596 // w: P;
1597 // z: ;
1598
1599 // if(c) P; else Q;
1600 //--------------------
1601 // v: if(!c) goto y;
1602 // w: P;
1603 // x: goto z;
1604 // y: Q;
1605 // z: ;
1606
1607 // do the x label
1608 goto_programt tmp_x;
1611
1612 // do the z label
1613 goto_programt tmp_z;
1615 // We deliberately don't set a location for 'z', it's a dummy
1616 // target.
1617
1618 // y: Q;
1619 goto_programt tmp_y;
1621 if(has_else)
1622 {
1623 tmp_y.swap(false_case);
1624 y=tmp_y.instructions.begin();
1625 }
1626
1627 // v: if(!c) goto z/y;
1628 goto_programt tmp_v;
1630 boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1631
1632 // w: P;
1633 goto_programt tmp_w;
1634 tmp_w.swap(true_case);
1635
1636 // x: goto z;
1637 CHECK_RETURN(!tmp_w.instructions.empty());
1638 x->complete_goto(z);
1639 x->source_location_nonconst() = tmp_w.instructions.back().source_location();
1640
1641 dest.destructive_append(tmp_v);
1642 dest.destructive_append(tmp_w);
1643
1644 if(has_else)
1645 {
1646 dest.destructive_append(tmp_x);
1647 dest.destructive_append(tmp_y);
1648 }
1649
1650 dest.destructive_append(tmp_z);
1651}
1652
1654static bool has_and_or(const exprt &expr)
1655{
1656 forall_operands(it, expr)
1657 if(has_and_or(*it))
1658 return true;
1659
1660 if(expr.id()==ID_and || expr.id()==ID_or)
1661 return true;
1662
1663 return false;
1664}
1665
1667 const exprt &guard,
1668 goto_programt::targett target_true,
1669 const source_locationt &source_location,
1670 goto_programt &dest,
1671 const irep_idt &mode)
1672{
1673 if(has_and_or(guard) && needs_cleaning(guard))
1674 {
1675 // if(guard) goto target;
1676 // becomes
1677 // if(guard) goto target; else goto next;
1678 // next: skip;
1679
1680 goto_programt tmp;
1681 goto_programt::targett target_false =
1682 tmp.add(goto_programt::make_skip(source_location));
1683
1685 guard, target_true, target_false, source_location, dest, mode);
1686
1687 dest.destructive_append(tmp);
1688 }
1689 else
1690 {
1691 // simple branch
1692 exprt cond=guard;
1693 clean_expr(cond, dest, mode);
1694
1695 dest.add(goto_programt::make_goto(target_true, cond, source_location));
1696 }
1697}
1698
1701 const exprt &guard,
1702 goto_programt::targett target_true,
1703 goto_programt::targett target_false,
1704 const source_locationt &source_location,
1705 goto_programt &dest,
1706 const irep_idt &mode)
1707{
1708 if(guard.id()==ID_not)
1709 {
1710 // simply swap targets
1712 to_not_expr(guard).op(),
1713 target_false,
1714 target_true,
1715 source_location,
1716 dest,
1717 mode);
1718 return;
1719 }
1720
1721 if(guard.id()==ID_and)
1722 {
1723 // turn
1724 // if(a && b) goto target_true; else goto target_false;
1725 // into
1726 // if(!a) goto target_false;
1727 // if(!b) goto target_false;
1728 // goto target_true;
1729
1730 std::list<exprt> op;
1731 collect_operands(guard, guard.id(), op);
1732
1733 for(const auto &expr : op)
1735 boolean_negate(expr), target_false, source_location, dest, mode);
1736
1737 dest.add(goto_programt::make_goto(target_true, source_location));
1738
1739 return;
1740 }
1741 else if(guard.id()==ID_or)
1742 {
1743 // turn
1744 // if(a || b) goto target_true; else goto target_false;
1745 // into
1746 // if(a) goto target_true;
1747 // if(b) goto target_true;
1748 // goto target_false;
1749
1750 std::list<exprt> op;
1751 collect_operands(guard, guard.id(), op);
1752
1753 // true branch(es)
1754 for(const auto &expr : op)
1756 expr, target_true, source_location, dest, mode);
1757
1758 // false branch
1759 dest.add(goto_programt::make_goto(target_false, guard.source_location()));
1760
1761 return;
1762 }
1763
1764 exprt cond=guard;
1765 clean_expr(cond, dest, mode);
1766
1767 // true branch
1768 dest.add(goto_programt::make_goto(target_true, cond, source_location));
1769
1770 // false branch
1771 dest.add(goto_programt::make_goto(target_false, source_location));
1772}
1773
1775 const exprt &expr,
1776 irep_idt &value)
1777{
1778 if(expr.id() == ID_typecast)
1779 return get_string_constant(to_typecast_expr(expr).op(), value);
1780
1781 if(
1782 expr.id() == ID_address_of &&
1783 to_address_of_expr(expr).object().id() == ID_index)
1784 {
1785 exprt index_op =
1786 get_constant(to_index_expr(to_address_of_expr(expr).object()).array());
1787 simplify(index_op, ns);
1788
1789 if(index_op.id()==ID_string_constant)
1790 {
1791 value = to_string_constant(index_op).get_value();
1792 return false;
1793 }
1794 else if(index_op.id()==ID_array)
1795 {
1796 std::string result;
1797 forall_operands(it, index_op)
1798 if(it->is_constant())
1799 {
1800 const auto i = numeric_cast<std::size_t>(*it);
1801 if(!i.has_value())
1802 return true;
1803
1804 if(i.value() != 0) // to skip terminating 0
1805 result += static_cast<char>(i.value());
1806 }
1807
1808 return value=result, false;
1809 }
1810 }
1811
1812 if(expr.id()==ID_string_constant)
1813 {
1814 value = to_string_constant(expr).get_value();
1815 return false;
1816 }
1817
1818 return true;
1819}
1820
1822{
1824
1825 const bool res = get_string_constant(expr, result);
1827 !res,
1828 "expected string constant",
1829 expr.find_source_location(),
1830 expr.pretty());
1831
1832 return result;
1833}
1834
1836{
1837 if(expr.id()==ID_symbol)
1838 {
1839 const symbolt &symbol=
1840 ns.lookup(to_symbol_expr(expr));
1841
1842 return symbol.value;
1843 }
1844 else if(expr.id()==ID_member)
1845 {
1846 auto tmp = to_member_expr(expr);
1847 tmp.compound() = get_constant(tmp.compound());
1848 return std::move(tmp);
1849 }
1850 else if(expr.id()==ID_index)
1851 {
1852 auto tmp = to_index_expr(expr);
1853 tmp.op0() = get_constant(tmp.op0());
1854 tmp.op1() = get_constant(tmp.op1());
1855 return std::move(tmp);
1856 }
1857 else
1858 return expr;
1859}
1860
1862 const typet &type,
1863 const std::string &suffix,
1864 goto_programt &dest,
1865 const source_locationt &source_location,
1866 const irep_idt &mode)
1867{
1868 PRECONDITION(!mode.empty());
1869 symbolt &new_symbol = get_fresh_aux_symbol(
1870 type,
1872 "tmp_" + suffix,
1873 source_location,
1874 mode,
1875 symbol_table);
1876
1877 code_frontend_declt decl(new_symbol.symbol_expr());
1878 decl.add_source_location()=source_location;
1879 convert_frontend_decl(decl, dest, mode);
1880
1881 return new_symbol;
1882}
1883
1885 exprt &expr,
1886 const std::string &suffix,
1887 goto_programt &dest,
1888 const irep_idt &mode)
1889{
1890 const source_locationt source_location=expr.find_source_location();
1891
1892 symbolt &new_symbol =
1893 new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
1894
1895 code_assignt assignment;
1896 assignment.lhs()=new_symbol.symbol_expr();
1897 assignment.rhs()=expr;
1898 assignment.add_source_location()=source_location;
1899
1900 convert(assignment, dest, mode);
1901
1902 expr=new_symbol.symbol_expr();
1903}
1904
1906 const codet &code,
1907 symbol_table_baset &symbol_table,
1908 goto_programt &dest,
1909 message_handlert &message_handler,
1910 const irep_idt &mode)
1911{
1912 symbol_table_buildert symbol_table_builder =
1913 symbol_table_buildert::wrap(symbol_table);
1914 goto_convertt goto_convert(symbol_table_builder, message_handler);
1915 goto_convert.goto_convert(code, dest, mode);
1916}
1917
1919 symbol_table_baset &symbol_table,
1920 goto_programt &dest,
1921 message_handlert &message_handler)
1922{
1923 // find main symbol
1924 const symbol_tablet::symbolst::const_iterator s_it=
1925 symbol_table.symbols.find("main");
1926
1928 s_it != symbol_table.symbols.end(), "failed to find main symbol");
1929
1930 const symbolt &symbol=s_it->second;
1931
1933 to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
1934}
1935
1951 const code_blockt &thread_body,
1952 goto_programt &dest,
1953 const irep_idt &mode)
1954{
1955 goto_programt preamble, body, postamble;
1956
1958 convert(thread_body, body, mode);
1959
1961 static_cast<const codet &>(get_nil_irep()),
1962 thread_body.source_location(),
1963 END_THREAD,
1964 nil_exprt(),
1965 {}));
1966 e->source_location_nonconst() = thread_body.source_location();
1968
1970 static_cast<const codet &>(get_nil_irep()),
1971 thread_body.source_location(),
1973 nil_exprt(),
1974 {c}));
1975 preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
1976
1977 dest.destructive_append(preamble);
1978 dest.destructive_append(body);
1979 dest.destructive_append(postamble);
1980}
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Operator to return the address of an object.
Definition: pointer_expr.h:361
Result of an attempt to find ancestor information about two nodes.
std::size_t right_depth_below_common_ancestor
node_indext common_ancestor
Boolean AND.
Definition: std_expr.h:1974
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
The Boolean type.
Definition: std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:270
const exprt & assertion() const
Definition: std_code.h:276
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition: std_code.h:217
const exprt & assumption() const
Definition: std_code.h:223
A codet representing sequential composition of program statements.
Definition: std_code.h:130
code_operandst & statements()
Definition: std_code.h:138
source_locationt end_location() const
Definition: std_code.h:187
void add(const codet &code)
Definition: std_code.h:168
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1182
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1218
A codet representing the removal of a local variable going out of scope.
codet representation of a do while statement.
Definition: std_code.h:672
const codet & body() const
Definition: std_code.h:689
const exprt & cond() const
Definition: std_code.h:679
codet representation of an expression statement.
Definition: std_code.h:1394
const exprt & expression() const
Definition: std_code.h:1401
codet representation of a for statement.
Definition: std_code.h:734
const exprt & cond() const
Definition: std_code.h:759
const exprt & iter() const
Definition: std_code.h:769
const codet & body() const
Definition: std_code.h:779
const exprt & init() const
Definition: std_code.h:749
A codet representing the declaration of a local variable.
Definition: std_code.h:347
const irep_idt & get_identifier() const
Definition: std_code.h:364
codet representation of a "return from a function" statement.
Definition: std_code.h:893
const exprt & return_value() const
Definition: std_code.h:903
bool has_return_value() const
Definition: std_code.h:913
codet representation of a function call statement.
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1097
const exprt & upper() const
upper bound of range
Definition: std_code.h:1119
const exprt & lower() const
lower bound of range
Definition: std_code.h:1107
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1131
codet representation of a goto statement.
Definition: std_code.h:841
codet representation of an if-then-else statement.
Definition: std_code.h:460
const exprt & cond() const
Definition: std_code.h:478
const codet & else_case() const
Definition: std_code.h:498
const codet & then_case() const
Definition: std_code.h:488
codet representation of a label for branch targets.
Definition: std_code.h:959
const irep_idt & get_label() const
Definition: std_code.h:967
exception_listt & exception_list()
Definition: std_code.h:1860
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1849
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1023
const exprt & case_op() const
Definition: std_code.h:1040
codet & code()
Definition: std_code.h:1050
bool is_default() const
Definition: std_code.h:1030
codet representing a switch statement.
Definition: std_code.h:548
const codet & body() const
Definition: std_code.h:565
const exprt & value() const
Definition: std_code.h:555
const parameterst & parameters() const
Definition: std_types.h:655
codet representing a while statement.
Definition: std_code.h:610
const exprt & cond() const
Definition: std_code.h:617
const codet & body() const
Definition: std_code.h:627
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Operator to dereference a pointer.
Definition: pointer_expr.h:648
void set_current_node(optionalt< node_indext > val)
Sets the current node.
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
void optimize_guarded_gotos(goto_programt &dest)
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a bra...
void convert_atomic_begin(const codet &code, goto_programt &dest)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_switch_case_range(const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
irep_idt get_string_constant(const exprt &expr)
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
exprt get_constant(const exprt &expr)
void convert_start_thread(const codet &code, goto_programt &dest)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) goto target_true; else goto target_false;
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
void convert_atomic_end(const codet &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
struct goto_convertt::targetst targets
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
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 convert_goto(const code_gotot &code, goto_programt &dest)
exprt case_guard(const exprt &value, const caset &case_op)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
void convert_decl_type(const codet &code, goto_programt &dest)
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
void convert_loop_contracts(const codet &code, goto_programt::targett loop, const irep_idt &mode)
void convert_skip(const codet &code, goto_programt &dest)
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
void finish_computed_gotos(goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
exprt::operandst caset
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
static void replace_new_object(const exprt &object, exprt &dest)
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
void convert_return(const code_frontend_returnt &, goto_programt &dest, const irep_idt &mode)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
void generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
Generates the necessary goto-instructions to represent a thread-block.
void convert_end_thread(const codet &code, goto_programt &dest)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
void complete_goto(targett _target)
Definition: goto_program.h:463
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
targetst targets
The list of successor instructions.
Definition: goto_program.h:403
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:534
const source_locationt & source_location() const
Definition: goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:863
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:706
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:803
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:890
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:788
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:996
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
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
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
mstreamt & debug() const
Definition: message.h:429
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
void set_case_number(const irep_idt &number)
const irep_idt & get_value() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:18
Destructor Calls.
std::size_t node_indext
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
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.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
static bool has_and_or(const exprt &expr)
if(guard) goto target;
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
static void finish_catch_push_targets(goto_programt &dest)
Populate the CATCH instructions with the targets corresponding to their associated labels.
static bool is_empty(const goto_programt &goto_program)
Program Transformation.
Program Transformation.
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:32
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ ASSIGN
Definition: goto_program.h:46
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
const irept & get_nil_irep()
Definition: irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
bool is_skip(const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
Determine whether the instruction is semantically equivalent to a skip (no-op).
Definition: remove_skip.cpp:27
Program Transformation.
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#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_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1203
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1077
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:875
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:304
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1883
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition: std_code.h:943
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:716
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:251
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:654
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1004
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:530
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1161
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1282
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:823
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:592
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition: std_code.h:429
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1239
const codet & to_code(const exprt &expr)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
computed_gotost computed_gotos
goto_programt::targett continue_target
void set_break(goto_programt::targett _break_target)
destructor_treet destructor_stack
goto_programt::targett default_target
goto_programt::targett return_target
void set_default(goto_programt::targett _default_target)
void set_continue(goto_programt::targett _continue_target)
goto_programt::targett break_target
Author: Diffblue Ltd.