cprover
Loading...
Searching...
No Matches
goto_convert_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
13#define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
14
15#include <list>
16#include <vector>
17#include <unordered_set>
18
19#include <util/message.h>
20#include <util/namespace.h>
21#include <util/replace_expr.h>
22#include <util/std_code.h>
23
24#include "allocate_objects.h"
25#include "destructor_tree.h"
26#include "goto_program.h"
27
29
31{
32public:
33 void
34 goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
35
45
47 {
48 }
49
50protected:
53 std::string tmp_symbol_prefix;
55
57 const codet &code,
59 const irep_idt &mode);
60
61 //
62 // tools for symbols
63 //
65 const typet &type,
66 const std::string &suffix,
68 const source_locationt &,
69 const irep_idt &mode);
70
72 const exprt &expr,
74 const irep_idt &mode);
75
76 //
77 // translation of C expressions (with side effects)
78 // into the program logic
79 //
80
81 void clean_expr(
82 exprt &expr,
84 const irep_idt &mode,
85 bool result_is_used = true);
86
87 void
89
90 static bool needs_cleaning(const exprt &expr);
91
93 exprt &expr,
94 const std::string &suffix,
96 const irep_idt &mode);
97
99
100 static bool has_function_call(const exprt &expr);
101
103 side_effect_exprt &expr,
105 const irep_idt &mode,
106 bool result_is_used,
107 bool address_taken);
109 side_effect_exprt &expr,
111 bool result_is_used,
112 bool address_taken,
113 const irep_idt &mode);
114 void remove_pre(
115 side_effect_exprt &expr,
117 bool result_is_used,
118 bool address_taken,
119 const irep_idt &mode);
120 void remove_post(
121 side_effect_exprt &expr,
123 const irep_idt &mode,
124 bool result_is_used);
128 const irep_idt &mode,
129 bool result_is_used);
130 void remove_cpp_new(
131 side_effect_exprt &expr,
133 bool result_is_used);
135 side_effect_exprt &expr,
137 void remove_malloc(
138 side_effect_exprt &expr,
140 const irep_idt &mode,
141 bool result_is_used);
143 side_effect_exprt &expr,
146 side_effect_exprt &expr,
148 const irep_idt &mode,
149 bool result_is_used);
151 exprt &expr,
153 const irep_idt &mode);
154 void remove_overflow(
157 bool result_is_used,
158 const irep_idt &mode);
159
160 virtual void do_cpp_new(
161 const exprt &lhs,
162 const side_effect_exprt &rhs,
164
166 const exprt &lhs,
167 const side_effect_exprt &rhs,
169
171 const exprt &lhs,
172 const side_effect_exprt &rhs,
174
175 static void replace_new_object(
176 const exprt &object,
177 exprt &dest);
178
180 const exprt &lhs,
181 const side_effect_exprt &rhs,
183
184 //
185 // function calls
186 //
187
188 virtual void do_function_call(
189 const exprt &lhs,
190 const exprt &function,
191 const exprt::operandst &arguments,
193 const irep_idt &mode);
194
195 virtual void do_function_call_if(
196 const exprt &lhs,
197 const if_exprt &function,
198 const exprt::operandst &arguments,
200 const irep_idt &mode);
201
202 virtual void do_function_call_symbol(
203 const exprt &lhs,
204 const symbol_exprt &function,
205 const exprt::operandst &arguments,
207 const irep_idt &mode);
208
209 virtual void do_function_call_symbol(const symbolt &)
210 {
211 }
212
213 virtual void do_function_call_other(
214 const exprt &lhs,
215 const exprt &function,
216 const exprt::operandst &arguments,
218
219 //
220 // conversion
221 //
222 void convert_block(
223 const code_blockt &code,
225 const irep_idt &mode);
227 const code_frontend_declt &,
229 const irep_idt &mode);
230 void convert_decl_type(const codet &code, goto_programt &dest);
232 const code_expressiont &code,
234 const irep_idt &mode);
235 void convert_assign(
236 const code_assignt &code,
238 const irep_idt &mode);
239 void convert_cpp_delete(const codet &code, goto_programt &dest);
241 const codet &code,
243 const irep_idt &mode);
244 void
245 convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
246 void convert_while(
247 const code_whilet &code,
249 const irep_idt &mode);
250 void convert_dowhile(
251 const code_dowhilet &code,
253 const irep_idt &mode);
254 void convert_assume(
255 const code_assumet &code,
257 const irep_idt &mode);
258 void convert_assert(
259 const code_assertt &code,
261 const irep_idt &mode);
262 void convert_switch(
263 const code_switcht &code,
265 const irep_idt &mode);
266 void convert_break(
267 const code_breakt &code,
269 const irep_idt &mode);
270 void convert_return(
271 const code_frontend_returnt &,
273 const irep_idt &mode);
274 void convert_continue(
275 const code_continuet &code,
277 const irep_idt &mode);
279 const code_ifthenelset &code,
281 const irep_idt &mode);
282 void convert_goto(const code_gotot &code, goto_programt &dest);
284 void convert_skip(const codet &code, goto_programt &dest);
285 void convert_label(
286 const code_labelt &code,
288 const irep_idt &mode);
291 const code_switch_caset &code,
293 const irep_idt &mode);
297 const irep_idt &mode);
299 const code_function_callt &code,
301 const irep_idt &mode);
302 void convert_start_thread(const codet &code, goto_programt &dest);
303 void convert_end_thread(const codet &code, goto_programt &dest);
304 void convert_atomic_begin(const codet &code, goto_programt &dest);
305 void convert_atomic_end(const codet &code, goto_programt &dest);
307 const codet &code,
309 const irep_idt &mode);
311 const codet &code,
313 const irep_idt &mode);
315 const codet &code,
317 const irep_idt &mode);
319 const codet &code,
321 const irep_idt &mode);
323 const codet &code,
325 const irep_idt &mode);
327 const codet &code,
329 const irep_idt &mode);
331 const codet &code,
333 const irep_idt &mode);
334 void convert_asm(const code_asmt &code, goto_programt &dest);
335
336 void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
337
338 void copy(
339 const codet &code,
342
343 //
344 // exceptions
345 //
346
348
350 const source_locationt &source_location,
352 const irep_idt &mode,
355
356 //
357 // gotos
358 //
359
360 void finish_gotos(goto_programt &dest, const irep_idt &mode);
363
364 typedef std::map<irep_idt,
365 std::pair<goto_programt::targett, node_indext>>
367 typedef std::list<std::pair<goto_programt::targett, node_indext>>
369 typedef std::list<goto_programt::targett> computed_gotost;
371 typedef std::list<std::pair<goto_programt::targett, caset> > casest;
372 typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
373
374 struct targetst
375 {
378
383
386
389
392
407
414
421
427
433
440
448
450 {
451 // for 'while', 'for', 'dowhile'
452
454 {
455 break_set=targets.break_set;
456 continue_set=targets.continue_set;
457 break_target=targets.break_target;
458 continue_target=targets.continue_target;
459 }
460
462 {
463 targets.break_set=break_set;
464 targets.continue_set=continue_set;
465 targets.break_target=break_target;
466 targets.continue_target=continue_target;
467 }
468
472 };
473
475 {
476 // for 'switch'
477
479 {
480 break_set=targets.break_set;
481 default_set=targets.default_set;
482 break_target=targets.break_target;
483 default_target=targets.default_target;
484 break_stack_node=targets.destructor_stack.get_current_node();
485 cases=targets.cases;
486 cases_map=targets.cases_map;
487 }
488
490 {
491 targets.break_set=break_set;
492 targets.default_set=default_set;
493 targets.break_target=break_target;
494 targets.default_target=default_target;
495 targets.cases=cases;
496 targets.cases_map=cases_map;
497 }
498
503
506 };
507
509 {
510 // for 'try...catch' and the like
511
513 {
514 throw_set=targets.throw_set;
515 throw_target=targets.throw_target;
516 throw_stack_node=targets.destructor_stack.get_current_node();
517 }
518
520 {
521 targets.throw_set=throw_set;
522 targets.throw_target=throw_target;
523 }
524
528 };
529
531 {
532 // for 'try...leave...finally'
533
535 {
536 leave_set=targets.leave_set;
537 leave_target=targets.leave_target;
538 leave_stack_node=targets.destructor_stack.get_current_node();
539 }
540
542 {
543 targets.leave_set=leave_set;
544 targets.leave_target=leave_target;
545 }
546
550 };
551
553 const exprt &value,
554 const caset &case_op);
555
556 // if(cond) { true_case } else { false_case }
558 const exprt &cond,
559 goto_programt &true_case,
560 goto_programt &false_case,
561 const source_locationt &,
563 const irep_idt &mode);
564
565 // if(guard) goto target_true; else goto target_false;
567 const exprt &guard,
570 const source_locationt &,
572 const irep_idt &mode);
573
574 // if(guard) goto target;
576 const exprt &guard,
578 const source_locationt &,
580 const irep_idt &mode);
581
582 // turn a OP b OP c into a list a, b, c
583 static void collect_operands(
584 const exprt &expr,
585 const irep_idt &id,
586 std::list<exprt> &dest);
587
588 // START_THREAD; ... END_THREAD;
592 const irep_idt &mode);
593
594 //
595 // misc
596 //
598 bool get_string_constant(const exprt &expr, irep_idt &);
599 exprt get_constant(const exprt &expr);
600
616 const exprt &lhs,
617 const symbol_exprt &function,
618 const exprt::operandst &arguments,
620
621 // some built-in functions
622 void do_atomic_begin(
623 const exprt &lhs,
624 const symbol_exprt &function,
625 const exprt::operandst &arguments,
627 void do_atomic_end(
628 const exprt &lhs,
629 const symbol_exprt &function,
630 const exprt::operandst &arguments,
633 const exprt &lhs,
634 const symbol_exprt &function,
635 const exprt::operandst &arguments,
638 const exprt &lhs,
639 const symbol_exprt &rhs,
640 const exprt::operandst &arguments,
642 void do_array_op(
643 const irep_idt &id,
644 const exprt &lhs,
645 const symbol_exprt &function,
646 const exprt::operandst &arguments,
648 void do_printf(
649 const exprt &lhs,
650 const symbol_exprt &function,
651 const exprt::operandst &arguments,
653 void do_scanf(
654 const exprt &lhs,
655 const symbol_exprt &function,
656 const exprt::operandst &arguments,
658 void do_input(
659 const exprt &rhs,
660 const exprt::operandst &arguments,
662 void do_output(
663 const exprt &rhs,
664 const exprt::operandst &arguments,
666 void do_prob_coin(
667 const exprt &lhs,
668 const symbol_exprt &function,
669 const exprt::operandst &arguments,
671 void do_prob_uniform(
672 const exprt &lhs,
673 const symbol_exprt &function,
674 const exprt::operandst &arguments,
676 void do_havoc_slice(
677 const exprt &lhs,
678 const symbol_exprt &function,
679 const exprt::operandst &arguments,
681 const irep_idt &mode);
682
683 exprt get_array_argument(const exprt &src);
684};
685
686#endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
lifetimet
Selects the kind of objects allocated.
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
codet representation of an inline assembler statement.
Definition std_code.h:1253
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing sequential composition of program statements.
Definition std_code.h:130
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
codet representation of a do while statement.
Definition std_code.h:672
codet representation of an expression statement.
Definition std_code.h:1394
codet representation of a for statement.
Definition std_code.h:734
A codet representing the declaration of a local variable.
Definition std_code.h:347
codet representation of a "return from a function" statement.
Definition std_code.h:893
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
codet representation of a goto statement.
Definition std_code.h:841
codet representation of an if-then-else statement.
Definition std_code.h:460
codet representation of a label for branch targets.
Definition std_code.h:959
codet representation of a switch-case, i.e. a case statement within a switch.
Definition std_code.h:1023
codet representing a switch statement.
Definition std_code.h:548
codet representing a while statement.
Definition std_code.h:610
Data structure for representing an arbitrary statement in a program.
Tree to keep track of the destructors generated along each branch of a function.
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
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
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)
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)
void do_havoc_slice(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
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)
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
void goto_convert(const codet &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 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 remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void convert_start_thread(const codet &code, goto_programt &dest)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
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 do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert_atomic_end(const codet &code, goto_programt &dest)
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 convert_gcc_local_label(const codet &code, goto_programt &dest)
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
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 do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert_goto(const code_gotot &code, goto_programt &dest)
symbol_exprt exception_flag(const irep_idt &mode)
void do_enum_is_in_range(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Converts calls to the built in enum_is_in_range function to a test that the given enum value is in th...
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 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 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 do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
void convert_decl_type(const codet &code, goto_programt &dest)
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
add function calls to function queue for later processing
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)
std::map< goto_programt::targett, casest::iterator > cases_mapt
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 do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
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 cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
goto_convertt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
std::map< irep_idt, std::pair< goto_programt::targett, node_indext > > labelst
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
static bool has_function_call(const exprt &expr)
exprt get_array_argument(const exprt &src)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call_symbol(const symbolt &)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void finish_computed_gotos(goto_programt &dest)
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void do_create_thread(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
virtual ~goto_convertt()
std::list< std::pair< goto_programt::targett, node_indext > > gotost
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;
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void do_array_equal(const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest, const irep_idt &mode)
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)
std::list< goto_programt::targett > computed_gotost
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 rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::list< std::pair< goto_programt::targett, caset > > casest
void convert_end_thread(const codet &code, goto_programt &dest)
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
The trinary if-then-else operator.
Definition std_expr.h:2226
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition c_expr.h:117
An expression containing a side effect.
Definition std_code.h:1450
Expression to hold a symbol (variable)
Definition std_expr.h:80
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
std::size_t node_indext
Concrete Goto Program.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
dstringt irep_idt
Definition irep.h:37
break_continue_targetst(const targetst &targets)
break_switch_targetst(const targetst &targets)
void restore(targetst &targets)
leave_targett(const targetst &targets)
goto_programt::targett leave_target
goto_programt::targett continue_target
void set_leave(goto_programt::targett _leave_target)
void set_return(goto_programt::targett _return_target)
void set_break(goto_programt::targett _break_target)
destructor_treet destructor_stack
goto_programt::targett default_target
goto_programt::targett return_target
goto_programt::targett leave_target
void set_throw(goto_programt::targett _throw_target)
void set_default(goto_programt::targett _default_target)
void set_continue(goto_programt::targett _continue_target)
goto_programt::targett throw_target
goto_programt::targett break_target
goto_programt::targett throw_target
throw_targett(const targetst &targets)
void restore(targetst &targets)