cprover
goto_convert_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
14 
15 #include <list>
16 #include <vector>
17 #include <unordered_set>
18 
19 #include <util/allocate_objects.h>
20 #include <util/message.h>
21 #include <util/namespace.h>
22 #include <util/replace_expr.h>
23 #include <util/std_code.h>
24 
25 #include "goto_program.h"
26 #include "destructor_tree.h"
27 
28 class goto_convertt:public messaget
29 {
30 public:
31  void
32  goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
33 
35  symbol_table_baset &_symbol_table,
36  message_handlert &_message_handler):
37  messaget(_message_handler),
38  symbol_table(_symbol_table),
39  ns(_symbol_table),
40  tmp_symbol_prefix("goto_convertt")
41  {
42  }
43 
44  virtual ~goto_convertt()
45  {
46  }
47 
48 protected:
51  std::string tmp_symbol_prefix;
53 
54  void goto_convert_rec(
55  const codet &code,
56  goto_programt &dest,
57  const irep_idt &mode);
58 
59  //
60  // tools for symbols
61  //
63  const typet &type,
64  const std::string &suffix,
65  goto_programt &dest,
66  const source_locationt &,
67  const irep_idt &mode);
68 
70  const exprt &expr,
71  goto_programt &dest,
72  const irep_idt &mode);
73 
74  //
75  // translation of C expressions (with side effects)
76  // into the program logic
77  //
78 
79  void clean_expr(
80  exprt &expr,
81  goto_programt &dest,
82  const irep_idt &mode,
83  bool result_is_used = true);
84 
85  void
86  clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode);
87 
88  static bool needs_cleaning(const exprt &expr);
89 
90  void make_temp_symbol(
91  exprt &expr,
92  const std::string &suffix,
93  goto_programt &,
94  const irep_idt &mode);
95 
96  void rewrite_boolean(exprt &dest);
97 
98  static bool has_sideeffect(const exprt &expr);
99  static bool has_function_call(const exprt &expr);
100 
101  void remove_side_effect(
102  side_effect_exprt &expr,
103  goto_programt &dest,
104  const irep_idt &mode,
105  bool result_is_used);
106  void remove_assignment(
107  side_effect_exprt &expr,
108  goto_programt &dest,
109  bool result_is_used,
110  const irep_idt &mode);
111  void remove_pre(
112  side_effect_exprt &expr,
113  goto_programt &dest,
114  bool result_is_used,
115  const irep_idt &mode);
116  void remove_post(
117  side_effect_exprt &expr,
118  goto_programt &dest,
119  const irep_idt &mode,
120  bool result_is_used);
123  goto_programt &dest,
124  const irep_idt &mode,
125  bool result_is_used);
126  void remove_cpp_new(
127  side_effect_exprt &expr,
128  goto_programt &dest,
129  bool result_is_used);
130  void remove_cpp_delete(
131  side_effect_exprt &expr,
132  goto_programt &dest);
133  void remove_malloc(
134  side_effect_exprt &expr,
135  goto_programt &dest,
136  const irep_idt &mode,
137  bool result_is_used);
139  side_effect_exprt &expr,
140  goto_programt &dest);
142  side_effect_exprt &expr,
143  goto_programt &dest,
144  const irep_idt &mode,
145  bool result_is_used);
147  exprt &expr,
148  goto_programt &dest,
149  const irep_idt &mode);
150 
151  virtual void do_cpp_new(
152  const exprt &lhs,
153  const side_effect_exprt &rhs,
154  goto_programt &dest);
155 
157  const exprt &lhs,
158  const side_effect_exprt &rhs,
159  goto_programt &dest);
160 
162  const exprt &lhs,
163  const side_effect_exprt &rhs,
164  goto_programt &dest);
165 
166  static void replace_new_object(
167  const exprt &object,
168  exprt &dest);
169 
170  void cpp_new_initializer(
171  const exprt &lhs,
172  const side_effect_exprt &rhs,
173  goto_programt &dest);
174 
175  //
176  // function calls
177  //
178 
179  virtual void do_function_call(
180  const exprt &lhs,
181  const exprt &function,
182  const exprt::operandst &arguments,
183  goto_programt &dest,
184  const irep_idt &mode);
185 
186  virtual void do_function_call_if(
187  const exprt &lhs,
188  const if_exprt &function,
189  const exprt::operandst &arguments,
190  goto_programt &dest,
191  const irep_idt &mode);
192 
193  virtual void do_function_call_symbol(
194  const exprt &lhs,
195  const symbol_exprt &function,
196  const exprt::operandst &arguments,
197  goto_programt &dest);
198 
199  virtual void do_function_call_symbol(const symbolt &)
200  {
201  }
202 
203  virtual void do_function_call_other(
204  const exprt &lhs,
205  const exprt &function,
206  const exprt::operandst &arguments,
207  goto_programt &dest);
208 
209  //
210  // conversion
211  //
212  void convert_block(
213  const code_blockt &code,
214  goto_programt &dest,
215  const irep_idt &mode);
216  void convert_decl(
217  const code_declt &code,
218  goto_programt &dest,
219  const irep_idt &mode);
220  void convert_decl_type(const codet &code, goto_programt &dest);
221  void convert_expression(
222  const code_expressiont &code,
223  goto_programt &dest,
224  const irep_idt &mode);
225  void convert_assign(
226  const code_assignt &code,
227  goto_programt &dest,
228  const irep_idt &mode);
229  void convert_cpp_delete(const codet &code, goto_programt &dest);
231  const codet &code,
233  const irep_idt &mode);
234  void
235  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
236  void convert_while(
237  const code_whilet &code,
238  goto_programt &dest,
239  const irep_idt &mode);
240  void convert_dowhile(
241  const code_dowhilet &code,
242  goto_programt &dest,
243  const irep_idt &mode);
244  void convert_assume(
245  const code_assumet &code,
246  goto_programt &dest,
247  const irep_idt &mode);
248  void convert_assert(
249  const code_assertt &code,
250  goto_programt &dest,
251  const irep_idt &mode);
252  void convert_switch(
253  const code_switcht &code,
254  goto_programt &dest,
255  const irep_idt &mode);
256  void convert_break(
257  const code_breakt &code,
258  goto_programt &dest,
259  const irep_idt &mode);
260  void convert_return(
261  const code_returnt &code,
262  goto_programt &dest,
263  const irep_idt &mode);
264  void convert_continue(
265  const code_continuet &code,
266  goto_programt &dest,
267  const irep_idt &mode);
268  void convert_ifthenelse(
269  const code_ifthenelset &code,
270  goto_programt &dest,
271  const irep_idt &mode);
272  void convert_goto(const code_gotot &code, goto_programt &dest);
273  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
274  void convert_skip(const codet &code, goto_programt &dest);
275  void convert_label(
276  const code_labelt &code,
277  goto_programt &dest,
278  const irep_idt &mode);
279  void convert_gcc_local_label(const codet &code, goto_programt &dest);
280  void convert_switch_case(
281  const code_switch_caset &code,
282  goto_programt &dest,
283  const irep_idt &mode);
286  goto_programt &dest,
287  const irep_idt &mode);
289  const code_function_callt &code,
290  goto_programt &dest,
291  const irep_idt &mode);
292  void convert_start_thread(const codet &code, goto_programt &dest);
293  void convert_end_thread(const codet &code, goto_programt &dest);
294  void convert_atomic_begin(const codet &code, goto_programt &dest);
295  void convert_atomic_end(const codet &code, goto_programt &dest);
297  const codet &code,
298  goto_programt &dest,
299  const irep_idt &mode);
301  const codet &code,
302  goto_programt &dest,
303  const irep_idt &mode);
304  void convert_msc_leave(
305  const codet &code,
306  goto_programt &dest,
307  const irep_idt &mode);
308  void convert_try_catch(
309  const codet &code,
310  goto_programt &dest,
311  const irep_idt &mode);
313  const codet &code,
314  goto_programt &dest,
315  const irep_idt &mode);
317  const codet &code,
318  goto_programt &dest,
319  const irep_idt &mode);
321  const codet &code,
322  goto_programt &dest,
323  const irep_idt &mode);
324  void convert_asm(const code_asmt &code, goto_programt &dest);
325 
326  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
327 
328  void copy(
329  const codet &code,
331  goto_programt &dest);
332 
333  //
334  // exceptions
335  //
336 
337  symbol_exprt exception_flag(const irep_idt &mode);
338 
340  const source_locationt &source_location,
341  goto_programt &dest,
342  const irep_idt &mode,
343  optionalt<node_indext> destructor_start_point = {},
344  optionalt<node_indext> destructor_end_point = {});
345 
346  //
347  // gotos
348  //
349 
350  void finish_gotos(goto_programt &dest, const irep_idt &mode);
353 
354  typedef std::map<irep_idt,
355  std::pair<goto_programt::targett, node_indext>>
357  typedef std::list<std::pair<goto_programt::targett, node_indext>>
359  typedef std::list<goto_programt::targett> computed_gotost;
361  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
362  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
363 
364  struct targetst
365  {
368 
373 
376 
379 
382 
384  return_set(false),
385  has_return_value(false),
386  break_set(false),
387  continue_set(false),
388  default_set(false),
389  throw_set(false),
390  leave_set(false),
395  {
396  }
397 
398  void set_break(goto_programt::targett _break_target)
399  {
400  break_set=true;
401  break_target=_break_target;
403  }
404 
405  void set_continue(goto_programt::targett _continue_target)
406  {
407  continue_set=true;
408  continue_target=_continue_target;
410  }
411 
412  void set_default(goto_programt::targett _default_target)
413  {
414  default_set=true;
415  default_target=_default_target;
416  }
417 
418  void set_return(goto_programt::targett _return_target)
419  {
420  return_set=true;
421  return_target=_return_target;
422  }
423 
424  void set_throw(goto_programt::targett _throw_target)
425  {
426  throw_set=true;
427  throw_target=_throw_target;
429  }
430 
431  void set_leave(goto_programt::targett _leave_target)
432  {
433  leave_set=true;
434  leave_target=_leave_target;
436  }
438 
440  {
441  // for 'while', 'for', 'dowhile'
442 
444  {
449  }
450 
452  {
457  }
458 
462  };
463 
465  {
466  // for 'switch'
467 
469  {
477  }
478 
480  {
487  }
488 
493 
496  };
497 
499  {
500  // for 'try...catch' and the like
501 
502  explicit throw_targett(const targetst &targets)
503  {
507  }
508 
510  {
513  }
514 
516  bool throw_set;
518  };
519 
521  {
522  // for 'try...leave...finally'
523 
524  explicit leave_targett(const targetst &targets)
525  {
529  }
530 
532  {
535  }
536 
538  bool leave_set;
540  };
541 
543  const exprt &value,
544  const caset &case_op);
545 
546  // if(cond) { true_case } else { false_case }
547  void generate_ifthenelse(
548  const exprt &cond,
549  goto_programt &true_case,
550  goto_programt &false_case,
551  const source_locationt &,
552  goto_programt &dest,
553  const irep_idt &mode);
554 
555  // if(guard) goto target_true; else goto target_false;
557  const exprt &guard,
558  goto_programt::targett target_true,
559  goto_programt::targett target_false,
560  const source_locationt &,
561  goto_programt &dest,
562  const irep_idt &mode);
563 
564  // if(guard) goto target;
566  const exprt &guard,
567  goto_programt::targett target_true,
568  const source_locationt &,
569  goto_programt &dest,
570  const irep_idt &mode);
571 
572  // turn a OP b OP c into a list a, b, c
573  static void collect_operands(
574  const exprt &expr,
575  const irep_idt &id,
576  std::list<exprt> &dest);
577 
578  // START_THREAD; ... END_THREAD;
580  const code_blockt &thread_body,
581  goto_programt &dest,
582  const irep_idt &mode);
583 
584  //
585  // misc
586  //
587  irep_idt get_string_constant(const exprt &expr);
588  bool get_string_constant(const exprt &expr, irep_idt &);
589  exprt get_constant(const exprt &expr);
590 
591  // some built-in functions
592  void do_atomic_begin(
593  const exprt &lhs,
594  const symbol_exprt &function,
595  const exprt::operandst &arguments,
596  goto_programt &dest);
597  void do_atomic_end(
598  const exprt &lhs,
599  const symbol_exprt &function,
600  const exprt::operandst &arguments,
601  goto_programt &dest);
603  const exprt &lhs,
604  const symbol_exprt &function,
605  const exprt::operandst &arguments,
606  goto_programt &dest);
608  const exprt &lhs,
609  const symbol_exprt &rhs,
610  const exprt::operandst &arguments,
611  goto_programt &dest);
612  void do_array_op(
613  const irep_idt &id,
614  const exprt &lhs,
615  const symbol_exprt &function,
616  const exprt::operandst &arguments,
617  goto_programt &dest);
618  void do_printf(
619  const exprt &lhs,
620  const symbol_exprt &function,
621  const exprt::operandst &arguments,
622  goto_programt &dest);
623  void do_scanf(
624  const exprt &lhs,
625  const symbol_exprt &function,
626  const exprt::operandst &arguments,
627  goto_programt &dest);
628  void do_input(
629  const exprt &rhs,
630  const exprt::operandst &arguments,
631  goto_programt &dest);
632  void do_output(
633  const exprt &rhs,
634  const exprt::operandst &arguments,
635  goto_programt &dest);
636  void do_prob_coin(
637  const exprt &lhs,
638  const symbol_exprt &function,
639  const exprt::operandst &arguments,
640  goto_programt &dest);
641  void do_prob_uniform(
642  const exprt &lhs,
643  const symbol_exprt &function,
644  const exprt::operandst &arguments,
645  goto_programt &dest);
646 
647  exprt get_array_argument(const exprt &src);
648 };
649 
650 #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:1023
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:494
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:1439
goto_convertt::targetst::set_break
void set_break(goto_programt::targett _break_target)
Definition: goto_convert_class.h:398
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:65
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:490
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:1641
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:50
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:896
goto_convertt::targetst::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:378
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:347
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1669
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:426
code_fort
codet representation of a for statement.
Definition: std_code.h:1020
goto_convertt::leave_targett::leave_set
bool leave_set
Definition: goto_convert_class.h:538
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:296
goto_convertt::targetst::default_set
bool default_set
Definition: goto_convert_class.h:367
typet
The type of an expression, extends irept.
Definition: type.h:29
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:161
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:283
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:24
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2117
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:2964
goto_convertt::convert_skip
void convert_skip(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:832
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:362
goto_convertt::convert_assert
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:817
goto_convertt::~goto_convertt
virtual ~goto_convertt()
Definition: goto_convert_class.h:44
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:51
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:106
goto_convertt::targetst::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:378
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:587
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:1377
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:139
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:1450
goto_convertt::convert_assume
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:840
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:292
goto_convertt::leave_targett
Definition: goto_convert_class.h:521
exprt
Base class for all expressions.
Definition: expr.h:53
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:375
code_continuet
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1634
goto_convertt::break_switch_targetst::default_set
bool default_set
Definition: goto_convert_class.h:491
irep_idt
dstringt irep_idt
Definition: irep.h:32
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1513
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
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:539
node_indext
std::size_t node_indext
Definition: destructor_tree.h:15
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:1891
goto_convertt::break_continue_targetst::break_continue_targetst
break_continue_targetst(const targetst &targets)
Definition: goto_convert_class.h:443
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:353
goto_convertt::targetst::throw_set
bool throw_set
Definition: goto_convert_class.h:367
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
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:1802
goto_convertt::goto_convert
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:275
goto_convertt::leave_targett::leave_targett
leave_targett(const targetst &targets)
Definition: goto_convert_class.h:524
goto_convertt::throw_targett
Definition: goto_convert_class.h:499
goto_convertt::targetst::set_leave
void set_leave(goto_programt::targett _leave_target)
Definition: goto_convert_class.h:431
goto_convertt::targetst::leave_set
bool leave_set
Definition: goto_convert_class.h:367
goto_convertt::targetst::has_return_value
bool has_return_value
Definition: goto_convert_class.h:366
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:369
goto_convertt::convert_break
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1212
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
goto_convertt::targetst::gotos
gotost gotos
Definition: goto_convert_class.h:370
goto_convertt::break_switch_targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:495
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:958
goto_convertt::break_switch_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:479
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:569
goto_convertt::break_switch_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:489
goto_convertt::leave_targett::leave_stack_node
node_indext leave_stack_node
Definition: goto_convert_class.h:539
goto_convertt::convert_continue
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1288
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:1598
goto_convertt
Definition: goto_convert_class.h:29
goto_convertt::break_continue_targetst::break_set
bool break_set
Definition: goto_convert_class.h:461
goto_convertt::get_string_constant
irep_idt get_string_constant(const exprt &expr)
Definition: goto_convert.cpp:1762
goto_convertt::targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:380
goto_convertt::rewrite_boolean
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
Definition: goto_clean_expr.cpp:110
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1127
goto_convertt::targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:377
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1375
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:159
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:231
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:535
goto_convertt::break_continue_targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:460
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:470
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:615
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:401
goto_convertt::targetst::set_return
void set_return(goto_programt::targett _return_target)
Definition: goto_convert_class.h:418
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
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:358
goto_convertt::convert_goto
void convert_goto(const code_gotot &code, goto_programt &dest)
Definition: goto_convert.cpp:1307
goto_convertt::break_switch_targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:492
goto_convertt::targetst::return_set
bool return_set
Definition: goto_convert_class.h:366
message_handlert
Definition: message.h:28
goto_convertt::targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:366
goto_convertt::break_continue_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:451
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
goto_convertt::targetst::break_set
bool break_set
Definition: goto_convert_class.h:366
goto_convertt::convert_for
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:875
goto_convertt::targetst::set_throw
void set_throw(goto_programt::targett _throw_target)
Definition: goto_convert_class.h:424
goto_convertt::remove_cpp_delete
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:385
goto_convertt::caset
exprt::operandst caset
Definition: goto_convert_class.h:360
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:211
goto_convertt::get_constant
exprt get_constant(const exprt &expr)
Definition: goto_convert.cpp:1776
goto_convertt::goto_convertt
goto_convertt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: goto_convert_class.h:34
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:606
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:967
goto_convertt::convert_assign
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:672
goto_convertt::targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:378
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:199
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:1423
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:32
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
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:434
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:199
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:365
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:1310
goto_convertt::break_switch_targetst::break_switch_targetst
break_switch_targetst(const targetst &targets)
Definition: goto_convert_class.h:468
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:509
goto_convertt::targetst::destructor_stack
destructor_treet destructor_stack
Definition: goto_convert_class.h:372
goto_convertt::case_guard
exprt case_guard(const exprt &value, const caset &case_op)
Definition: goto_convert.cpp:1092
goto_convertt::convert_gcc_local_label
void convert_gcc_local_label(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:346
goto_convertt::convert_return
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1229
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:37
code_switcht
codet representing a switch statement.
Definition: std_code.h:834
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:1329
goto_convertt::targetst::cases
casest cases
Definition: goto_convert_class.h:374
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:491
goto_convertt::gotost
std::list< std::pair< goto_programt::targett, node_indext > > gotost
Definition: goto_convert_class.h:358
goto_convertt::convert_loop_invariant
void convert_loop_invariant(const codet &code, goto_programt::targett loop, const irep_idt &mode)
Definition: goto_convert.cpp:852
goto_convertt::computed_gotost
std::list< goto_programt::targett > computed_gotost
Definition: goto_convert_class.h:359
goto_convertt::throw_targett::throw_set
bool throw_set
Definition: goto_convert_class.h:516
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
lifetimet::STATIC_GLOBAL
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
goto_convertt::targetst::set_continue
void set_continue(goto_programt::targett _continue_target)
Definition: goto_convert_class.h:405
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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::labelst
std::map< irep_idt, std::pair< goto_programt::targett, node_indext > > labelst
Definition: goto_convert_class.h:356
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:49
goto_convertt::break_continue_targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:461
goto_convertt::leave_targett::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:537
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:755
replace_expr.h
goto_convertt::convert_atomic_end
void convert_atomic_end(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1365
goto_convertt::targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:377
goto_convertt::break_switch_targetst
Definition: goto_convert_class.h:465
goto_convertt::throw_targett::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:515
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:305
message.h
goto_convertt::targetst::leave_stack_node
node_indext leave_stack_node
Definition: goto_convert_class.h:381
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:385
goto_convertt::lifetime
lifetimet lifetime
Definition: goto_convert_class.h:52
goto_convertt::break_continue_targetst
Definition: goto_convert_class.h:440
goto_convertt::targetst::set_default
void set_default(goto_programt::targett _default_target)
Definition: goto_convert_class.h:412
allocate_objects.h
goto_convertt::targetst::continue_stack_node
node_indext continue_stack_node
Definition: goto_convert_class.h:380
goto_convertt::throw_targett::throw_stack_node
node_indext throw_stack_node
Definition: goto_convert_class.h:517
goto_convertt::leave_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:531
goto_convertt::throw_targett::throw_targett
throw_targett(const targetst &targets)
Definition: goto_convert_class.h:502
goto_convertt::casest
std::list< std::pair< goto_programt::targett, caset > > casest
Definition: goto_convert_class.h:361
goto_convertt::targetst::targetst
targetst()
Definition: goto_convert_class.h:383
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
goto_convertt::convert_atomic_begin
void convert_atomic_begin(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1353
goto_convertt::convert_decl_type
void convert_decl_type(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:665
goto_convertt::targetst::computed_gotos
computed_gotost computed_gotos
Definition: goto_convert_class.h:371
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:380
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
goto_convertt::convert_switch
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1112
goto_convertt::break_continue_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:459
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:377
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:1825
goto_convertt::convert_end_thread
void convert_end_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1341
goto_convertt::convert_gcc_computed_goto
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1317