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_function_call(const exprt &expr);
101 
102  void remove_side_effect(
103  side_effect_exprt &expr,
104  goto_programt &dest,
105  const irep_idt &mode,
106  bool result_is_used,
107  bool address_taken);
108  void remove_assignment(
109  side_effect_exprt &expr,
110  goto_programt &dest,
111  bool result_is_used,
112  bool address_taken,
113  const irep_idt &mode);
114  void remove_pre(
115  side_effect_exprt &expr,
116  goto_programt &dest,
117  bool result_is_used,
118  bool address_taken,
119  const irep_idt &mode);
120  void remove_post(
121  side_effect_exprt &expr,
122  goto_programt &dest,
123  const irep_idt &mode,
124  bool result_is_used);
127  goto_programt &dest,
128  const irep_idt &mode,
129  bool result_is_used);
130  void remove_cpp_new(
131  side_effect_exprt &expr,
132  goto_programt &dest,
133  bool result_is_used);
134  void remove_cpp_delete(
135  side_effect_exprt &expr,
136  goto_programt &dest);
137  void remove_malloc(
138  side_effect_exprt &expr,
139  goto_programt &dest,
140  const irep_idt &mode,
141  bool result_is_used);
143  side_effect_exprt &expr,
144  goto_programt &dest);
146  side_effect_exprt &expr,
147  goto_programt &dest,
148  const irep_idt &mode,
149  bool result_is_used);
151  exprt &expr,
152  goto_programt &dest,
153  const irep_idt &mode);
154  void remove_overflow(
156  goto_programt &dest,
157  bool result_is_used,
158  const irep_idt &mode);
159 
160  virtual void do_cpp_new(
161  const exprt &lhs,
162  const side_effect_exprt &rhs,
163  goto_programt &dest);
164 
166  const exprt &lhs,
167  const side_effect_exprt &rhs,
168  goto_programt &dest);
169 
171  const exprt &lhs,
172  const side_effect_exprt &rhs,
173  goto_programt &dest);
174 
175  static void replace_new_object(
176  const exprt &object,
177  exprt &dest);
178 
179  void cpp_new_initializer(
180  const exprt &lhs,
181  const side_effect_exprt &rhs,
182  goto_programt &dest);
183 
184  //
185  // function calls
186  //
187 
188  virtual void do_function_call(
189  const exprt &lhs,
190  const exprt &function,
191  const exprt::operandst &arguments,
192  goto_programt &dest,
193  const irep_idt &mode);
194 
195  virtual void do_function_call_if(
196  const exprt &lhs,
197  const if_exprt &function,
198  const exprt::operandst &arguments,
199  goto_programt &dest,
200  const irep_idt &mode);
201 
202  virtual void do_function_call_symbol(
203  const exprt &lhs,
204  const symbol_exprt &function,
205  const exprt::operandst &arguments,
206  goto_programt &dest);
207 
208  virtual void do_function_call_symbol(const symbolt &)
209  {
210  }
211 
212  virtual void do_function_call_other(
213  const exprt &lhs,
214  const exprt &function,
215  const exprt::operandst &arguments,
216  goto_programt &dest);
217 
218  //
219  // conversion
220  //
221  void convert_block(
222  const code_blockt &code,
223  goto_programt &dest,
224  const irep_idt &mode);
225  void convert_decl(
226  const code_declt &code,
227  goto_programt &dest,
228  const irep_idt &mode);
229  void convert_decl_type(const codet &code, goto_programt &dest);
230  void convert_expression(
231  const code_expressiont &code,
232  goto_programt &dest,
233  const irep_idt &mode);
234  void convert_assign(
235  const code_assignt &code,
236  goto_programt &dest,
237  const irep_idt &mode);
238  void convert_cpp_delete(const codet &code, goto_programt &dest);
240  const codet &code,
242  const irep_idt &mode);
243  void
244  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
245  void convert_while(
246  const code_whilet &code,
247  goto_programt &dest,
248  const irep_idt &mode);
249  void convert_dowhile(
250  const code_dowhilet &code,
251  goto_programt &dest,
252  const irep_idt &mode);
253  void convert_assume(
254  const code_assumet &code,
255  goto_programt &dest,
256  const irep_idt &mode);
257  void convert_assert(
258  const code_assertt &code,
259  goto_programt &dest,
260  const irep_idt &mode);
261  void convert_switch(
262  const code_switcht &code,
263  goto_programt &dest,
264  const irep_idt &mode);
265  void convert_break(
266  const code_breakt &code,
267  goto_programt &dest,
268  const irep_idt &mode);
269  void convert_return(
270  const code_returnt &code,
271  goto_programt &dest,
272  const irep_idt &mode);
273  void convert_continue(
274  const code_continuet &code,
275  goto_programt &dest,
276  const irep_idt &mode);
277  void convert_ifthenelse(
278  const code_ifthenelset &code,
279  goto_programt &dest,
280  const irep_idt &mode);
281  void convert_goto(const code_gotot &code, goto_programt &dest);
282  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
283  void convert_skip(const codet &code, goto_programt &dest);
284  void convert_label(
285  const code_labelt &code,
286  goto_programt &dest,
287  const irep_idt &mode);
288  void convert_gcc_local_label(const codet &code, goto_programt &dest);
289  void convert_switch_case(
290  const code_switch_caset &code,
291  goto_programt &dest,
292  const irep_idt &mode);
295  goto_programt &dest,
296  const irep_idt &mode);
298  const code_function_callt &code,
299  goto_programt &dest,
300  const irep_idt &mode);
301  void convert_start_thread(const codet &code, goto_programt &dest);
302  void convert_end_thread(const codet &code, goto_programt &dest);
303  void convert_atomic_begin(const codet &code, goto_programt &dest);
304  void convert_atomic_end(const codet &code, goto_programt &dest);
306  const codet &code,
307  goto_programt &dest,
308  const irep_idt &mode);
310  const codet &code,
311  goto_programt &dest,
312  const irep_idt &mode);
313  void convert_msc_leave(
314  const codet &code,
315  goto_programt &dest,
316  const irep_idt &mode);
317  void convert_try_catch(
318  const codet &code,
319  goto_programt &dest,
320  const irep_idt &mode);
322  const codet &code,
323  goto_programt &dest,
324  const irep_idt &mode);
326  const codet &code,
327  goto_programt &dest,
328  const irep_idt &mode);
330  const codet &code,
331  goto_programt &dest,
332  const irep_idt &mode);
333  void convert_asm(const code_asmt &code, goto_programt &dest);
334 
335  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
336 
337  void copy(
338  const codet &code,
340  goto_programt &dest);
341 
342  //
343  // exceptions
344  //
345 
346  symbol_exprt exception_flag(const irep_idt &mode);
347 
349  const source_locationt &source_location,
350  goto_programt &dest,
351  const irep_idt &mode,
352  optionalt<node_indext> destructor_start_point = {},
353  optionalt<node_indext> destructor_end_point = {});
354 
355  //
356  // gotos
357  //
358 
359  void finish_gotos(goto_programt &dest, const irep_idt &mode);
362 
363  typedef std::map<irep_idt,
364  std::pair<goto_programt::targett, node_indext>>
366  typedef std::list<std::pair<goto_programt::targett, node_indext>>
368  typedef std::list<goto_programt::targett> computed_gotost;
370  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
371  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
372 
373  struct targetst
374  {
377 
382 
385 
388 
391 
393  return_set(false),
394  has_return_value(false),
395  break_set(false),
396  continue_set(false),
397  default_set(false),
398  throw_set(false),
399  leave_set(false),
404  {
405  }
406 
407  void set_break(goto_programt::targett _break_target)
408  {
409  break_set=true;
410  break_target=_break_target;
412  }
413 
414  void set_continue(goto_programt::targett _continue_target)
415  {
416  continue_set=true;
417  continue_target=_continue_target;
419  }
420 
421  void set_default(goto_programt::targett _default_target)
422  {
423  default_set=true;
424  default_target=_default_target;
425  }
426 
427  void set_return(goto_programt::targett _return_target)
428  {
429  return_set=true;
430  return_target=_return_target;
431  }
432 
433  void set_throw(goto_programt::targett _throw_target)
434  {
435  throw_set=true;
436  throw_target=_throw_target;
438  }
439 
440  void set_leave(goto_programt::targett _leave_target)
441  {
442  leave_set=true;
443  leave_target=_leave_target;
445  }
447 
449  {
450  // for 'while', 'for', 'dowhile'
451 
453  {
458  }
459 
461  {
466  }
467 
471  };
472 
474  {
475  // for 'switch'
476 
478  {
486  }
487 
489  {
496  }
497 
502 
505  };
506 
508  {
509  // for 'try...catch' and the like
510 
511  explicit throw_targett(const targetst &targets)
512  {
516  }
517 
519  {
522  }
523 
525  bool throw_set;
527  };
528 
530  {
531  // for 'try...leave...finally'
532 
533  explicit leave_targett(const targetst &targets)
534  {
538  }
539 
541  {
544  }
545 
547  bool leave_set;
549  };
550 
552  const exprt &value,
553  const caset &case_op);
554 
555  // if(cond) { true_case } else { false_case }
556  void generate_ifthenelse(
557  const exprt &cond,
558  goto_programt &true_case,
559  goto_programt &false_case,
560  const source_locationt &,
561  goto_programt &dest,
562  const irep_idt &mode);
563 
564  // if(guard) goto target_true; else goto target_false;
566  const exprt &guard,
567  goto_programt::targett target_true,
568  goto_programt::targett target_false,
569  const source_locationt &,
570  goto_programt &dest,
571  const irep_idt &mode);
572 
573  // if(guard) goto target;
575  const exprt &guard,
576  goto_programt::targett target_true,
577  const source_locationt &,
578  goto_programt &dest,
579  const irep_idt &mode);
580 
581  // turn a OP b OP c into a list a, b, c
582  static void collect_operands(
583  const exprt &expr,
584  const irep_idt &id,
585  std::list<exprt> &dest);
586 
587  // START_THREAD; ... END_THREAD;
589  const code_blockt &thread_body,
590  goto_programt &dest,
591  const irep_idt &mode);
592 
593  //
594  // misc
595  //
596  irep_idt get_string_constant(const exprt &expr);
597  bool get_string_constant(const exprt &expr, irep_idt &);
598  exprt get_constant(const exprt &expr);
599 
614  void do_enum_is_in_range(
615  const exprt &lhs,
616  const symbol_exprt &function,
617  const exprt::operandst &arguments,
618  goto_programt &dest);
619 
620  // some built-in functions
621  void do_atomic_begin(
622  const exprt &lhs,
623  const symbol_exprt &function,
624  const exprt::operandst &arguments,
625  goto_programt &dest);
626  void do_atomic_end(
627  const exprt &lhs,
628  const symbol_exprt &function,
629  const exprt::operandst &arguments,
630  goto_programt &dest);
632  const exprt &lhs,
633  const symbol_exprt &function,
634  const exprt::operandst &arguments,
635  goto_programt &dest);
637  const exprt &lhs,
638  const symbol_exprt &rhs,
639  const exprt::operandst &arguments,
640  goto_programt &dest);
641  void do_array_op(
642  const irep_idt &id,
643  const exprt &lhs,
644  const symbol_exprt &function,
645  const exprt::operandst &arguments,
646  goto_programt &dest);
647  void do_printf(
648  const exprt &lhs,
649  const symbol_exprt &function,
650  const exprt::operandst &arguments,
651  goto_programt &dest);
652  void do_scanf(
653  const exprt &lhs,
654  const symbol_exprt &function,
655  const exprt::operandst &arguments,
656  goto_programt &dest);
657  void do_input(
658  const exprt &rhs,
659  const exprt::operandst &arguments,
660  goto_programt &dest);
661  void do_output(
662  const exprt &rhs,
663  const exprt::operandst &arguments,
664  goto_programt &dest);
665  void do_prob_coin(
666  const exprt &lhs,
667  const symbol_exprt &function,
668  const exprt::operandst &arguments,
669  goto_programt &dest);
670  void do_prob_uniform(
671  const exprt &lhs,
672  const symbol_exprt &function,
673  const exprt::operandst &arguments,
674  goto_programt &dest);
675 
676  exprt get_array_argument(const exprt &src);
677 };
678 
679 #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:18
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:1044
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
goto_convertt::break_switch_targetst::cases
casest cases
Definition: goto_convert_class.h:503
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:387
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
goto_convertt::targetst::set_break
void set_break(goto_programt::targett _break_target)
Definition: goto_convert_class.h:407
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:62
goto_convertt::do_output
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:326
goto_convertt::break_switch_targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:499
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:1671
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:17
code_whilet
codet representing a while statement.
Definition: std_code.h:926
goto_convertt::targetst::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:387
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:400
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1699
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:1050
goto_convertt::leave_targett::leave_set
bool leave_set
Definition: goto_convert_class.h:547
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:376
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:158
goto_convertt::get_array_argument
exprt get_array_argument(const exprt &src)
Definition: builtin_functions.cpp:533
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:506
goto_convertt::has_function_call
static bool has_function_call(const exprt &expr)
Definition: goto_convert_side_effect.cpp:25
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
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:499
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
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:364
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:212
goto_convertt::cases_mapt
std::map< goto_programt::targett, casest::iterator > cases_mapt
Definition: goto_convert_class.h:371
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:86
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:387
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
goto_convertt::convert_ifthenelse
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1407
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:31
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:1480
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:345
goto_convertt::leave_targett
Definition: goto_convert_class.h:530
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:384
code_continuet
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1664
goto_convertt::break_switch_targetst::default_set
bool default_set
Definition: goto_convert_class.h:500
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:1543
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:430
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:1921
goto_convertt::break_continue_targetst::break_continue_targetst
break_continue_targetst(const targetst &targets)
Definition: goto_convert_class.h:452
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:376
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:776
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:1832
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:533
goto_convertt::throw_targett
Definition: goto_convert_class.h:508
goto_convertt::targetst::set_leave
void set_leave(goto_programt::targett _leave_target)
Definition: goto_convert_class.h:440
goto_convertt::targetst::leave_set
bool leave_set
Definition: goto_convert_class.h:376
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:592
goto_convertt::targetst::has_return_value
bool has_return_value
Definition: goto_convert_class.h:375
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
goto_convertt::targetst::labels
labelst labels
Definition: goto_convert_class.h:378
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:613
goto_convertt::convert_break
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1242
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
goto_convertt::targetst::gotos
gotost gotos
Definition: goto_convert_class.h:379
goto_convertt::break_switch_targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:504
goto_convertt::exception_flag
symbol_exprt exception_flag(const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:236
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:988
goto_convertt::break_switch_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:488
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:498
goto_convertt::leave_targett::leave_stack_node
node_indext leave_stack_node
Definition: goto_convert_class.h:548
goto_convertt::convert_continue
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1318
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:209
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:284
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:145
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1628
goto_convertt
Definition: goto_convert_class.h:31
goto_convertt::break_continue_targetst::break_set
bool break_set
Definition: goto_convert_class.h:470
goto_convertt::get_string_constant
irep_idt get_string_constant(const exprt &expr)
Definition: goto_convert.cpp:1792
goto_convertt::targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:389
goto_convertt::rewrite_boolean
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
Definition: goto_clean_expr.cpp:107
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1157
goto_convertt::targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:386
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:38
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1405
goto_convertt::convert_CPROVER_throw
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:181
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:146
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:565
goto_convertt::break_continue_targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:469
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:523
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:640
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:454
goto_convertt::targetst::set_return
void set_return(goto_programt::targett _return_target)
Definition: goto_convert_class.h:427
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:20
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:411
goto_convertt::convert_goto
void convert_goto(const code_gotot &code, goto_programt &dest)
Definition: goto_convert.cpp:1337
goto_convertt::break_switch_targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:501
goto_convertt::targetst::return_set
bool return_set
Definition: goto_convert_class.h:375
message_handlert
Definition: message.h:28
goto_convertt::targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:375
goto_convertt::break_continue_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:460
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
goto_convertt::targetst::break_set
bool break_set
Definition: goto_convert_class.h:375
goto_convertt::convert_for
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:896
goto_convertt::targetst::set_throw
void set_throw(goto_programt::targett _throw_target)
Definition: goto_convert_class.h:433
goto_convertt::remove_cpp_delete
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:438
goto_convertt::caset
exprt::operandst caset
Definition: goto_convert_class.h:369
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:264
goto_convertt::get_constant
exprt get_constant(const exprt &expr)
Definition: goto_convert.cpp:1806
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:988
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:387
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:208
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:1453
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:30
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:83
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:18
source_locationt
Definition: source_location.h:19
goto_convertt::remove_temporary_object
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
Definition: goto_convert_side_effect.cpp:487
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:311
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:195
goto_convertt::targetst
Definition: goto_convert_class.h:374
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:341
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
goto_convertt::break_switch_targetst::break_switch_targetst
break_switch_targetst(const targetst &targets)
Definition: goto_convert_class.h:477
goto_convertt::convert_msc_leave
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:70
goto_convertt::throw_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:518
goto_convertt::targetst::destructor_stack
destructor_treet destructor_stack
Definition: goto_convert_class.h:381
goto_convertt::case_guard
exprt case_guard(const exprt &value, const caset &case_op)
Definition: goto_convert.cpp:1113
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:1259
code_switcht
codet representing a switch statement.
Definition: std_code.h:864
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:1359
goto_convertt::targetst::cases
casest cases
Definition: goto_convert_class.h:383
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:55
goto_convertt::break_switch_targetst::break_set
bool break_set
Definition: goto_convert_class.h:500
goto_convertt::gotost
std::list< std::pair< goto_programt::targett, node_indext > > gotost
Definition: goto_convert_class.h:367
goto_convertt::computed_gotost
std::list< goto_programt::targett > computed_gotost
Definition: goto_convert_class.h:368
goto_convertt::throw_targett::throw_set
bool throw_set
Definition: goto_convert_class.h:525
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:181
goto_convertt::targetst::set_continue
void set_continue(goto_programt::targett _continue_target)
Definition: goto_convert_class.h:414
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
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:566
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:690
goto_convertt::labelst
std::map< irep_idt, std::pair< goto_programt::targett, node_indext > > labelst
Definition: goto_convert_class.h:365
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:470
goto_convertt::leave_targett::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:546
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:763
goto_convertt::convert_loop_contracts
void convert_loop_contracts(const codet &code, goto_programt::targett loop, const irep_idt &mode)
Definition: goto_convert.cpp:860
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:1395
goto_convertt::targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:386
goto_convertt::break_switch_targetst
Definition: goto_convert_class.h:474
goto_convertt::throw_targett::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:524
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
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:390
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:449
goto_convertt::targetst::set_default
void set_default(goto_programt::targett _default_target)
Definition: goto_convert_class.h:421
allocate_objects.h
goto_convertt::targetst::continue_stack_node
node_indext continue_stack_node
Definition: goto_convert_class.h:389
goto_convertt::throw_targett::throw_stack_node
node_indext throw_stack_node
Definition: goto_convert_class.h:526
goto_convertt::leave_targett::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:540
goto_convertt::throw_targett::throw_targett
throw_targett(const targetst &targets)
Definition: goto_convert_class.h:511
goto_convertt::casest
std::list< std::pair< goto_programt::targett, caset > > casest
Definition: goto_convert_class.h:370
goto_convertt::targetst::targetst
targetst()
Definition: goto_convert_class.h:392
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1896
goto_convertt::convert_atomic_begin
void convert_atomic_begin(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1383
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:380
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:31
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:109
goto_convertt::targetst::throw_stack_node
node_indext throw_stack_node
Definition: goto_convert_class.h:389
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1840
goto_convertt::convert_switch
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1142
goto_convertt::break_continue_targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:468
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
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:386
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:1855
goto_convertt::convert_end_thread
void convert_end_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1371
goto_convertt::convert_gcc_computed_goto
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1347