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 
18 #include <util/namespace.h>
19 #include <util/replace_expr.h>
20 #include <util/guard.h>
21 #include <util/std_code.h>
22 #include <util/message.h>
23 
24 #include "goto_program.h"
25 
26 class goto_convertt:public messaget
27 {
28 public:
29  void
30  goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
31 
33  symbol_table_baset &_symbol_table,
34  message_handlert &_message_handler):
35  messaget(_message_handler),
36  symbol_table(_symbol_table),
37  ns(_symbol_table),
38  tmp_symbol_prefix("goto_convertt")
39  {
40  }
41 
42  virtual ~goto_convertt()
43  {
44  }
45 
46 protected:
49  std::string tmp_symbol_prefix;
50 
51  void goto_convert_rec(
52  const codet &code,
53  goto_programt &dest,
54  const irep_idt &mode);
55 
56  //
57  // tools for symbols
58  //
60  const typet &type,
61  const std::string &suffix,
62  goto_programt &dest,
63  const source_locationt &,
64  const irep_idt &mode);
65 
67  const exprt &expr,
68  goto_programt &dest,
69  const irep_idt &mode);
70 
71  //
72  // translation of C expressions (with side effects)
73  // into the program logic
74  //
75 
76  void clean_expr(
77  exprt &expr,
78  goto_programt &dest,
79  const irep_idt &mode,
80  bool result_is_used = true);
81 
82  void
83  clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode);
84 
85  static bool needs_cleaning(const exprt &expr);
86 
87  void make_temp_symbol(
88  exprt &expr,
89  const std::string &suffix,
90  goto_programt &,
91  const irep_idt &mode);
92 
93  void rewrite_boolean(exprt &dest);
94 
95  static bool has_sideeffect(const exprt &expr);
96  static bool has_function_call(const exprt &expr);
97 
98  void remove_side_effect(
99  side_effect_exprt &expr,
100  goto_programt &dest,
101  const irep_idt &mode,
102  bool result_is_used);
103  void remove_assignment(
104  side_effect_exprt &expr,
105  goto_programt &dest,
106  bool result_is_used,
107  const irep_idt &mode);
108  void remove_pre(
109  side_effect_exprt &expr,
110  goto_programt &dest,
111  bool result_is_used,
112  const irep_idt &mode);
113  void remove_post(
114  side_effect_exprt &expr,
115  goto_programt &dest,
116  const irep_idt &mode,
117  bool result_is_used);
119  side_effect_exprt &expr,
120  goto_programt &dest,
121  const irep_idt &mode,
122  bool result_is_used);
123  void remove_cpp_new(
124  side_effect_exprt &expr,
125  goto_programt &dest,
126  bool result_is_used);
127  void remove_cpp_delete(
128  side_effect_exprt &expr,
129  goto_programt &dest);
130  void remove_malloc(
131  side_effect_exprt &expr,
132  goto_programt &dest,
133  const irep_idt &mode,
134  bool result_is_used);
136  side_effect_exprt &expr,
137  goto_programt &dest);
139  side_effect_exprt &expr,
140  goto_programt &dest,
141  const irep_idt &mode,
142  bool result_is_used);
144  exprt &expr,
145  goto_programt &dest,
146  const irep_idt &mode);
147 
148  virtual void do_cpp_new(
149  const exprt &lhs,
150  const side_effect_exprt &rhs,
151  goto_programt &dest);
152 
153  void do_java_new(
154  const exprt &lhs,
155  const side_effect_exprt &rhs,
156  goto_programt &dest);
157 
158  void do_java_new_array(
159  const exprt &lhs,
160  const side_effect_exprt &rhs,
161  goto_programt &dest);
162 
163  static void replace_new_object(
164  const exprt &object,
165  exprt &dest);
166 
167  void cpp_new_initializer(
168  const exprt &lhs,
169  const side_effect_exprt &rhs,
170  goto_programt &dest);
171 
172  //
173  // function calls
174  //
175 
176  virtual void do_function_call(
177  const exprt &lhs,
178  const exprt &function,
179  const exprt::operandst &arguments,
180  goto_programt &dest,
181  const irep_idt &mode);
182 
183  virtual void do_function_call_if(
184  const exprt &lhs,
185  const if_exprt &function,
186  const exprt::operandst &arguments,
187  goto_programt &dest,
188  const irep_idt &mode);
189 
190  virtual void do_function_call_symbol(
191  const exprt &lhs,
192  const symbol_exprt &function,
193  const exprt::operandst &arguments,
194  goto_programt &dest);
195 
196  virtual void do_function_call_symbol(const symbolt &)
197  {
198  }
199 
200  virtual void do_function_call_other(
201  const exprt &lhs,
202  const exprt &function,
203  const exprt::operandst &arguments,
204  goto_programt &dest);
205 
206  //
207  // conversion
208  //
209  void convert_block(
210  const code_blockt &code,
211  goto_programt &dest,
212  const irep_idt &mode);
213  void convert_decl(
214  const code_declt &code,
215  goto_programt &dest,
216  const irep_idt &mode);
217  void convert_decl_type(const codet &code, goto_programt &dest);
218  void convert_expression(
219  const code_expressiont &code,
220  goto_programt &dest,
221  const irep_idt &mode);
222  void convert_assign(
223  const code_assignt &code,
224  goto_programt &dest,
225  const irep_idt &mode);
226  void convert_cpp_delete(const codet &code, goto_programt &dest);
228  const codet &code,
230  const irep_idt &mode);
231  void
232  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
233  void convert_while(
234  const code_whilet &code,
235  goto_programt &dest,
236  const irep_idt &mode);
237  void convert_dowhile(
238  const code_dowhilet &code,
239  goto_programt &dest,
240  const irep_idt &mode);
241  void convert_assume(
242  const code_assumet &code,
243  goto_programt &dest,
244  const irep_idt &mode);
245  void convert_assert(
246  const code_assertt &code,
247  goto_programt &dest,
248  const irep_idt &mode);
249  void convert_switch(
250  const code_switcht &code,
251  goto_programt &dest,
252  const irep_idt &mode);
253  void convert_break(
254  const code_breakt &code,
255  goto_programt &dest,
256  const irep_idt &mode);
257  void convert_return(
258  const code_returnt &code,
259  goto_programt &dest,
260  const irep_idt &mode);
261  void convert_continue(
262  const code_continuet &code,
263  goto_programt &dest,
264  const irep_idt &mode);
265  void convert_ifthenelse(
266  const code_ifthenelset &code,
267  goto_programt &dest,
268  const irep_idt &mode);
269  void
270  convert_init(const codet &code, goto_programt &dest, const irep_idt &mode);
271  void convert_goto(const code_gotot &code, goto_programt &dest);
272  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
273  void convert_skip(const codet &code, goto_programt &dest);
274  void convert_label(
275  const code_labelt &code,
276  goto_programt &dest,
277  const irep_idt &mode);
278  void convert_gcc_local_label(const codet &code, goto_programt &dest);
279  void convert_switch_case(
280  const code_switch_caset &code,
281  goto_programt &dest,
282  const irep_idt &mode);
284  const codet &code,
285  goto_programt &dest,
286  const irep_idt &mode);
288  const code_function_callt &code,
289  goto_programt &dest,
290  const irep_idt &mode);
291  void convert_start_thread(const codet &code, goto_programt &dest);
292  void convert_end_thread(const codet &code, goto_programt &dest);
293  void convert_atomic_begin(const codet &code, goto_programt &dest);
294  void convert_atomic_end(const codet &code, goto_programt &dest);
296  const codet &code,
297  goto_programt &dest,
298  const irep_idt &mode);
300  const codet &code,
301  goto_programt &dest,
302  const irep_idt &mode);
303  void convert_msc_leave(
304  const codet &code,
305  goto_programt &dest,
306  const irep_idt &mode);
307  void convert_try_catch(
308  const codet &code,
309  goto_programt &dest,
310  const irep_idt &mode);
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);
323  void convert_asm(const code_asmt &code, goto_programt &dest);
324 
325  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
326 
327  void copy(
328  const codet &code,
330  goto_programt &dest);
331 
332  //
333  // exceptions
334  //
335 
336  typedef std::vector<codet> destructor_stackt;
337 
340  const source_locationt &,
341  std::size_t stack_size,
342  goto_programt &dest,
343  const irep_idt &mode);
345  const source_locationt &,
346  std::size_t stack_size,
347  goto_programt &dest,
349  const irep_idt &mode);
350 
351  //
352  // gotos
353  //
354 
355  void finish_gotos(goto_programt &dest, const irep_idt &mode);
358 
359  typedef std::map<irep_idt,
360  std::pair<goto_programt::targett, destructor_stackt>>
362  typedef std::list<std::pair<goto_programt::targett, destructor_stackt>>
364  typedef std::list<goto_programt::targett> computed_gotost;
366  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
367  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
368 
369  struct targetst
370  {
373 
378 
381 
384 
387 
389  return_set(false),
390  has_return_value(false),
391  break_set(false),
392  continue_set(false),
393  default_set(false),
394  throw_set(false),
395  leave_set(false),
396  break_stack_size(0),
398  throw_stack_size(0),
400  {
401  }
402 
403  void set_break(goto_programt::targett _break_target)
404  {
405  break_set=true;
406  break_target=_break_target;
408  }
409 
410  void set_continue(goto_programt::targett _continue_target)
411  {
412  continue_set=true;
413  continue_target=_continue_target;
415  }
416 
417  void set_default(goto_programt::targett _default_target)
418  {
419  default_set=true;
420  default_target=_default_target;
421  }
422 
423  void set_return(goto_programt::targett _return_target)
424  {
425  return_set=true;
426  return_target=_return_target;
427  }
428 
429  void set_throw(goto_programt::targett _throw_target)
430  {
431  throw_set=true;
432  throw_target=_throw_target;
434  }
435 
436  void set_leave(goto_programt::targett _leave_target)
437  {
438  leave_set=true;
439  leave_target=_leave_target;
441  }
442  } targets;
443 
445  {
446  // for 'while', 'for', 'dowhile'
447 
449  {
454  }
455 
457  {
462  }
463 
467  };
468 
470  {
471  // for 'switch'
472 
474  {
482  }
483 
485  {
492  }
493 
497  std::size_t break_stack_size;
498 
501  };
502 
504  {
505  // for 'try...catch' and the like
506 
507  explicit throw_targett(const targetst &targets)
508  {
512  }
513 
515  {
518  }
519 
521  bool throw_set;
522  std::size_t throw_stack_size;
523  };
524 
526  {
527  // for 'try...leave...finally'
528 
529  explicit leave_targett(const targetst &targets)
530  {
534  }
535 
537  {
540  }
541 
543  bool leave_set;
544  std::size_t leave_stack_size;
545  };
546 
548  const exprt &value,
549  const caset &case_op);
550 
551  // if(cond) { true_case } else { false_case }
552  void generate_ifthenelse(
553  const exprt &cond,
554  goto_programt &true_case,
555  goto_programt &false_case,
556  const source_locationt &,
557  goto_programt &dest,
558  const irep_idt &mode);
559 
560  // if(guard) goto target_true; else goto target_false;
562  const exprt &guard,
563  goto_programt::targett target_true,
564  goto_programt::targett target_false,
565  const source_locationt &,
566  goto_programt &dest,
567  const irep_idt &mode);
568 
569  // if(guard) goto target;
571  const exprt &guard,
572  goto_programt::targett target_true,
573  const source_locationt &,
574  goto_programt &dest,
575  const irep_idt &mode);
576 
577  // turn a OP b OP c into a list a, b, c
578  static void collect_operands(
579  const exprt &expr,
580  const irep_idt &id,
581  std::list<exprt> &dest);
582 
583  // START_THREAD; ... END_THREAD;
585  const code_blockt &thread_body,
586  goto_programt &dest,
587  const irep_idt &mode);
588 
589  //
590  // misc
591  //
592  irep_idt get_string_constant(const exprt &expr);
593  bool get_string_constant(const exprt &expr, irep_idt &);
594  exprt get_constant(const exprt &expr);
595 
596  // some built-in functions
597  void do_atomic_begin(
598  const exprt &lhs,
599  const symbol_exprt &function,
600  const exprt::operandst &arguments,
601  goto_programt &dest);
602  void do_atomic_end(
603  const exprt &lhs,
604  const symbol_exprt &function,
605  const exprt::operandst &arguments,
606  goto_programt &dest);
607  void do_create_thread(
608  const exprt &lhs,
609  const symbol_exprt &function,
610  const exprt::operandst &arguments,
611  goto_programt &dest);
612  void do_array_equal(
613  const exprt &lhs,
614  const symbol_exprt &rhs,
615  const exprt::operandst &arguments,
616  goto_programt &dest);
617  void do_array_op(
618  const irep_idt &id,
619  const exprt &lhs,
620  const symbol_exprt &function,
621  const exprt::operandst &arguments,
622  goto_programt &dest);
623  void do_printf(
624  const exprt &lhs,
625  const symbol_exprt &function,
626  const exprt::operandst &arguments,
627  goto_programt &dest);
628  void do_scanf(
629  const exprt &lhs,
630  const symbol_exprt &function,
631  const exprt::operandst &arguments,
632  goto_programt &dest);
633  void do_input(
634  const exprt &rhs,
635  const exprt::operandst &arguments,
636  goto_programt &dest);
637  void do_output(
638  const exprt &rhs,
639  const exprt::operandst &arguments,
640  goto_programt &dest);
641  void do_prob_coin(
642  const exprt &lhs,
643  const symbol_exprt &function,
644  const exprt::operandst &arguments,
645  goto_programt &dest);
646  void do_prob_uniform(
647  const exprt &lhs,
648  const symbol_exprt &function,
649  const exprt::operandst &arguments,
650  goto_programt &dest);
651 
652  exprt get_array_argument(const exprt &src);
653 };
654 
655 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
goto_convertt::labelst
std::map< irep_idt, std::pair< goto_programt::targett, destructor_stackt > > labelst
Definition: goto_convert_class.h:361
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
goto_convertt::exception_flag
symbol_exprt exception_flag()
Definition: goto_convert_exceptions.cpp:247
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:35
goto_convertt::convert_dowhile
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1072
goto_convertt::remove_function_call
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:334
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
goto_convertt::break_switch_targetst::cases
casest cases
Definition: goto_convert_class.h:499
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:407
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
goto_convertt::targetst::set_break
void set_break(goto_programt::targett _break_target)
Definition: goto_convert_class.h:403
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:64
goto_convertt::do_output
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:340
goto_convertt::break_switch_targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:495
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:1723
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:48
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:767
goto_convertt::targetst::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:383
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:399
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1459
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:425
code_fort
codet representation of a for statement.
Definition: std_code.h:893
goto_convertt::leave_targett::leave_set
bool leave_set
Definition: goto_convert_class.h:543
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:291
goto_convertt::targetst::default_set
bool default_set
Definition: goto_convert_class.h:372
typet
The type of an expression, extends irept.
Definition: type.h:27
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:160
goto_convertt::get_array_argument
exprt get_array_argument(const exprt &src)
Definition: builtin_functions.cpp:553
goto_convertt::goto_convert_rec
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:278
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:526
goto_convertt::has_function_call
static bool has_function_call(const exprt &expr)
Definition: goto_convert_side_effect.cpp:23
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:494
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
goto_convertt::convert_skip
void convert_skip(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:866
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:383
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:224
goto_convertt::cases_mapt
std::map< goto_programt::targett, casest::iterator > cases_mapt
Definition: goto_convert_class.h:367
goto_convertt::convert_assert
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:850
goto_convertt::~goto_convertt
virtual ~goto_convertt()
Definition: goto_convert_class.h:42
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:49
goto_convertt::convert_try_catch
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:91
goto_convertt::finish_gotos
void finish_gotos(goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:105
goto_convertt::targetst::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:383
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:548
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:1453
goto_convertt::remove_pre
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:146
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:1523
goto_convertt::convert_assume
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:875
goto_convertt::leave_targett
Definition: goto_convert_class.h:525
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:539
goto_convertt::targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:380
goto_convertt::targetst::destructor_stack
destructor_stackt destructor_stack
Definition: goto_convert_class.h:377
code_continuet
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1430
goto_convertt::break_switch_targetst::default_set
bool default_set
Definition: goto_convert_class.h:496
irep_idt
dstringt irep_idt
Definition: irep.h:32
goto_convertt::destructor_stackt
std::vector< codet > destructor_stackt
Definition: goto_convert_class.h:336
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:429
goto_convertt::remove_side_effect
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Definition: goto_convert_side_effect.cpp:603
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
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:1976
goto_convertt::break_continue_targetst::break_continue_targetst
break_continue_targetst(const targetst &targets)
Definition: goto_convert_class.h:448
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:347
goto_convertt::targetst::throw_set
bool throw_set
Definition: goto_convert_class.h:372
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
goto_convertt::convert_gcc_switch_case_range
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:379
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:1887
goto_convertt::goto_convert
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:270
goto_convertt::leave_targett::leave_targett
leave_targett(const targetst &targets)
Definition: goto_convert_class.h:529
goto_convertt::throw_targett
Definition: goto_convert_class.h:503
goto_convertt::targetst::set_leave
void set_leave(goto_programt::targett _leave_target)
Definition: goto_convert_class.h:436
goto_convertt::targetst::leave_set
bool leave_set
Definition: goto_convert_class.h:372
goto_convertt::targetst::has_return_value
bool has_return_value
Definition: goto_convert_class.h:371
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
guard.h
goto_convertt::targetst::labels
labelst labels
Definition: goto_convert_class.h:374
goto_convertt::convert_break
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1278
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
goto_convertt::targetst::gotos
gotost gotos
Definition: goto_convert_class.h:375
goto_convertt::break_switch_targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:500
goto_convertt::convert_init
void convert_init(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:771
goto_convertt::targetst::continue_stack_size
std::size_t continue_stack_size
Definition: goto_convert_class.h:385
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:829
goto_convertt::break_switch_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:484
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:568
goto_convertt::break_switch_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:494
goto_convertt::convert_continue
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1359
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:219
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:152
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1400
goto_convertt
Definition: goto_convert_class.h:26
goto_convertt::break_continue_targetst::break_set
bool break_set
Definition: goto_convert_class.h:466
goto_convertt::get_string_constant
irep_idt get_string_constant(const exprt &expr)
Definition: goto_convert.cpp:1847
goto_convertt::rewrite_boolean
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
Definition: goto_clean_expr.cpp:109
code_gotot
codet representation of a goto statement.
Definition: std_code.h:983
goto_convertt::targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:382
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1256
goto_convertt::convert_CPROVER_throw
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:186
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:160
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:228
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
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:496
goto_convertt::break_continue_targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:465
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:631
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:453
goto_convertt::targetst::set_return
void set_return(goto_programt::targett _return_target)
Definition: goto_convert_class.h:423
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:23
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:410
goto_convertt::convert_goto
void convert_goto(const code_gotot &code, goto_programt &dest)
Definition: goto_convert.cpp:1379
goto_convertt::targetst::return_set
bool return_set
Definition: goto_convert_class.h:371
message_handlert
Definition: message.h:24
goto_convertt::targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:371
goto_convertt::break_continue_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:456
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
goto_convertt::targetst::break_set
bool break_set
Definition: goto_convert_class.h:371
goto_convertt::convert_for
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:912
goto_convertt::targetst::set_throw
void set_throw(goto_programt::targett _throw_target)
Definition: goto_convert_class.h:429
goto_convertt::remove_cpp_delete
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:437
goto_convertt::caset
exprt::operandst caset
Definition: goto_convert_class.h:365
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:231
goto_convertt::get_constant
exprt get_constant(const exprt &expr)
Definition: goto_convert.cpp:1861
goto_convertt::goto_convertt
goto_convertt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: goto_convert_class.h:32
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:605
std_code.h
goto_convertt::targetst::throw_stack_size
std::size_t throw_stack_size
Definition: goto_convert_class.h:385
goto_convertt::convert_while
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1011
goto_convertt::convert_assign
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:671
goto_convertt::targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:383
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:196
goto_program.h
goto_convertt::collect_operands
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
Definition: goto_convert.cpp:1496
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:31
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:96
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:489
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:193
goto_convertt::do_input
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:321
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:184
goto_convertt::targetst
Definition: goto_convert_class.h:369
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:359
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
goto_convertt::break_switch_targetst::break_switch_targetst
break_switch_targetst(const targetst &targets)
Definition: goto_convert_class.h:473
goto_convertt::convert_msc_leave
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:68
goto_convertt::throw_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:514
goto_convertt::case_guard
exprt case_guard(const exprt &value, const caset &case_op)
Definition: goto_convert.cpp:1143
goto_convertt::convert_gcc_local_label
void convert_gcc_local_label(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:340
goto_convertt::convert_return
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1296
goto_convertt::remove_assignment
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
Definition: goto_convert_side_effect.cpp:36
code_switcht
codet representing a switch statement.
Definition: std_code.h:705
stack
#define stack(x)
Definition: parser.h:144
symbolt
Symbol table entry.
Definition: symbol.h:27
goto_convertt::convert_start_thread
void convert_start_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1403
goto_convertt::targetst::cases
casest cases
Definition: goto_convert_class.h:379
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:53
goto_convertt::break_switch_targetst::break_set
bool break_set
Definition: goto_convert_class.h:496
goto_convertt::convert_loop_invariant
void convert_loop_invariant(const codet &code, goto_programt::targett loop, const irep_idt &mode)
Definition: goto_convert.cpp:889
goto_convertt::throw_targett::throw_stack_size
std::size_t throw_stack_size
Definition: goto_convert_class.h:522
goto_convertt::computed_gotost
std::list< goto_programt::targett > computed_gotost
Definition: goto_convert_class.h:364
goto_convertt::throw_targett::throw_set
bool throw_set
Definition: goto_convert_class.h:521
goto_convertt::targetst::set_continue
void set_continue(goto_programt::targett _continue_target)
Definition: goto_convert_class.h:410
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_convertt::unwind_destructor_stack
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:269
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:589
goto_convertt::break_switch_targetst::break_stack_size
std::size_t break_stack_size
Definition: goto_convert_class.h:497
goto_convertt::gotost
std::list< std::pair< goto_programt::targett, destructor_stackt > > gotost
Definition: goto_convert_class.h:363
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:47
goto_convertt::break_continue_targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:466
goto_convertt::leave_targett::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:542
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:788
replace_expr.h
goto_convertt::targetst::leave_stack_size
std::size_t leave_stack_size
Definition: goto_convert_class.h:386
goto_convertt::convert_atomic_end
void convert_atomic_end(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1441
goto_convertt::targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:382
goto_convertt::break_switch_targetst
Definition: goto_convert_class.h:469
goto_convertt::throw_targett::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:520
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
goto_convertt::convert_label
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:301
message.h
goto_convertt::leave_targett::leave_stack_size
std::size_t leave_stack_size
Definition: goto_convert_class.h:544
goto_convertt::break_continue_targetst
Definition: goto_convert_class.h:444
goto_convertt::targetst::set_default
void set_default(goto_programt::targett _default_target)
Definition: goto_convert_class.h:417
goto_convertt::leave_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:536
goto_convertt::throw_targett::throw_targett
throw_targett(const targetst &targets)
Definition: goto_convert_class.h:507
goto_convertt::casest
std::list< std::pair< goto_programt::targett, caset > > casest
Definition: goto_convert_class.h:366
goto_convertt::targetst::targetst
targetst()
Definition: goto_convert_class.h:388
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
goto_convertt::convert_atomic_begin
void convert_atomic_begin(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1429
goto_convertt::convert_decl_type
void convert_decl_type(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:664
goto_convertt::targetst::computed_gotos
computed_gotost computed_gotos
Definition: goto_convert_class.h:376
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:30
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:108
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1504
goto_convertt::targetst::break_stack_size
std::size_t break_stack_size
Definition: goto_convert_class.h:385
goto_convertt::convert_switch
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1171
goto_convertt::break_continue_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:464
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
goto_convertt::targetst::return_target
goto_programt::targett return_target
Definition: goto_convert_class.h:382
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:1910
goto_convertt::convert_end_thread
void convert_end_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1417
goto_convertt::convert_gcc_computed_goto
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1390