CBMC
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 <util/message.h>
16 #include <util/namespace.h>
17 #include <util/replace_expr.h>
18 #include <util/std_code.h>
19 
21 
23 
24 #include "scope_tree.h"
25 
26 #include <list>
27 #include <unordered_set>
28 #include <vector>
29 
32 
33 class goto_convertt : public messaget
34 {
35 public:
36  void
37  goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
38 
40  symbol_table_baset &_symbol_table,
41  message_handlert &_message_handler)
42  : messaget(_message_handler),
43  symbol_table(_symbol_table),
44  ns(_symbol_table),
45  tmp_symbol_prefix("goto_convertt")
46  {
47  }
48 
49  virtual ~goto_convertt()
50  {
51  }
52 
53 protected:
56  std::string tmp_symbol_prefix;
58 
60  {
64  std::list<irep_idt> temporaries;
70 
71  clean_expr_resultt() = default;
72 
73  void add(clean_expr_resultt &&other)
74  {
75  temporaries.splice(temporaries.begin(), other.temporaries);
76  side_effects.destructive_append(other.side_effects);
77  }
78 
79  void add_temporary(const irep_idt &id)
80  {
81  temporaries.push_front(id);
82  }
83  };
84 
85  void goto_convert_rec(
86  const codet &code,
87  goto_programt &dest,
88  const irep_idt &mode);
89 
90  //
91  // tools for symbols
92  //
93  [[nodiscard]] symbolt &new_tmp_symbol(
94  const typet &type,
95  const std::string &suffix,
96  goto_programt &dest,
97  const source_locationt &,
98  const irep_idt &mode);
99 
101  const exprt &expr,
102  goto_programt &dest,
103  const irep_idt &mode);
104 
105  //
106  // translation of C expressions (with side effects)
107  // into the program logic
108  //
109 
110  [[nodiscard]] clean_expr_resultt
111  clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used = true);
112 
113  [[nodiscard]] clean_expr_resultt
114  clean_expr_address_of(exprt &expr, const irep_idt &mode);
115 
116  static bool needs_cleaning(const exprt &expr);
117 
118  // Do we need to introduce a temporary for the value of an assignment
119  // to the given lhs? E.g., a[i] needs a temporary as its value may change
120  // when i is changed; likewise, *p needs a temporary as its value may change
121  // when p is changed.
122  static bool assignment_lhs_needs_temporary(const exprt &lhs)
123  {
124  return lhs.id() != ID_symbol;
125  }
126 
127  [[nodiscard]] irep_idt make_temp_symbol(
128  exprt &expr,
129  const std::string &suffix,
130  goto_programt &,
131  const irep_idt &mode);
132 
133  void rewrite_boolean(exprt &dest);
134 
135  [[nodiscard]] clean_expr_resultt remove_side_effect(
136  side_effect_exprt &expr,
137  const irep_idt &mode,
138  bool result_is_used,
139  bool address_taken);
140  [[nodiscard]] clean_expr_resultt remove_assignment(
141  side_effect_exprt &expr,
142  bool result_is_used,
143  bool address_taken,
144  const irep_idt &mode);
145  [[nodiscard]] clean_expr_resultt remove_pre(
146  side_effect_exprt &expr,
147  bool result_is_used,
148  bool address_taken,
149  const irep_idt &mode);
150  [[nodiscard]] clean_expr_resultt remove_post(
151  side_effect_exprt &expr,
152  const irep_idt &mode,
153  bool result_is_used);
154  [[nodiscard]] clean_expr_resultt remove_function_call(
156  const irep_idt &mode,
157  bool result_is_used);
158  [[nodiscard]] clean_expr_resultt
159  remove_cpp_new(side_effect_exprt &expr, bool result_is_used);
160  [[nodiscard]] clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr);
161  [[nodiscard]] clean_expr_resultt remove_malloc(
162  side_effect_exprt &expr,
163  const irep_idt &mode,
164  bool result_is_used);
165  [[nodiscard]] clean_expr_resultt
167  [[nodiscard]] clean_expr_resultt remove_statement_expression(
168  side_effect_exprt &expr,
169  const irep_idt &mode,
170  bool result_is_used);
171  [[nodiscard]] clean_expr_resultt
173  [[nodiscard]] clean_expr_resultt remove_overflow(
175  bool result_is_used,
176  const irep_idt &mode);
177 
178  virtual void do_cpp_new(
179  const exprt &lhs,
180  const side_effect_exprt &rhs,
181  goto_programt &dest);
182 
184  const exprt &lhs,
185  const side_effect_exprt &rhs,
186  goto_programt &dest);
187 
189  const exprt &lhs,
190  const side_effect_exprt &rhs,
191  goto_programt &dest);
192 
193  static void replace_new_object(const exprt &object, exprt &dest);
194 
195  void cpp_new_initializer(
196  const exprt &lhs,
197  const side_effect_exprt &rhs,
198  goto_programt &dest);
199 
200  //
201  // function calls
202  //
203 
204  virtual void do_function_call(
205  const exprt &lhs,
206  const exprt &function,
207  const exprt::operandst &arguments,
208  goto_programt &dest,
209  const irep_idt &mode);
210 
211  virtual void do_function_call_if(
212  const exprt &lhs,
213  const if_exprt &function,
214  const exprt::operandst &arguments,
215  goto_programt &dest,
216  const irep_idt &mode);
217 
218  virtual void do_function_call_symbol(
219  const exprt &lhs,
220  const symbol_exprt &function,
221  const exprt::operandst &arguments,
222  goto_programt &dest,
223  const irep_idt &mode);
224 
225  virtual void do_function_call_symbol(const symbolt &)
226  {
227  }
228 
229  virtual void do_function_call_other(
230  const exprt &lhs,
231  const exprt &function,
232  const exprt::operandst &arguments,
233  goto_programt &dest);
234 
235  //
236  // conversion
237  //
238  void convert_block(
239  const code_blockt &code,
240  goto_programt &dest,
241  const irep_idt &mode);
243  const code_frontend_declt &,
244  goto_programt &,
245  const irep_idt &mode);
246  void convert_decl_type(const codet &code, goto_programt &dest);
247  void convert_expression(
248  const code_expressiont &code,
249  goto_programt &dest,
250  const irep_idt &mode);
251  void convert_assign(
252  const code_assignt &code,
253  goto_programt &dest,
254  const irep_idt &mode);
255  void convert_cpp_delete(const codet &code, goto_programt &dest);
256  void convert_loop_contracts(const codet &code, goto_programt::targett loop);
257  void
258  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
259  void convert_while(
260  const code_whilet &code,
261  goto_programt &dest,
262  const irep_idt &mode);
263  void convert_dowhile(
264  const code_dowhilet &code,
265  goto_programt &dest,
266  const irep_idt &mode);
267  void convert_assume(
268  const code_assumet &code,
269  goto_programt &dest,
270  const irep_idt &mode);
271  void convert_assert(
272  const code_assertt &code,
273  goto_programt &dest,
274  const irep_idt &mode);
275  void convert_switch(
276  const code_switcht &code,
277  goto_programt &dest,
278  const irep_idt &mode);
279  void convert_break(
280  const code_breakt &code,
281  goto_programt &dest,
282  const irep_idt &mode);
283  void convert_return(
284  const code_frontend_returnt &,
285  goto_programt &dest,
286  const irep_idt &mode);
287  void convert_continue(
288  const code_continuet &code,
289  goto_programt &dest,
290  const irep_idt &mode);
291  void convert_ifthenelse(
292  const code_ifthenelset &code,
293  goto_programt &dest,
294  const irep_idt &mode);
295  void convert_goto(const code_gotot &code, goto_programt &dest);
296  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
297  void convert_skip(const codet &code, goto_programt &dest);
298  void convert_label(
299  const code_labelt &code,
300  goto_programt &dest,
301  const irep_idt &mode);
302  void convert_gcc_local_label(const codet &code, goto_programt &dest);
303  void convert_switch_case(
304  const code_switch_caset &code,
305  goto_programt &dest,
306  const irep_idt &mode);
309  goto_programt &dest,
310  const irep_idt &mode);
312  const code_function_callt &code,
313  goto_programt &dest,
314  const irep_idt &mode);
315  void convert_start_thread(const codet &code, goto_programt &dest);
316  void convert_end_thread(const codet &code, goto_programt &dest);
317  void convert_atomic_begin(const codet &code, goto_programt &dest);
318  void convert_atomic_end(const codet &code, goto_programt &dest);
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_msc_leave(
328  const codet &code,
329  goto_programt &dest,
330  const irep_idt &mode);
331  void convert_try_catch(
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);
344  const codet &code,
345  goto_programt &dest,
346  const irep_idt &mode);
347  void convert_asm(const code_asmt &code, goto_programt &dest);
348 
349  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
350 
351  void copy(
352  const codet &code,
354  goto_programt &dest);
355 
356  //
357  // exceptions
358  //
359 
360  symbol_exprt exception_flag(const irep_idt &mode);
361 
363  const source_locationt &source_location,
364  goto_programt &dest,
365  const irep_idt &mode,
366  std::optional<node_indext> destructor_end_point = {},
367  std::optional<node_indext> destructor_start_point = {});
368 
369  typedef std::list<
370  std::pair<goto_programt::targett, goto_programt::instructiont>>
373  goto_programt &dest,
374  std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
375  const build_declaration_hops_inputst &inputs);
376 
377  //
378  // gotos
379  //
380 
381  void finish_gotos(goto_programt &dest, const irep_idt &mode);
384 
385  typedef std::map<irep_idt, std::pair<goto_programt::targett, node_indext>>
387  typedef std::list<std::pair<goto_programt::targett, node_indext>> gotost;
388  typedef std::list<goto_programt::targett> computed_gotost;
390  typedef std::list<std::pair<goto_programt::targett, caset>> casest;
391  typedef std::map<
393  casest::iterator,
396 
397  struct targetst
398  {
399  goto_programt *prefix = nullptr;
400  goto_programt *suffix = nullptr;
401 
404 
409 
412 
415 
418 
420  : return_set(false),
421  has_return_value(false),
422  break_set(false),
423  continue_set(false),
424  default_set(false),
425  throw_set(false),
426  leave_set(false),
431  {
432  }
433 
434  void set_break(goto_programt::targett _break_target)
435  {
436  break_set = true;
437  break_target = _break_target;
439  }
440 
441  void set_continue(goto_programt::targett _continue_target)
442  {
443  continue_set = true;
444  continue_target = _continue_target;
446  }
447 
448  void set_default(goto_programt::targett _default_target)
449  {
450  default_set = true;
451  default_target = _default_target;
452  }
453 
454  void set_return(goto_programt::targett _return_target)
455  {
456  return_set = true;
457  return_target = _return_target;
458  }
459 
460  void set_throw(goto_programt::targett _throw_target)
461  {
462  throw_set = true;
463  throw_target = _throw_target;
465  }
466 
467  void set_leave(goto_programt::targett _leave_target)
468  {
469  leave_set = true;
470  leave_target = _leave_target;
472  }
474 
476  {
477  // for 'while', 'for', 'dowhile'
478 
480  {
485  }
486 
488  {
493  }
494 
498  };
499 
501  {
502  // for 'switch'
503 
505  {
511  cases = targets.cases;
513  }
514 
516  {
521  targets.cases = cases;
523  }
524 
529 
532  };
533 
535  {
536  // for 'try...catch' and the like
537 
538  explicit throw_targett(const targetst &targets)
539  {
543  }
544 
546  {
549  }
550 
552  bool throw_set;
554  };
555 
557  {
558  // for 'try...leave...finally'
559 
560  explicit leave_targett(const targetst &targets)
561  {
565  }
566 
568  {
571  }
572 
574  bool leave_set;
576  };
577 
578  exprt case_guard(const exprt &value, const caset &case_op);
579 
580  // if(cond) { true_case } else { false_case }
581  void generate_ifthenelse(
582  const exprt &cond,
583  const source_locationt &,
584  goto_programt &true_case,
585  const source_locationt &,
586  goto_programt &false_case,
587  const source_locationt &,
588  goto_programt &dest,
589  const irep_idt &mode);
590 
591  // if(guard) goto target_true; else goto target_false;
593  const exprt &guard,
594  goto_programt::targett target_true,
595  goto_programt::targett target_false,
596  const source_locationt &,
597  goto_programt &dest,
598  const irep_idt &mode);
599 
600  // if(guard) goto target;
602  const exprt &guard,
603  goto_programt::targett target_true,
604  const source_locationt &,
605  goto_programt &dest,
606  const irep_idt &mode);
607 
608  // turn a OP b OP c into a list a, b, c
609  static void collect_operands(
610  const exprt &expr,
611  const irep_idt &id,
612  std::list<exprt> &dest);
613 
614  // START_THREAD; ... END_THREAD;
616  const code_blockt &thread_body,
617  goto_programt &dest,
618  const irep_idt &mode);
619 
620  //
621  // misc
622  //
623  irep_idt get_string_constant(const exprt &expr);
624  bool get_string_constant(const exprt &expr, irep_idt &);
625  exprt get_constant(const exprt &expr);
626 
627  // some built-in functions
628  void do_atomic_begin(
629  const exprt &lhs,
630  const symbol_exprt &function,
631  const exprt::operandst &arguments,
632  goto_programt &dest);
633  void do_atomic_end(
634  const exprt &lhs,
635  const symbol_exprt &function,
636  const exprt::operandst &arguments,
637  goto_programt &dest);
639  const exprt &lhs,
640  const symbol_exprt &function,
641  const exprt::operandst &arguments,
642  goto_programt &dest);
644  const exprt &lhs,
645  const symbol_exprt &rhs,
646  const exprt::operandst &arguments,
647  goto_programt &dest);
648  void do_array_op(
649  const irep_idt &id,
650  const exprt &lhs,
651  const symbol_exprt &function,
652  const exprt::operandst &arguments,
653  goto_programt &dest);
654  void do_printf(
655  const exprt &lhs,
656  const symbol_exprt &function,
657  const exprt::operandst &arguments,
658  goto_programt &dest);
659  void do_scanf(
660  const exprt &lhs,
661  const symbol_exprt &function,
662  const exprt::operandst &arguments,
663  goto_programt &dest);
664  void do_input(
665  const exprt &rhs,
666  const exprt::operandst &arguments,
667  goto_programt &dest);
668  void do_output(
669  const exprt &rhs,
670  const exprt::operandst &arguments,
671  goto_programt &dest);
672  void do_prob_coin(
673  const exprt &lhs,
674  const symbol_exprt &function,
675  const exprt::operandst &arguments,
676  goto_programt &dest);
677  void do_prob_uniform(
678  const exprt &lhs,
679  const symbol_exprt &function,
680  const exprt::operandst &arguments,
681  goto_programt &dest);
682  void do_havoc_slice(
683  const exprt &lhs,
684  const symbol_exprt &function,
685  const exprt::operandst &arguments,
686  goto_programt &dest,
687  const irep_idt &mode);
688  void do_alloca(
689  const exprt &lhs,
690  const symbol_exprt &function,
691  const exprt::operandst &arguments,
692  goto_programt &dest,
693  const irep_idt &mode);
694 
695  exprt get_array_argument(const exprt &src);
696 };
697 
698 #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)
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.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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)
clean_expr_resultt clean_expr_address_of(exprt &expr, const irep_idt &mode)
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 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_loop_contracts(const codet &code, goto_programt::targett loop)
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)
clean_expr_resultt remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode)
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 convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_pre(side_effect_exprt &expr, bool result_is_used, bool address_taken, 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 generate_ifthenelse(const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
void convert_start_thread(const codet &code, goto_programt &dest)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_post(side_effect_exprt &expr, 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 unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
struct goto_convertt::targetst targets
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void 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)
clean_expr_resultt remove_assignment(side_effect_exprt &expr, bool result_is_used, bool address_taken, 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 convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_malloc(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
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 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 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)
clean_expr_resultt remove_side_effect(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
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)
exprt get_array_argument(const exprt &src)
irep_idt make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
Returns 'true' for expressions that may change the program state.
clean_expr_resultt remove_cpp_new(side_effect_exprt &expr, bool result_is_used)
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
virtual void do_function_call_symbol(const symbolt &)
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'
clean_expr_resultt remove_temporary_object(side_effect_exprt &expr)
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)
std::list< std::pair< goto_programt::targett, goto_programt::instructiont > > declaration_hop_instrumentationt
virtual ~goto_convertt()
clean_expr_resultt remove_function_call(side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
std::list< std::pair< goto_programt::targett, node_indext > > gotost
exprt::operandst caset
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void do_array_equal(const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
declaration_hop_instrumentationt build_declaration_hops(goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)
static void replace_new_object(const exprt &object, exprt &dest)
clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr)
clean_expr_resultt remove_statement_expression(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
void convert_msc_leave(const codet &code, goto_programt &dest, 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)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_overflow(side_effect_expr_overflowt &expr, bool result_is_used, 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.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
The trinary if-then-else operator.
Definition: std_expr.h:2375
const irep_idt & id() const
Definition: irep.h:388
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Tree to keep track of the destructors generated along each branch of a function.
Definition: scope_tree.h:93
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
Definition: scope_tree.cpp:109
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:118
An expression containing a side effect.
Definition: std_code.h:1450
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
Concrete Goto Program.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:32
std::size_t node_indext
Definition: scope_tree.h:19
break_continue_targetst(const targetst &targets)
break_switch_targetst(const targetst &targets)
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
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)
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.
Definition: goto_program.h:392