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 
28 class goto_convertt:public messaget
29 {
30 public:
31  void
32  goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
33 
35  symbol_table_baset &_symbol_table,
36  message_handlert &_message_handler):
37  messaget(_message_handler),
38  symbol_table(_symbol_table),
39  ns(_symbol_table),
40  tmp_symbol_prefix("goto_convertt")
41  {
42  }
43 
44  virtual ~goto_convertt()
45  {
46  }
47 
48 protected:
51  std::string tmp_symbol_prefix;
53 
54  void goto_convert_rec(
55  const codet &code,
56  goto_programt &dest,
57  const irep_idt &mode);
58 
59  //
60  // tools for symbols
61  //
63  const typet &type,
64  const std::string &suffix,
65  goto_programt &dest,
66  const source_locationt &,
67  const irep_idt &mode);
68 
70  const exprt &expr,
71  goto_programt &dest,
72  const irep_idt &mode);
73 
74  //
75  // translation of C expressions (with side effects)
76  // into the program logic
77  //
78 
79  void clean_expr(
80  exprt &expr,
81  goto_programt &dest,
82  const irep_idt &mode,
83  bool result_is_used = true);
84 
85  void
86  clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode);
87 
88  static bool needs_cleaning(const exprt &expr);
89 
90  void make_temp_symbol(
91  exprt &expr,
92  const std::string &suffix,
93  goto_programt &,
94  const irep_idt &mode);
95 
96  void rewrite_boolean(exprt &dest);
97 
98  static bool has_sideeffect(const exprt &expr);
99  static bool has_function_call(const exprt &expr);
100 
101  void remove_side_effect(
102  side_effect_exprt &expr,
103  goto_programt &dest,
104  const irep_idt &mode,
105  bool result_is_used,
106  bool address_taken);
107  void remove_assignment(
108  side_effect_exprt &expr,
109  goto_programt &dest,
110  bool result_is_used,
111  bool address_taken,
112  const irep_idt &mode);
113  void remove_pre(
114  side_effect_exprt &expr,
115  goto_programt &dest,
116  bool result_is_used,
117  bool address_taken,
118  const irep_idt &mode);
119  void remove_post(
120  side_effect_exprt &expr,
121  goto_programt &dest,
122  const irep_idt &mode,
123  bool result_is_used);
126  goto_programt &dest,
127  const irep_idt &mode,
128  bool result_is_used);
129  void remove_cpp_new(
130  side_effect_exprt &expr,
131  goto_programt &dest,
132  bool result_is_used);
133  void remove_cpp_delete(
134  side_effect_exprt &expr,
135  goto_programt &dest);
136  void remove_malloc(
137  side_effect_exprt &expr,
138  goto_programt &dest,
139  const irep_idt &mode,
140  bool result_is_used);
142  side_effect_exprt &expr,
143  goto_programt &dest);
145  side_effect_exprt &expr,
146  goto_programt &dest,
147  const irep_idt &mode,
148  bool result_is_used);
150  exprt &expr,
151  goto_programt &dest,
152  const irep_idt &mode);
153 
154  virtual void do_cpp_new(
155  const exprt &lhs,
156  const side_effect_exprt &rhs,
157  goto_programt &dest);
158 
160  const exprt &lhs,
161  const side_effect_exprt &rhs,
162  goto_programt &dest);
163 
165  const exprt &lhs,
166  const side_effect_exprt &rhs,
167  goto_programt &dest);
168 
169  static void replace_new_object(
170  const exprt &object,
171  exprt &dest);
172 
173  void cpp_new_initializer(
174  const exprt &lhs,
175  const side_effect_exprt &rhs,
176  goto_programt &dest);
177 
178  //
179  // function calls
180  //
181 
182  virtual void do_function_call(
183  const exprt &lhs,
184  const exprt &function,
185  const exprt::operandst &arguments,
186  goto_programt &dest,
187  const irep_idt &mode);
188 
189  virtual void do_function_call_if(
190  const exprt &lhs,
191  const if_exprt &function,
192  const exprt::operandst &arguments,
193  goto_programt &dest,
194  const irep_idt &mode);
195 
196  virtual void do_function_call_symbol(
197  const exprt &lhs,
198  const symbol_exprt &function,
199  const exprt::operandst &arguments,
200  goto_programt &dest);
201 
202  virtual void do_function_call_symbol(const symbolt &)
203  {
204  }
205 
206  virtual void do_function_call_other(
207  const exprt &lhs,
208  const exprt &function,
209  const exprt::operandst &arguments,
210  goto_programt &dest);
211 
212  //
213  // conversion
214  //
215  void convert_block(
216  const code_blockt &code,
217  goto_programt &dest,
218  const irep_idt &mode);
219  void convert_decl(
220  const code_declt &code,
221  goto_programt &dest,
222  const irep_idt &mode);
223  void convert_decl_type(const codet &code, goto_programt &dest);
224  void convert_expression(
225  const code_expressiont &code,
226  goto_programt &dest,
227  const irep_idt &mode);
228  void convert_assign(
229  const code_assignt &code,
230  goto_programt &dest,
231  const irep_idt &mode);
232  void convert_cpp_delete(const codet &code, goto_programt &dest);
234  const codet &code,
236  const irep_idt &mode);
237  void
238  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
239  void convert_while(
240  const code_whilet &code,
241  goto_programt &dest,
242  const irep_idt &mode);
243  void convert_dowhile(
244  const code_dowhilet &code,
245  goto_programt &dest,
246  const irep_idt &mode);
247  void convert_assume(
248  const code_assumet &code,
249  goto_programt &dest,
250  const irep_idt &mode);
251  void convert_assert(
252  const code_assertt &code,
253  goto_programt &dest,
254  const irep_idt &mode);
255  void convert_switch(
256  const code_switcht &code,
257  goto_programt &dest,
258  const irep_idt &mode);
259  void convert_break(
260  const code_breakt &code,
261  goto_programt &dest,
262  const irep_idt &mode);
263  void convert_return(
264  const code_returnt &code,
265  goto_programt &dest,
266  const irep_idt &mode);
267  void convert_continue(
268  const code_continuet &code,
269  goto_programt &dest,
270  const irep_idt &mode);
271  void convert_ifthenelse(
272  const code_ifthenelset &code,
273  goto_programt &dest,
274  const irep_idt &mode);
275  void convert_goto(const code_gotot &code, goto_programt &dest);
276  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
277  void convert_skip(const codet &code, goto_programt &dest);
278  void convert_label(
279  const code_labelt &code,
280  goto_programt &dest,
281  const irep_idt &mode);
282  void convert_gcc_local_label(const codet &code, goto_programt &dest);
283  void convert_switch_case(
284  const code_switch_caset &code,
285  goto_programt &dest,
286  const irep_idt &mode);
289  goto_programt &dest,
290  const irep_idt &mode);
292  const code_function_callt &code,
293  goto_programt &dest,
294  const irep_idt &mode);
295  void convert_start_thread(const codet &code, goto_programt &dest);
296  void convert_end_thread(const codet &code, goto_programt &dest);
297  void convert_atomic_begin(const codet &code, goto_programt &dest);
298  void convert_atomic_end(const codet &code, goto_programt &dest);
300  const codet &code,
301  goto_programt &dest,
302  const irep_idt &mode);
304  const codet &code,
305  goto_programt &dest,
306  const irep_idt &mode);
307  void convert_msc_leave(
308  const codet &code,
309  goto_programt &dest,
310  const irep_idt &mode);
311  void convert_try_catch(
312  const codet &code,
313  goto_programt &dest,
314  const irep_idt &mode);
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);
327  void convert_asm(const code_asmt &code, goto_programt &dest);
328 
329  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
330 
331  void copy(
332  const codet &code,
334  goto_programt &dest);
335 
336  //
337  // exceptions
338  //
339 
340  symbol_exprt exception_flag(const irep_idt &mode);
341 
343  const source_locationt &source_location,
344  goto_programt &dest,
345  const irep_idt &mode,
346  optionalt<node_indext> destructor_start_point = {},
347  optionalt<node_indext> destructor_end_point = {});
348 
349  //
350  // gotos
351  //
352 
353  void finish_gotos(goto_programt &dest, const irep_idt &mode);
356 
357  typedef std::map<irep_idt,
358  std::pair<goto_programt::targett, node_indext>>
360  typedef std::list<std::pair<goto_programt::targett, node_indext>>
362  typedef std::list<goto_programt::targett> computed_gotost;
364  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
365  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
366 
367  struct targetst
368  {
371 
376 
379 
382 
385 
387  return_set(false),
388  has_return_value(false),
389  break_set(false),
390  continue_set(false),
391  default_set(false),
392  throw_set(false),
393  leave_set(false),
398  {
399  }
400 
401  void set_break(goto_programt::targett _break_target)
402  {
403  break_set=true;
404  break_target=_break_target;
406  }
407 
408  void set_continue(goto_programt::targett _continue_target)
409  {
410  continue_set=true;
411  continue_target=_continue_target;
413  }
414 
415  void set_default(goto_programt::targett _default_target)
416  {
417  default_set=true;
418  default_target=_default_target;
419  }
420 
421  void set_return(goto_programt::targett _return_target)
422  {
423  return_set=true;
424  return_target=_return_target;
425  }
426 
427  void set_throw(goto_programt::targett _throw_target)
428  {
429  throw_set=true;
430  throw_target=_throw_target;
432  }
433 
434  void set_leave(goto_programt::targett _leave_target)
435  {
436  leave_set=true;
437  leave_target=_leave_target;
439  }
441 
443  {
444  // for 'while', 'for', 'dowhile'
445 
447  {
452  }
453 
455  {
460  }
461 
465  };
466 
468  {
469  // for 'switch'
470 
472  {
480  }
481 
483  {
490  }
491 
496 
499  };
500 
502  {
503  // for 'try...catch' and the like
504 
505  explicit throw_targett(const targetst &targets)
506  {
510  }
511 
513  {
516  }
517 
519  bool throw_set;
521  };
522 
524  {
525  // for 'try...leave...finally'
526 
527  explicit leave_targett(const targetst &targets)
528  {
532  }
533 
535  {
538  }
539 
541  bool leave_set;
543  };
544 
546  const exprt &value,
547  const caset &case_op);
548 
549  // if(cond) { true_case } else { false_case }
550  void generate_ifthenelse(
551  const exprt &cond,
552  goto_programt &true_case,
553  goto_programt &false_case,
554  const source_locationt &,
555  goto_programt &dest,
556  const irep_idt &mode);
557 
558  // if(guard) goto target_true; else goto target_false;
560  const exprt &guard,
561  goto_programt::targett target_true,
562  goto_programt::targett target_false,
563  const source_locationt &,
564  goto_programt &dest,
565  const irep_idt &mode);
566 
567  // if(guard) goto target;
569  const exprt &guard,
570  goto_programt::targett target_true,
571  const source_locationt &,
572  goto_programt &dest,
573  const irep_idt &mode);
574 
575  // turn a OP b OP c into a list a, b, c
576  static void collect_operands(
577  const exprt &expr,
578  const irep_idt &id,
579  std::list<exprt> &dest);
580 
581  // START_THREAD; ... END_THREAD;
583  const code_blockt &thread_body,
584  goto_programt &dest,
585  const irep_idt &mode);
586 
587  //
588  // misc
589  //
590  irep_idt get_string_constant(const exprt &expr);
591  bool get_string_constant(const exprt &expr, irep_idt &);
592  exprt get_constant(const exprt &expr);
593 
608  void do_enum_is_in_range(
609  const exprt &lhs,
610  const symbol_exprt &function,
611  const exprt::operandst &arguments,
612  goto_programt &dest);
613 
614  // some built-in functions
615  void do_atomic_begin(
616  const exprt &lhs,
617  const symbol_exprt &function,
618  const exprt::operandst &arguments,
619  goto_programt &dest);
620  void do_atomic_end(
621  const exprt &lhs,
622  const symbol_exprt &function,
623  const exprt::operandst &arguments,
624  goto_programt &dest);
626  const exprt &lhs,
627  const symbol_exprt &function,
628  const exprt::operandst &arguments,
629  goto_programt &dest);
631  const exprt &lhs,
632  const symbol_exprt &rhs,
633  const exprt::operandst &arguments,
634  goto_programt &dest);
635  void do_array_op(
636  const irep_idt &id,
637  const exprt &lhs,
638  const symbol_exprt &function,
639  const exprt::operandst &arguments,
640  goto_programt &dest);
641  void do_printf(
642  const exprt &lhs,
643  const symbol_exprt &function,
644  const exprt::operandst &arguments,
645  goto_programt &dest);
646  void do_scanf(
647  const exprt &lhs,
648  const symbol_exprt &function,
649  const exprt::operandst &arguments,
650  goto_programt &dest);
651  void do_input(
652  const exprt &rhs,
653  const exprt::operandst &arguments,
654  goto_programt &dest);
655  void do_output(
656  const exprt &rhs,
657  const exprt::operandst &arguments,
658  goto_programt &dest);
659  void do_prob_coin(
660  const exprt &lhs,
661  const symbol_exprt &function,
662  const exprt::operandst &arguments,
663  goto_programt &dest);
664  void do_prob_uniform(
665  const exprt &lhs,
666  const symbol_exprt &function,
667  const exprt::operandst &arguments,
668  goto_programt &dest);
669 
670  exprt get_array_argument(const exprt &src);
671 };
672 
673 #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:1701
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:619
A codet representing an assignment in the program.
Definition: std_code.h:295
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
A codet representing sequential composition of program statements.
Definition: std_code.h:170
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1630
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1666
A codet representing the declaration of a local variable.
Definition: std_code.h:402
codet representation of a do while statement.
Definition: std_code.h:990
codet representation of an expression statement.
Definition: std_code.h:1842
codet representation of a for statement.
Definition: std_code.h:1052
codet representation of a function call statement.
Definition: std_code.h:1215
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1545
codet representation of a goto statement.
Definition: std_code.h:1159
codet representation of an if-then-else statement.
Definition: std_code.h:778
codet representation of a label for branch targets.
Definition: std_code.h:1407
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
codet representing a switch statement.
Definition: std_code.h:866
codet representing a while statement.
Definition: std_code.h:928
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
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 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)
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)
static bool has_sideeffect(const exprt &expr)
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 convert_loop_invariant(const codet &code, goto_programt::targett loop, const irep_idt &mode)
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:74
instructionst::iterator targett
Definition: goto_program.h:550
The trinary if-then-else operator.
Definition: std_expr.h:2087
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:92
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
An expression containing a side effect.
Definition: std_code.h:1898
Expression to hold a symbol (variable)
Definition: std_expr.h:81
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:33
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)