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;
54  lifetimet lifetime = lifetimet::STATIC_GLOBAL;
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_sideeffect(const exprt &expr);
101  static bool has_function_call(const exprt &expr);
102 
103  void remove_side_effect(
104  side_effect_exprt &expr,
105  goto_programt &dest,
106  const irep_idt &mode,
107  bool result_is_used,
108  bool address_taken);
109  void remove_assignment(
110  side_effect_exprt &expr,
111  goto_programt &dest,
112  bool result_is_used,
113  bool address_taken,
114  const irep_idt &mode);
115  void remove_pre(
116  side_effect_exprt &expr,
117  goto_programt &dest,
118  bool result_is_used,
119  bool address_taken,
120  const irep_idt &mode);
121  void remove_post(
122  side_effect_exprt &expr,
123  goto_programt &dest,
124  const irep_idt &mode,
125  bool result_is_used);
128  goto_programt &dest,
129  const irep_idt &mode,
130  bool result_is_used);
131  void remove_cpp_new(
132  side_effect_exprt &expr,
133  goto_programt &dest,
134  bool result_is_used);
135  void remove_cpp_delete(
136  side_effect_exprt &expr,
137  goto_programt &dest);
138  void remove_malloc(
139  side_effect_exprt &expr,
140  goto_programt &dest,
141  const irep_idt &mode,
142  bool result_is_used);
144  side_effect_exprt &expr,
145  goto_programt &dest);
147  side_effect_exprt &expr,
148  goto_programt &dest,
149  const irep_idt &mode,
150  bool result_is_used);
152  exprt &expr,
153  goto_programt &dest,
154  const irep_idt &mode);
155  void remove_overflow(
157  goto_programt &dest,
158  bool result_is_used,
159  const irep_idt &mode);
160 
161  virtual void do_cpp_new(
162  const exprt &lhs,
163  const side_effect_exprt &rhs,
164  goto_programt &dest);
165 
167  const exprt &lhs,
168  const side_effect_exprt &rhs,
169  goto_programt &dest);
170 
172  const exprt &lhs,
173  const side_effect_exprt &rhs,
174  goto_programt &dest);
175 
176  static void replace_new_object(
177  const exprt &object,
178  exprt &dest);
179 
180  void cpp_new_initializer(
181  const exprt &lhs,
182  const side_effect_exprt &rhs,
183  goto_programt &dest);
184 
185  //
186  // function calls
187  //
188 
189  virtual void do_function_call(
190  const exprt &lhs,
191  const exprt &function,
192  const exprt::operandst &arguments,
193  goto_programt &dest,
194  const irep_idt &mode);
195 
196  virtual void do_function_call_if(
197  const exprt &lhs,
198  const if_exprt &function,
199  const exprt::operandst &arguments,
200  goto_programt &dest,
201  const irep_idt &mode);
202 
203  virtual void do_function_call_symbol(
204  const exprt &lhs,
205  const symbol_exprt &function,
206  const exprt::operandst &arguments,
207  goto_programt &dest);
208 
209  virtual void do_function_call_symbol(const symbolt &)
210  {
211  }
212 
213  virtual void do_function_call_other(
214  const exprt &lhs,
215  const exprt &function,
216  const exprt::operandst &arguments,
217  goto_programt &dest);
218 
219  //
220  // conversion
221  //
222  void convert_block(
223  const code_blockt &code,
224  goto_programt &dest,
225  const irep_idt &mode);
226  void convert_decl(
227  const code_declt &code,
228  goto_programt &dest,
229  const irep_idt &mode);
230  void convert_decl_type(const codet &code, goto_programt &dest);
231  void convert_expression(
232  const code_expressiont &code,
233  goto_programt &dest,
234  const irep_idt &mode);
235  void convert_assign(
236  const code_assignt &code,
237  goto_programt &dest,
238  const irep_idt &mode);
239  void convert_cpp_delete(const codet &code, goto_programt &dest);
241  const codet &code,
243  const irep_idt &mode);
244  void
245  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
246  void convert_while(
247  const code_whilet &code,
248  goto_programt &dest,
249  const irep_idt &mode);
250  void convert_dowhile(
251  const code_dowhilet &code,
252  goto_programt &dest,
253  const irep_idt &mode);
254  void convert_assume(
255  const code_assumet &code,
256  goto_programt &dest,
257  const irep_idt &mode);
258  void convert_assert(
259  const code_assertt &code,
260  goto_programt &dest,
261  const irep_idt &mode);
262  void convert_switch(
263  const code_switcht &code,
264  goto_programt &dest,
265  const irep_idt &mode);
266  void convert_break(
267  const code_breakt &code,
268  goto_programt &dest,
269  const irep_idt &mode);
270  void convert_return(
271  const code_returnt &code,
272  goto_programt &dest,
273  const irep_idt &mode);
274  void convert_continue(
275  const code_continuet &code,
276  goto_programt &dest,
277  const irep_idt &mode);
278  void convert_ifthenelse(
279  const code_ifthenelset &code,
280  goto_programt &dest,
281  const irep_idt &mode);
282  void convert_goto(const code_gotot &code, goto_programt &dest);
283  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
284  void convert_skip(const codet &code, goto_programt &dest);
285  void convert_label(
286  const code_labelt &code,
287  goto_programt &dest,
288  const irep_idt &mode);
289  void convert_gcc_local_label(const codet &code, goto_programt &dest);
290  void convert_switch_case(
291  const code_switch_caset &code,
292  goto_programt &dest,
293  const irep_idt &mode);
296  goto_programt &dest,
297  const irep_idt &mode);
299  const code_function_callt &code,
300  goto_programt &dest,
301  const irep_idt &mode);
302  void convert_start_thread(const codet &code, goto_programt &dest);
303  void convert_end_thread(const codet &code, goto_programt &dest);
304  void convert_atomic_begin(const codet &code, goto_programt &dest);
305  void convert_atomic_end(const codet &code, goto_programt &dest);
307  const codet &code,
308  goto_programt &dest,
309  const irep_idt &mode);
311  const codet &code,
312  goto_programt &dest,
313  const irep_idt &mode);
314  void convert_msc_leave(
315  const codet &code,
316  goto_programt &dest,
317  const irep_idt &mode);
318  void convert_try_catch(
319  const codet &code,
320  goto_programt &dest,
321  const irep_idt &mode);
323  const codet &code,
324  goto_programt &dest,
325  const irep_idt &mode);
327  const codet &code,
328  goto_programt &dest,
329  const irep_idt &mode);
331  const codet &code,
332  goto_programt &dest,
333  const irep_idt &mode);
334  void convert_asm(const code_asmt &code, goto_programt &dest);
335 
336  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
337 
338  void copy(
339  const codet &code,
341  goto_programt &dest);
342 
343  //
344  // exceptions
345  //
346 
347  symbol_exprt exception_flag(const irep_idt &mode);
348 
350  const source_locationt &source_location,
351  goto_programt &dest,
352  const irep_idt &mode,
353  optionalt<node_indext> destructor_start_point = {},
354  optionalt<node_indext> destructor_end_point = {});
355 
356  //
357  // gotos
358  //
359 
360  void finish_gotos(goto_programt &dest, const irep_idt &mode);
363 
364  typedef std::map<irep_idt,
365  std::pair<goto_programt::targett, node_indext>>
367  typedef std::list<std::pair<goto_programt::targett, node_indext>>
369  typedef std::list<goto_programt::targett> computed_gotost;
371  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
372  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
373 
374  struct targetst
375  {
378 
383 
386 
389 
392 
394  return_set(false),
395  has_return_value(false),
396  break_set(false),
397  continue_set(false),
398  default_set(false),
399  throw_set(false),
400  leave_set(false),
405  {
406  }
407 
408  void set_break(goto_programt::targett _break_target)
409  {
410  break_set=true;
411  break_target=_break_target;
413  }
414 
415  void set_continue(goto_programt::targett _continue_target)
416  {
417  continue_set=true;
418  continue_target=_continue_target;
420  }
421 
422  void set_default(goto_programt::targett _default_target)
423  {
424  default_set=true;
425  default_target=_default_target;
426  }
427 
428  void set_return(goto_programt::targett _return_target)
429  {
430  return_set=true;
431  return_target=_return_target;
432  }
433 
434  void set_throw(goto_programt::targett _throw_target)
435  {
436  throw_set=true;
437  throw_target=_throw_target;
439  }
440 
441  void set_leave(goto_programt::targett _leave_target)
442  {
443  leave_set=true;
444  leave_target=_leave_target;
446  }
448 
450  {
451  // for 'while', 'for', 'dowhile'
452 
454  {
459  }
460 
462  {
467  }
468 
472  };
473 
475  {
476  // for 'switch'
477 
479  {
487  }
488 
490  {
497  }
498 
503 
506  };
507 
509  {
510  // for 'try...catch' and the like
511 
512  explicit throw_targett(const targetst &targets)
513  {
517  }
518 
520  {
523  }
524 
526  bool throw_set;
528  };
529 
531  {
532  // for 'try...leave...finally'
533 
534  explicit leave_targett(const targetst &targets)
535  {
539  }
540 
542  {
545  }
546 
548  bool leave_set;
550  };
551 
553  const exprt &value,
554  const caset &case_op);
555 
556  // if(cond) { true_case } else { false_case }
557  void generate_ifthenelse(
558  const exprt &cond,
559  goto_programt &true_case,
560  goto_programt &false_case,
561  const source_locationt &,
562  goto_programt &dest,
563  const irep_idt &mode);
564 
565  // if(guard) goto target_true; else goto target_false;
567  const exprt &guard,
568  goto_programt::targett target_true,
569  goto_programt::targett target_false,
570  const source_locationt &,
571  goto_programt &dest,
572  const irep_idt &mode);
573 
574  // if(guard) goto target;
576  const exprt &guard,
577  goto_programt::targett target_true,
578  const source_locationt &,
579  goto_programt &dest,
580  const irep_idt &mode);
581 
582  // turn a OP b OP c into a list a, b, c
583  static void collect_operands(
584  const exprt &expr,
585  const irep_idt &id,
586  std::list<exprt> &dest);
587 
588  // START_THREAD; ... END_THREAD;
590  const code_blockt &thread_body,
591  goto_programt &dest,
592  const irep_idt &mode);
593 
594  //
595  // misc
596  //
597  irep_idt get_string_constant(const exprt &expr);
598  bool get_string_constant(const exprt &expr, irep_idt &);
599  exprt get_constant(const exprt &expr);
600 
615  void do_enum_is_in_range(
616  const exprt &lhs,
617  const symbol_exprt &function,
618  const exprt::operandst &arguments,
619  goto_programt &dest);
620 
621  // some built-in functions
622  void do_atomic_begin(
623  const exprt &lhs,
624  const symbol_exprt &function,
625  const exprt::operandst &arguments,
626  goto_programt &dest);
627  void do_atomic_end(
628  const exprt &lhs,
629  const symbol_exprt &function,
630  const exprt::operandst &arguments,
631  goto_programt &dest);
633  const exprt &lhs,
634  const symbol_exprt &function,
635  const exprt::operandst &arguments,
636  goto_programt &dest);
638  const exprt &lhs,
639  const symbol_exprt &rhs,
640  const exprt::operandst &arguments,
641  goto_programt &dest);
642  void do_array_op(
643  const irep_idt &id,
644  const exprt &lhs,
645  const symbol_exprt &function,
646  const exprt::operandst &arguments,
647  goto_programt &dest);
648  void do_printf(
649  const exprt &lhs,
650  const symbol_exprt &function,
651  const exprt::operandst &arguments,
652  goto_programt &dest);
653  void do_scanf(
654  const exprt &lhs,
655  const symbol_exprt &function,
656  const exprt::operandst &arguments,
657  goto_programt &dest);
658  void do_input(
659  const exprt &rhs,
660  const exprt::operandst &arguments,
661  goto_programt &dest);
662  void do_output(
663  const exprt &rhs,
664  const exprt::operandst &arguments,
665  goto_programt &dest);
666  void do_prob_coin(
667  const exprt &lhs,
668  const symbol_exprt &function,
669  const exprt::operandst &arguments,
670  goto_programt &dest);
671  void do_prob_uniform(
672  const exprt &lhs,
673  const symbol_exprt &function,
674  const exprt::operandst &arguments,
675  goto_programt &dest);
676 
677  exprt get_array_argument(const exprt &src);
678 };
679 
680 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
goto_convertt::convert_function_call
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_function_call.cpp:24
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_convertt::convert_dowhile
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1031
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
goto_convertt::break_switch_targetst::cases
casest cases
Definition: goto_convert_class.h:504
goto_convertt::do_cpp_new
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
Definition: builtin_functions.cpp:388
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
goto_convertt::targetst::set_break
void set_break(goto_programt::targett _break_target)
Definition: goto_convert_class.h:408
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:66
goto_convertt::do_output
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:327
goto_convertt::break_switch_targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:500
goto_convertt::generate_conditional_branch
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;
Definition: goto_convert.cpp:1658
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:52
goto_convertt::convert_msc_try_finally
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:16
code_whilet
codet representing a while statement.
Definition: std_code.h:928
goto_convertt::targetst::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:388
goto_convertt::do_create_thread
void do_create_thread(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
goto_convertt::replace_new_object
static void replace_new_object(const exprt &object, exprt &dest)
Definition: goto_convert_side_effect.cpp:401
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1701
goto_convertt::convert
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
Definition: goto_convert.cpp:429
code_fort
codet representation of a for statement.
Definition: std_code.h:1052
goto_convertt::leave_targett::leave_set
bool leave_set
Definition: goto_convert_class.h:548
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:299
goto_convertt::targetst::default_set
bool default_set
Definition: goto_convert_class.h:377
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_convertt::clean_expr
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
Definition: goto_clean_expr.cpp:162
goto_convertt::get_array_argument
exprt get_array_argument(const exprt &src)
Definition: builtin_functions.cpp:534
goto_convertt::goto_convert_rec
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:286
goto_convertt::cpp_new_initializer
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
Definition: builtin_functions.cpp:507
goto_convertt::has_function_call
static bool has_function_call(const exprt &expr)
Definition: goto_convert_side_effect.cpp:26
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
goto_convertt::remove_gcc_conditional_expression
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest, const irep_idt &mode)
Definition: goto_clean_expr.cpp:503
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
goto_convertt::convert_skip
void convert_skip(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:840
goto_convertt::do_atomic_end
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:365
goto_convertt::convert_CPROVER_try_finally
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:211
goto_convertt::cases_mapt
std::map< goto_programt::targett, casest::iterator > cases_mapt
Definition: goto_convert_class.h:372
goto_convertt::convert_assert
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:825
goto_convertt::~goto_convertt
virtual ~goto_convertt()
Definition: goto_convert_class.h:46
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:53
goto_convertt::convert_try_catch
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:85
goto_convertt::finish_gotos
void finish_gotos(goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:109
goto_convertt::targetst::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:388
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:619
goto_convertt::has_sideeffect
static bool has_sideeffect(const exprt &expr)
goto_convertt::convert_ifthenelse
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1394
goto_convertt::do_function_call
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_function_call.cpp:37
goto_convertt::generate_ifthenelse
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;
Definition: goto_convert.cpp:1467
goto_convertt::convert_assume
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:848
goto_convertt::remove_function_call
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:346
goto_convertt::leave_targett
Definition: goto_convert_class.h:531
exprt
Base class for all expressions.
Definition: expr.h:54
goto_convertt::convert_block
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:542
goto_convertt::targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:385
code_continuet
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1666
goto_convertt::break_switch_targetst::default_set
bool default_set
Definition: goto_convert_class.h:501
irep_idt
dstringt irep_idt
Definition: irep.h:37
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1545
goto_convertt::clean_expr_address_of
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
Definition: goto_clean_expr.cpp:434
node_indext
std::size_t node_indext
Definition: destructor_tree.h:15
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
namespace.h
goto_convertt::generate_thread_block
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.
Definition: goto_convert.cpp:1908
goto_convertt::break_continue_targetst::break_continue_targetst
break_continue_targetst(const targetst &targets)
Definition: goto_convert_class.h:453
goto_convertt::do_array_equal
void do_array_equal(const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
goto_convertt::convert_switch_case
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:356
goto_convertt::targetst::throw_set
bool throw_set
Definition: goto_convert_class.h:377
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
goto_convertt::new_tmp_symbol
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
Definition: goto_convert.cpp:1819
goto_convertt::goto_convert
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:278
goto_convertt::leave_targett::leave_targett
leave_targett(const targetst &targets)
Definition: goto_convert_class.h:534
goto_convertt::throw_targett
Definition: goto_convert_class.h:509
goto_convertt::targetst::set_leave
void set_leave(goto_programt::targett _leave_target)
Definition: goto_convert_class.h:441
goto_convertt::targetst::leave_set
bool leave_set
Definition: goto_convert_class.h:377
goto_convertt::remove_overflow
void remove_overflow(side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:593
goto_convertt::targetst::has_return_value
bool has_return_value
Definition: goto_convert_class.h:376
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_convertt::targetst::labels
labelst labels
Definition: goto_convert_class.h:379
goto_convertt::do_enum_is_in_range
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...
Definition: builtin_functions.cpp:614
goto_convertt::convert_break
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1229
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
goto_convertt::targetst::gotos
gotost gotos
Definition: goto_convert_class.h:380
goto_convertt::break_switch_targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:505
goto_convertt::exception_flag
symbol_exprt exception_flag(const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:235
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:990
goto_convertt::break_switch_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:489
goto_convertt::targets
struct goto_convertt::targetst targets
goto_convertt::convert_expression
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:572
goto_convertt::break_switch_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:499
goto_convertt::leave_targett::leave_stack_node
node_indext leave_stack_node
Definition: goto_convert_class.h:549
goto_convertt::convert_continue
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1305
goto_convertt::do_scanf
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:210
goto_convertt::unwind_destructor_stack
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...
Definition: goto_convert_exceptions.cpp:283
goto_convertt::convert_CPROVER_try_catch
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:144
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1630
goto_convertt
Definition: goto_convert_class.h:31
goto_convertt::break_continue_targetst::break_set
bool break_set
Definition: goto_convert_class.h:471
goto_convertt::get_string_constant
irep_idt get_string_constant(const exprt &expr)
Definition: goto_convert.cpp:1779
goto_convertt::targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:390
goto_convertt::rewrite_boolean
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
Definition: goto_clean_expr.cpp:111
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
goto_convertt::targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:387
goto_convertt::remove_assignment
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:39
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
goto_convertt::convert_CPROVER_throw
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:180
goto_convertt::do_function_call_other
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: goto_convert_function_call.cpp:152
goto_convertt::optimize_guarded_gotos
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...
Definition: goto_convert.cpp:234
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
goto_convertt::do_java_new
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
goto_convertt::break_continue_targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:470
goto_convertt::remove_statement_expression
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:524
goto_convertt::do_function_call_symbol
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
Definition: builtin_functions.cpp:641
goto_convertt::remove_malloc
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:455
goto_convertt::targetst::set_return
void set_return(goto_programt::targett _return_target)
Definition: goto_convert_class.h:428
goto_convertt::make_compound_literal
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
Definition: goto_clean_expr.cpp:24
destructor_tree.h
goto_convertt::remove_cpp_new
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
Definition: goto_convert_side_effect.cpp:412
goto_convertt::convert_goto
void convert_goto(const code_gotot &code, goto_programt &dest)
Definition: goto_convert.cpp:1324
goto_convertt::break_switch_targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:502
goto_convertt::targetst::return_set
bool return_set
Definition: goto_convert_class.h:376
message_handlert
Definition: message.h:28
goto_convertt::targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:376
goto_convertt::break_continue_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:461
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
goto_convertt::targetst::break_set
bool break_set
Definition: goto_convert_class.h:376
goto_convertt::convert_for
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:883
goto_convertt::targetst::set_throw
void set_throw(goto_programt::targett _throw_target)
Definition: goto_convert_class.h:434
goto_convertt::remove_cpp_delete
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:439
goto_convertt::caset
exprt::operandst caset
Definition: goto_convert_class.h:370
goto_convertt::remove_post
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:265
goto_convertt::get_constant
exprt get_constant(const exprt &expr)
Definition: goto_convert.cpp:1793
goto_convertt::goto_convertt
goto_convertt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: goto_convert_class.h:36
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:609
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_convertt::convert_while
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:975
goto_convertt::convert_assign
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:680
goto_convertt::targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:388
goto_convertt::do_java_new_array
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
goto_convertt::do_function_call_symbol
virtual void do_function_call_symbol(const symbolt &)
Definition: goto_convert_class.h:209
goto_program.h
Concrete Goto Program.
goto_convertt::collect_operands
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
Definition: goto_convert.cpp:1440
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:33
goto_convertt::do_function_call_if
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_function_call.cpp:89
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:21
source_locationt
Definition: source_location.h:20
goto_convertt::remove_temporary_object
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:488
goto_convertt::convert_asm
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
goto_convertt::finish_computed_gotos
void finish_computed_gotos(goto_programt &dest)
Definition: goto_convert.cpp:202
goto_convertt::do_input
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:312
goto_convertt::do_printf
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:196
goto_convertt::targetst
Definition: goto_convert_class.h:375
goto_convertt::do_atomic_begin
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:342
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
goto_convertt::break_switch_targetst::break_switch_targetst
break_switch_targetst(const targetst &targets)
Definition: goto_convert_class.h:478
goto_convertt::convert_msc_leave
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:69
goto_convertt::throw_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:519
goto_convertt::targetst::destructor_stack
destructor_treet destructor_stack
Definition: goto_convert_class.h:382
goto_convertt::case_guard
exprt case_guard(const exprt &value, const caset &case_op)
Definition: goto_convert.cpp:1100
goto_convertt::convert_gcc_local_label
void convert_gcc_local_label(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:349
goto_convertt::convert_return
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1246
code_switcht
codet representing a switch statement.
Definition: std_code.h:866
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_convertt::convert_start_thread
void convert_start_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1346
goto_convertt::targetst::cases
casest cases
Definition: goto_convert_class.h:384
goto_convertt::convert_msc_try_except
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:54
goto_convertt::break_switch_targetst::break_set
bool break_set
Definition: goto_convert_class.h:501
goto_convertt::gotost
std::list< std::pair< goto_programt::targett, node_indext > > gotost
Definition: goto_convert_class.h:368
goto_convertt::convert_loop_invariant
void convert_loop_invariant(const codet &code, goto_programt::targett loop, const irep_idt &mode)
Definition: goto_convert.cpp:860
goto_convertt::computed_gotost
std::list< goto_programt::targett > computed_gotost
Definition: goto_convert_class.h:369
goto_convertt::throw_targett::throw_set
bool throw_set
Definition: goto_convert_class.h:526
destructor_treet::get_current_node
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
Definition: destructor_tree.cpp:97
goto_convertt::remove_pre
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:182
goto_convertt::targetst::set_continue
void set_continue(goto_programt::targett _continue_target)
Definition: goto_convert_class.h:415
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_convertt::do_array_op
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:567
goto_convertt::remove_side_effect
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
Definition: goto_convert_side_effect.cpp:691
goto_convertt::labelst
std::map< irep_idt, std::pair< goto_programt::targett, node_indext > > labelst
Definition: goto_convert_class.h:366
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:51
goto_convertt::break_continue_targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:471
goto_convertt::leave_targett::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:547
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:763
side_effect_expr_overflowt
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
replace_expr.h
goto_convertt::convert_atomic_end
void convert_atomic_end(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1382
goto_convertt::targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:387
goto_convertt::break_switch_targetst
Definition: goto_convert_class.h:475
goto_convertt::throw_targett::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:525
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_convertt::convert_label
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:308
message.h
goto_convertt::targetst::leave_stack_node
node_indext leave_stack_node
Definition: goto_convert_class.h:391
goto_convertt::convert_gcc_switch_case_range
void convert_gcc_switch_case_range(const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:388
goto_convertt::lifetime
lifetimet lifetime
Definition: goto_convert_class.h:54
goto_convertt::break_continue_targetst
Definition: goto_convert_class.h:450
goto_convertt::targetst::set_default
void set_default(goto_programt::targett _default_target)
Definition: goto_convert_class.h:422
allocate_objects.h
goto_convertt::targetst::continue_stack_node
node_indext continue_stack_node
Definition: goto_convert_class.h:390
goto_convertt::throw_targett::throw_stack_node
node_indext throw_stack_node
Definition: goto_convert_class.h:527
goto_convertt::leave_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:541
goto_convertt::throw_targett::throw_targett
throw_targett(const targetst &targets)
Definition: goto_convert_class.h:512
goto_convertt::casest
std::list< std::pair< goto_programt::targett, caset > > casest
Definition: goto_convert_class.h:371
goto_convertt::targetst::targetst
targetst()
Definition: goto_convert_class.h:393
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1898
goto_convertt::convert_atomic_begin
void convert_atomic_begin(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1370
goto_convertt::convert_decl_type
void convert_decl_type(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:673
goto_convertt::targetst::computed_gotos
computed_gotost computed_gotos
Definition: goto_convert_class.h:381
goto_convertt::do_prob_uniform
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:32
goto_convertt::do_prob_coin
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:110
goto_convertt::targetst::throw_stack_node
node_indext throw_stack_node
Definition: goto_convert_class.h:390
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842
goto_convertt::convert_switch
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1129
goto_convertt::break_continue_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:469
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
destructor_treet
Tree to keep track of the destructors generated along each branch of a function.
Definition: destructor_tree.h:89
goto_convertt::targetst::return_target
goto_programt::targett return_target
Definition: goto_convert_class.h:387
goto_convertt::make_temp_symbol
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
Definition: goto_convert.cpp:1842
goto_convertt::convert_end_thread
void convert_end_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1358
goto_convertt::convert_gcc_computed_goto
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1334