cprover
goto_convert_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #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/allocate_objects.h>
20 #include <util/message.h>
21 #include <util/namespace.h>
22 #include <util/replace_expr.h>
23 #include <util/std_code.h>
24 
25 #include "goto_program.h"
26 #include "destructor_tree.h"
27 
29 
30 class goto_convertt:public messaget
31 {
32 public:
33  void
34  goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
35 
37  symbol_table_baset &_symbol_table,
38  message_handlert &_message_handler):
39  messaget(_message_handler),
40  symbol_table(_symbol_table),
41  ns(_symbol_table),
42  tmp_symbol_prefix("goto_convertt")
43  {
44  }
45 
46  virtual ~goto_convertt()
47  {
48  }
49 
50 protected:
53  std::string tmp_symbol_prefix;
55 
56  void goto_convert_rec(
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  void make_temp_symbol(
93  exprt &expr,
94  const std::string &suffix,
95  goto_programt &,
96  const irep_idt &mode);
97 
98  void rewrite_boolean(exprt &dest);
99 
100  static bool has_function_call(const exprt &expr);
101 
102  void remove_side_effect(
103  side_effect_exprt &expr,
104  goto_programt &dest,
105  const irep_idt &mode,
106  bool result_is_used,
107  bool address_taken);
108  void remove_assignment(
109  side_effect_exprt &expr,
110  goto_programt &dest,
111  bool result_is_used,
112  bool address_taken,
113  const irep_idt &mode);
114  void remove_pre(
115  side_effect_exprt &expr,
116  goto_programt &dest,
117  bool result_is_used,
118  bool address_taken,
119  const irep_idt &mode);
120  void remove_post(
121  side_effect_exprt &expr,
122  goto_programt &dest,
123  const irep_idt &mode,
124  bool result_is_used);
127  goto_programt &dest,
128  const irep_idt &mode,
129  bool result_is_used);
130  void remove_cpp_new(
131  side_effect_exprt &expr,
132  goto_programt &dest,
133  bool result_is_used);
134  void remove_cpp_delete(
135  side_effect_exprt &expr,
136  goto_programt &dest);
137  void remove_malloc(
138  side_effect_exprt &expr,
139  goto_programt &dest,
140  const irep_idt &mode,
141  bool result_is_used);
143  side_effect_exprt &expr,
144  goto_programt &dest);
146  side_effect_exprt &expr,
147  goto_programt &dest,
148  const irep_idt &mode,
149  bool result_is_used);
151  exprt &expr,
152  goto_programt &dest,
153  const irep_idt &mode);
154  void remove_overflow(
156  goto_programt &dest,
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,
163  goto_programt &dest);
164 
166  const exprt &lhs,
167  const side_effect_exprt &rhs,
168  goto_programt &dest);
169 
171  const exprt &lhs,
172  const side_effect_exprt &rhs,
173  goto_programt &dest);
174 
175  static void replace_new_object(
176  const exprt &object,
177  exprt &dest);
178 
179  void cpp_new_initializer(
180  const exprt &lhs,
181  const side_effect_exprt &rhs,
182  goto_programt &dest);
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,
192  goto_programt &dest,
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,
199  goto_programt &dest,
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,
206  goto_programt &dest);
207 
208  virtual void do_function_call_symbol(const symbolt &)
209  {
210  }
211 
212  virtual void do_function_call_other(
213  const exprt &lhs,
214  const exprt &function,
215  const exprt::operandst &arguments,
216  goto_programt &dest);
217 
218  //
219  // conversion
220  //
221  void convert_block(
222  const code_blockt &code,
223  goto_programt &dest,
224  const irep_idt &mode);
225  void convert_decl(
226  const code_declt &code,
227  goto_programt &dest,
228  const irep_idt &mode);
229  void convert_decl_type(const codet &code, goto_programt &dest);
230  void convert_expression(
231  const code_expressiont &code,
232  goto_programt &dest,
233  const irep_idt &mode);
234  void convert_assign(
235  const code_assignt &code,
236  goto_programt &dest,
237  const irep_idt &mode);
238  void convert_cpp_delete(const codet &code, goto_programt &dest);
240  const codet &code,
242  const irep_idt &mode);
243  void
244  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
245  void convert_while(
246  const code_whilet &code,
247  goto_programt &dest,
248  const irep_idt &mode);
249  void convert_dowhile(
250  const code_dowhilet &code,
251  goto_programt &dest,
252  const irep_idt &mode);
253  void convert_assume(
254  const code_assumet &code,
255  goto_programt &dest,
256  const irep_idt &mode);
257  void convert_assert(
258  const code_assertt &code,
259  goto_programt &dest,
260  const irep_idt &mode);
261  void convert_switch(
262  const code_switcht &code,
263  goto_programt &dest,
264  const irep_idt &mode);
265  void convert_break(
266  const code_breakt &code,
267  goto_programt &dest,
268  const irep_idt &mode);
269  void convert_return(
270  const code_returnt &code,
271  goto_programt &dest,
272  const irep_idt &mode);
273  void convert_continue(
274  const code_continuet &code,
275  goto_programt &dest,
276  const irep_idt &mode);
277  void convert_ifthenelse(
278  const code_ifthenelset &code,
279  goto_programt &dest,
280  const irep_idt &mode);
281  void convert_goto(const code_gotot &code, goto_programt &dest);
282  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
283  void convert_skip(const codet &code, goto_programt &dest);
284  void convert_label(
285  const code_labelt &code,
286  goto_programt &dest,
287  const irep_idt &mode);
288  void convert_gcc_local_label(const codet &code, goto_programt &dest);
289  void convert_switch_case(
290  const code_switch_caset &code,
291  goto_programt &dest,
292  const irep_idt &mode);
295  goto_programt &dest,
296  const irep_idt &mode);
298  const code_function_callt &code,
299  goto_programt &dest,
300  const irep_idt &mode);
301  void convert_start_thread(const codet &code, goto_programt &dest);
302  void convert_end_thread(const codet &code, goto_programt &dest);
303  void convert_atomic_begin(const codet &code, goto_programt &dest);
304  void convert_atomic_end(const codet &code, goto_programt &dest);
306  const codet &code,
307  goto_programt &dest,
308  const irep_idt &mode);
310  const codet &code,
311  goto_programt &dest,
312  const irep_idt &mode);
313  void convert_msc_leave(
314  const codet &code,
315  goto_programt &dest,
316  const irep_idt &mode);
317  void convert_try_catch(
318  const codet &code,
319  goto_programt &dest,
320  const irep_idt &mode);
322  const codet &code,
323  goto_programt &dest,
324  const irep_idt &mode);
326  const codet &code,
327  goto_programt &dest,
328  const irep_idt &mode);
330  const codet &code,
331  goto_programt &dest,
332  const irep_idt &mode);
333  void convert_asm(const code_asmt &code, goto_programt &dest);
334 
335  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
336 
337  void copy(
338  const codet &code,
340  goto_programt &dest);
341 
342  //
343  // exceptions
344  //
345 
346  symbol_exprt exception_flag(const irep_idt &mode);
347 
349  const source_locationt &source_location,
350  goto_programt &dest,
351  const irep_idt &mode,
352  optionalt<node_indext> destructor_start_point = {},
353  optionalt<node_indext> destructor_end_point = {});
354 
355  //
356  // gotos
357  //
358 
359  void finish_gotos(goto_programt &dest, const irep_idt &mode);
362 
363  typedef std::map<irep_idt,
364  std::pair<goto_programt::targett, node_indext>>
366  typedef std::list<std::pair<goto_programt::targett, node_indext>>
368  typedef std::list<goto_programt::targett> computed_gotost;
370  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
371  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
372 
373  struct targetst
374  {
377 
382 
385 
388 
391 
393  return_set(false),
394  has_return_value(false),
395  break_set(false),
396  continue_set(false),
397  default_set(false),
398  throw_set(false),
399  leave_set(false),
404  {
405  }
406 
407  void set_break(goto_programt::targett _break_target)
408  {
409  break_set=true;
410  break_target=_break_target;
412  }
413 
414  void set_continue(goto_programt::targett _continue_target)
415  {
416  continue_set=true;
417  continue_target=_continue_target;
419  }
420 
421  void set_default(goto_programt::targett _default_target)
422  {
423  default_set=true;
424  default_target=_default_target;
425  }
426 
427  void set_return(goto_programt::targett _return_target)
428  {
429  return_set=true;
430  return_target=_return_target;
431  }
432 
433  void set_throw(goto_programt::targett _throw_target)
434  {
435  throw_set=true;
436  throw_target=_throw_target;
438  }
439 
440  void set_leave(goto_programt::targett _leave_target)
441  {
442  leave_set=true;
443  leave_target=_leave_target;
445  }
447 
449  {
450  // for 'while', 'for', 'dowhile'
451 
453  {
458  }
459 
461  {
466  }
467 
471  };
472 
474  {
475  // for 'switch'
476 
478  {
486  }
487 
489  {
496  }
497 
502 
505  };
506 
508  {
509  // for 'try...catch' and the like
510 
511  explicit throw_targett(const targetst &targets)
512  {
516  }
517 
519  {
522  }
523 
525  bool throw_set;
527  };
528 
530  {
531  // for 'try...leave...finally'
532 
533  explicit leave_targett(const targetst &targets)
534  {
538  }
539 
541  {
544  }
545 
547  bool leave_set;
549  };
550 
552  const exprt &value,
553  const caset &case_op);
554 
555  // if(cond) { true_case } else { false_case }
556  void generate_ifthenelse(
557  const exprt &cond,
558  goto_programt &true_case,
559  goto_programt &false_case,
560  const source_locationt &,
561  goto_programt &dest,
562  const irep_idt &mode);
563 
564  // if(guard) goto target_true; else goto target_false;
566  const exprt &guard,
567  goto_programt::targett target_true,
568  goto_programt::targett target_false,
569  const source_locationt &,
570  goto_programt &dest,
571  const irep_idt &mode);
572 
573  // if(guard) goto target;
575  const exprt &guard,
576  goto_programt::targett target_true,
577  const source_locationt &,
578  goto_programt &dest,
579  const irep_idt &mode);
580 
581  // turn a OP b OP c into a list a, b, c
582  static void collect_operands(
583  const exprt &expr,
584  const irep_idt &id,
585  std::list<exprt> &dest);
586 
587  // START_THREAD; ... END_THREAD;
589  const code_blockt &thread_body,
590  goto_programt &dest,
591  const irep_idt &mode);
592 
593  //
594  // misc
595  //
596  irep_idt get_string_constant(const exprt &expr);
597  bool get_string_constant(const exprt &expr, irep_idt &);
598  exprt get_constant(const exprt &expr);
599 
614  void do_enum_is_in_range(
615  const exprt &lhs,
616  const symbol_exprt &function,
617  const exprt::operandst &arguments,
618  goto_programt &dest);
619 
620  // some built-in functions
621  void do_atomic_begin(
622  const exprt &lhs,
623  const symbol_exprt &function,
624  const exprt::operandst &arguments,
625  goto_programt &dest);
626  void do_atomic_end(
627  const exprt &lhs,
628  const symbol_exprt &function,
629  const exprt::operandst &arguments,
630  goto_programt &dest);
632  const exprt &lhs,
633  const symbol_exprt &function,
634  const exprt::operandst &arguments,
635  goto_programt &dest);
637  const exprt &lhs,
638  const symbol_exprt &rhs,
639  const exprt::operandst &arguments,
640  goto_programt &dest);
641  void do_array_op(
642  const irep_idt &id,
643  const exprt &lhs,
644  const symbol_exprt &function,
645  const exprt::operandst &arguments,
646  goto_programt &dest);
647  void do_printf(
648  const exprt &lhs,
649  const symbol_exprt &function,
650  const exprt::operandst &arguments,
651  goto_programt &dest);
652  void do_scanf(
653  const exprt &lhs,
654  const symbol_exprt &function,
655  const exprt::operandst &arguments,
656  goto_programt &dest);
657  void do_input(
658  const exprt &rhs,
659  const exprt::operandst &arguments,
660  goto_programt &dest);
661  void do_output(
662  const exprt &rhs,
663  const exprt::operandst &arguments,
664  goto_programt &dest);
665  void do_prob_coin(
666  const exprt &lhs,
667  const symbol_exprt &function,
668  const exprt::operandst &arguments,
669  goto_programt &dest);
670  void do_prob_uniform(
671  const exprt &lhs,
672  const symbol_exprt &function,
673  const exprt::operandst &arguments,
674  goto_programt &dest);
675 
676  exprt get_array_argument(const exprt &src);
677 };
678 
679 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
lifetimet
Selects the kind of objects allocated.
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
codet representation of an inline assembler statement.
Definition: std_code.h:1699
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
A codet representing an assignment in the program.
Definition: std_code.h:293
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
A codet representing sequential composition of program statements.
Definition: std_code.h:168
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1628
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1664
A codet representing the declaration of a local variable.
Definition: std_code.h:400
codet representation of a do while statement.
Definition: std_code.h:988
codet representation of an expression statement.
Definition: std_code.h:1840
codet representation of a for statement.
Definition: std_code.h:1050
codet representation of a function call statement.
Definition: std_code.h:1213
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1543
codet representation of a goto statement.
Definition: std_code.h:1157
codet representation of an if-then-else statement.
Definition: std_code.h:776
codet representation of a label for branch targets.
Definition: std_code.h:1405
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
codet representing a switch statement.
Definition: std_code.h:864
codet representing a while statement.
Definition: std_code.h:926
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
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 convert_return(const code_returnt &code, 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 convert_decl(const code_declt &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;
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
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_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)
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)
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.
Definition: goto_program.h:71
instructionst::iterator targett
Definition: goto_program.h:646
The trinary if-then-else operator.
Definition: std_expr.h:2172
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:2138
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:1896
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:28
std::size_t node_indext
Concrete Goto Program.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:30
dstringt irep_idt
Definition: irep.h:37
nonstd::optional< T > optionalt
Definition: optional.h:35
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
computed_gotost computed_gotos
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)