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,
58 goto_programt &dest,
59 const irep_idt &mode);
60
61 //
62 // tools for symbols
63 //
65 const typet &type,
66 const std::string &suffix,
67 goto_programt &dest,
68 const source_locationt &,
69 const irep_idt &mode);
70
72 const exprt &expr,
73 goto_programt &dest,
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,
83 goto_programt &dest,
84 const irep_idt &mode,
85 bool result_is_used = true);
86
87 void
88 clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode);
89
90 static bool needs_cleaning(const exprt &expr);
91
92 // Do we need to introduce a temporary for the value of an assignment
93 // to the given lhs? E.g., a[i] needs a temporary as its value may change
94 // when i is changed; likewise, *p needs a temporary as its value may change
95 // when p is changed.
96 static bool assignment_lhs_needs_temporary(const exprt &lhs)
97 {
98 return lhs.id() != ID_symbol;
99 }
100
101 void make_temp_symbol(
102 exprt &expr,
103 const std::string &suffix,
105 const irep_idt &mode);
106
107 void rewrite_boolean(exprt &dest);
108
109 static bool has_function_call(const exprt &expr);
110
112 side_effect_exprt &expr,
113 goto_programt &dest,
114 const irep_idt &mode,
115 bool result_is_used,
116 bool address_taken);
118 side_effect_exprt &expr,
119 goto_programt &dest,
120 bool result_is_used,
121 bool address_taken,
122 const irep_idt &mode);
123 void remove_pre(
124 side_effect_exprt &expr,
125 goto_programt &dest,
126 bool result_is_used,
127 bool address_taken,
128 const irep_idt &mode);
129 void remove_post(
130 side_effect_exprt &expr,
131 goto_programt &dest,
132 const irep_idt &mode,
133 bool result_is_used);
136 goto_programt &dest,
137 const irep_idt &mode,
138 bool result_is_used);
139 void remove_cpp_new(
140 side_effect_exprt &expr,
141 goto_programt &dest,
142 bool result_is_used);
144 side_effect_exprt &expr,
145 goto_programt &dest);
146 void remove_malloc(
147 side_effect_exprt &expr,
148 goto_programt &dest,
149 const irep_idt &mode,
150 bool result_is_used);
152 side_effect_exprt &expr,
153 goto_programt &dest);
155 side_effect_exprt &expr,
156 goto_programt &dest,
157 const irep_idt &mode,
158 bool result_is_used);
160 exprt &expr,
161 goto_programt &dest,
162 const irep_idt &mode);
163 void remove_overflow(
165 goto_programt &dest,
166 bool result_is_used,
167 const irep_idt &mode);
168
169 virtual void do_cpp_new(
170 const exprt &lhs,
171 const side_effect_exprt &rhs,
172 goto_programt &dest);
173
175 const exprt &lhs,
176 const side_effect_exprt &rhs,
177 goto_programt &dest);
178
180 const exprt &lhs,
181 const side_effect_exprt &rhs,
182 goto_programt &dest);
183
184 static void replace_new_object(
185 const exprt &object,
186 exprt &dest);
187
189 const exprt &lhs,
190 const side_effect_exprt &rhs,
191 goto_programt &dest);
192
193 //
194 // function calls
195 //
196
197 virtual void do_function_call(
198 const exprt &lhs,
199 const exprt &function,
200 const exprt::operandst &arguments,
201 goto_programt &dest,
202 const irep_idt &mode);
203
204 virtual void do_function_call_if(
205 const exprt &lhs,
206 const if_exprt &function,
207 const exprt::operandst &arguments,
208 goto_programt &dest,
209 const irep_idt &mode);
210
211 virtual void do_function_call_symbol(
212 const exprt &lhs,
213 const symbol_exprt &function,
214 const exprt::operandst &arguments,
215 goto_programt &dest,
216 const irep_idt &mode);
217
218 virtual void do_function_call_symbol(const symbolt &)
219 {
220 }
221
222 virtual void do_function_call_other(
223 const exprt &lhs,
224 const exprt &function,
225 const exprt::operandst &arguments,
226 goto_programt &dest);
227
228 //
229 // conversion
230 //
231 void convert_block(
232 const code_blockt &code,
233 goto_programt &dest,
234 const irep_idt &mode);
236 const code_frontend_declt &,
238 const irep_idt &mode);
239 void convert_decl_type(const codet &code, goto_programt &dest);
241 const code_expressiont &code,
242 goto_programt &dest,
243 const irep_idt &mode);
244 void convert_assign(
245 const code_assignt &code,
246 goto_programt &dest,
247 const irep_idt &mode);
248 void convert_cpp_delete(const codet &code, goto_programt &dest);
250 const codet &code,
252 const irep_idt &mode);
253 void
254 convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
255 void convert_while(
256 const code_whilet &code,
257 goto_programt &dest,
258 const irep_idt &mode);
259 void convert_dowhile(
260 const code_dowhilet &code,
261 goto_programt &dest,
262 const irep_idt &mode);
263 void convert_assume(
264 const code_assumet &code,
265 goto_programt &dest,
266 const irep_idt &mode);
267 void convert_assert(
268 const code_assertt &code,
269 goto_programt &dest,
270 const irep_idt &mode);
271 void convert_switch(
272 const code_switcht &code,
273 goto_programt &dest,
274 const irep_idt &mode);
275 void convert_break(
276 const code_breakt &code,
277 goto_programt &dest,
278 const irep_idt &mode);
279 void convert_return(
280 const code_frontend_returnt &,
281 goto_programt &dest,
282 const irep_idt &mode);
283 void convert_continue(
284 const code_continuet &code,
285 goto_programt &dest,
286 const irep_idt &mode);
288 const code_ifthenelset &code,
289 goto_programt &dest,
290 const irep_idt &mode);
291 void convert_goto(const code_gotot &code, goto_programt &dest);
292 void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
293 void convert_skip(const codet &code, goto_programt &dest);
294 void convert_label(
295 const code_labelt &code,
296 goto_programt &dest,
297 const irep_idt &mode);
298 void convert_gcc_local_label(const codet &code, goto_programt &dest);
300 const code_switch_caset &code,
301 goto_programt &dest,
302 const irep_idt &mode);
305 goto_programt &dest,
306 const irep_idt &mode);
308 const code_function_callt &code,
309 goto_programt &dest,
310 const irep_idt &mode);
311 void convert_start_thread(const codet &code, goto_programt &dest);
312 void convert_end_thread(const codet &code, goto_programt &dest);
313 void convert_atomic_begin(const codet &code, goto_programt &dest);
314 void convert_atomic_end(const codet &code, goto_programt &dest);
316 const codet &code,
317 goto_programt &dest,
318 const irep_idt &mode);
320 const codet &code,
321 goto_programt &dest,
322 const irep_idt &mode);
324 const codet &code,
325 goto_programt &dest,
326 const irep_idt &mode);
328 const codet &code,
329 goto_programt &dest,
330 const irep_idt &mode);
332 const codet &code,
333 goto_programt &dest,
334 const irep_idt &mode);
336 const codet &code,
337 goto_programt &dest,
338 const irep_idt &mode);
340 const codet &code,
341 goto_programt &dest,
342 const irep_idt &mode);
343 void convert_asm(const code_asmt &code, goto_programt &dest);
344
345 void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
346
347 void copy(
348 const codet &code,
350 goto_programt &dest);
351
352 //
353 // exceptions
354 //
355
357
359 const source_locationt &source_location,
360 goto_programt &dest,
361 const irep_idt &mode,
364
365 //
366 // gotos
367 //
368
369 void finish_gotos(goto_programt &dest, const irep_idt &mode);
372
373 typedef std::map<irep_idt,
374 std::pair<goto_programt::targett, node_indext>>
376 typedef std::list<std::pair<goto_programt::targett, node_indext>>
378 typedef std::list<goto_programt::targett> computed_gotost;
380 typedef std::list<std::pair<goto_programt::targett, caset> > casest;
381 typedef std::map<
383 casest::iterator,
386
387 struct targetst
388 {
391
394
399
402
405
408
423
430
437
443
449
456
464
466 {
467 // for 'while', 'for', 'dowhile'
468
470 {
471 break_set=targets.break_set;
472 continue_set=targets.continue_set;
473 break_target=targets.break_target;
474 continue_target=targets.continue_target;
475 }
476
478 {
479 targets.break_set=break_set;
480 targets.continue_set=continue_set;
481 targets.break_target=break_target;
482 targets.continue_target=continue_target;
483 }
484
488 };
489
491 {
492 // for 'switch'
493
495 {
496 break_set=targets.break_set;
497 default_set=targets.default_set;
498 break_target=targets.break_target;
499 default_target=targets.default_target;
500 break_stack_node=targets.destructor_stack.get_current_node();
501 cases=targets.cases;
502 cases_map=targets.cases_map;
503 }
504
506 {
507 targets.break_set=break_set;
508 targets.default_set=default_set;
509 targets.break_target=break_target;
510 targets.default_target=default_target;
511 targets.cases=cases;
512 targets.cases_map=cases_map;
513 }
514
519
522 };
523
525 {
526 // for 'try...catch' and the like
527
529 {
530 throw_set=targets.throw_set;
531 throw_target=targets.throw_target;
532 throw_stack_node=targets.destructor_stack.get_current_node();
533 }
534
536 {
537 targets.throw_set=throw_set;
538 targets.throw_target=throw_target;
539 }
540
544 };
545
547 {
548 // for 'try...leave...finally'
549
551 {
552 leave_set=targets.leave_set;
553 leave_target=targets.leave_target;
554 leave_stack_node=targets.destructor_stack.get_current_node();
555 }
556
558 {
559 targets.leave_set=leave_set;
560 targets.leave_target=leave_target;
561 }
562
566 };
567
569 const exprt &value,
570 const caset &case_op);
571
572 // if(cond) { true_case } else { false_case }
574 const exprt &cond,
575 goto_programt &true_case,
576 goto_programt &false_case,
577 const source_locationt &,
578 goto_programt &dest,
579 const irep_idt &mode);
580
581 // if(guard) goto target_true; else goto target_false;
583 const exprt &guard,
586 const source_locationt &,
587 goto_programt &dest,
588 const irep_idt &mode);
589
590 // if(guard) goto target;
592 const exprt &guard,
594 const source_locationt &,
595 goto_programt &dest,
596 const irep_idt &mode);
597
598 // turn a OP b OP c into a list a, b, c
599 static void collect_operands(
600 const exprt &expr,
601 const irep_idt &id,
602 std::list<exprt> &dest);
603
604 // START_THREAD; ... END_THREAD;
607 goto_programt &dest,
608 const irep_idt &mode);
609
610 //
611 // misc
612 //
614 bool get_string_constant(const exprt &expr, irep_idt &);
615 exprt get_constant(const exprt &expr);
616
617 // some built-in functions
618 void do_atomic_begin(
619 const exprt &lhs,
620 const symbol_exprt &function,
621 const exprt::operandst &arguments,
622 goto_programt &dest);
623 void do_atomic_end(
624 const exprt &lhs,
625 const symbol_exprt &function,
626 const exprt::operandst &arguments,
627 goto_programt &dest);
629 const exprt &lhs,
630 const symbol_exprt &function,
631 const exprt::operandst &arguments,
632 goto_programt &dest);
634 const exprt &lhs,
635 const symbol_exprt &rhs,
636 const exprt::operandst &arguments,
637 goto_programt &dest);
638 void do_array_op(
639 const irep_idt &id,
640 const exprt &lhs,
641 const symbol_exprt &function,
642 const exprt::operandst &arguments,
643 goto_programt &dest);
644 void do_printf(
645 const exprt &lhs,
646 const symbol_exprt &function,
647 const exprt::operandst &arguments,
648 goto_programt &dest);
649 void do_scanf(
650 const exprt &lhs,
651 const symbol_exprt &function,
652 const exprt::operandst &arguments,
653 goto_programt &dest);
654 void do_input(
655 const exprt &rhs,
656 const exprt::operandst &arguments,
657 goto_programt &dest);
658 void do_output(
659 const exprt &rhs,
660 const exprt::operandst &arguments,
661 goto_programt &dest);
662 void do_prob_coin(
663 const exprt &lhs,
664 const symbol_exprt &function,
665 const exprt::operandst &arguments,
666 goto_programt &dest);
667 void do_prob_uniform(
668 const exprt &lhs,
669 const symbol_exprt &function,
670 const exprt::operandst &arguments,
671 goto_programt &dest);
672 void do_havoc_slice(
673 const exprt &lhs,
674 const symbol_exprt &function,
675 const exprt::operandst &arguments,
676 goto_programt &dest,
677 const irep_idt &mode);
678 void do_alloca(
679 const exprt &lhs,
680 const symbol_exprt &function,
681 const exprt::operandst &arguments,
682 goto_programt &dest,
683 const irep_idt &mode);
684
685 exprt get_array_argument(const exprt &src);
686};
687
688#endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
lifetimet
Selects the kind of objects allocated.
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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 goto_instruction_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
goto_instruction_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:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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)
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)
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)
Returns 'true' for expressions that may change the program state.
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)
void do_alloca(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
alloca allocates memory that is freed when leaving the function (and not the block,...
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.
std::map< goto_programt::targett, casest::iterator, goto_programt::target_less_than > cases_mapt
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)
static bool assignment_lhs_needs_temporary(const exprt &lhs)
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:2323
const irep_idt & id() const
Definition irep.h:396
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:113
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.
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)
A total order over targett and const_targett.
dstringt irep_idt