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 goto_convert(const codet &code, goto_programt &dest);
30 
32  symbol_tablet &_symbol_table,
33  message_handlert &_message_handler):
34  messaget(_message_handler),
35  symbol_table(_symbol_table),
36  ns(_symbol_table),
38  tmp_symbol_prefix("goto_convertt")
39  {
40  }
41 
42  virtual ~goto_convertt()
43  {
44  }
45 
46 protected:
50  std::string tmp_symbol_prefix;
51 
52  void goto_convert_rec(const codet &code, goto_programt &dest);
53 
54  //
55  // tools for symbols
56  //
57  void new_name(symbolt &symbol);
58  const symbolt &lookup(const irep_idt &identifier);
59 
61  const typet &type,
62  const std::string &suffix,
63  goto_programt &dest,
64  const source_locationt &);
65 
67  const exprt &expr,
68  goto_programt &dest);
69 
70  //
71  // translation of C expressions (with side effects)
72  // into the program logic
73  //
74 
75  void clean_expr(
76  exprt &expr,
77  goto_programt &dest,
78  bool result_is_used=true);
79 
81  exprt &expr,
82  goto_programt &dest);
83 
84  static bool needs_cleaning(const exprt &expr);
85 
86  void make_temp_symbol(
87  exprt &expr,
88  const std::string &suffix,
89  goto_programt &);
90 
91  void rewrite_boolean(exprt &dest);
92 
93  static bool has_sideeffect(const exprt &expr);
94  static bool has_function_call(const exprt &expr);
95 
96  void remove_side_effect(
97  side_effect_exprt &expr,
98  goto_programt &dest,
99  bool result_is_used);
100  void remove_push_catch(
101  side_effect_exprt &expr,
102  goto_programt &dest);
103  void remove_assignment(
104  side_effect_exprt &expr,
105  goto_programt &dest,
106  bool result_is_used);
107  void remove_pre(
108  side_effect_exprt &expr,
109  goto_programt &dest,
110  bool result_is_used);
111  void remove_post(
112  side_effect_exprt &expr,
113  goto_programt &dest,
114  bool result_is_used);
116  side_effect_exprt &expr,
117  goto_programt &dest,
118  bool result_is_used);
119  void remove_cpp_new(
120  side_effect_exprt &expr,
121  goto_programt &dest,
122  bool result_is_used);
123  void remove_cpp_delete(
124  side_effect_exprt &expr,
125  goto_programt &dest,
126  bool result_is_used);
127  void remove_malloc(
128  side_effect_exprt &expr,
129  goto_programt &dest,
130  bool result_is_used);
132  side_effect_exprt &expr,
133  goto_programt &dest,
134  bool result_is_used);
136  side_effect_exprt &expr,
137  goto_programt &dest,
138  bool result_is_used);
140  exprt &expr,
141  goto_programt &dest);
142 
143  virtual void do_cpp_new(
144  const exprt &lhs,
145  const side_effect_exprt &rhs,
146  goto_programt &dest);
147 
148  void do_java_new(
149  const exprt &lhs,
150  const side_effect_exprt &rhs,
151  goto_programt &dest);
152 
153  void do_java_new_array(
154  const exprt &lhs,
155  const side_effect_exprt &rhs,
156  goto_programt &dest);
157 
158  static void replace_new_object(
159  const exprt &object,
160  exprt &dest);
161 
162  void cpp_new_initializer(
163  const exprt &lhs,
164  const side_effect_exprt &rhs,
165  goto_programt &dest);
166 
167  //
168  // function calls
169  //
170 
171  virtual void do_function_call(
172  const exprt &lhs,
173  const exprt &function,
174  const exprt::operandst &arguments,
175  goto_programt &dest);
176 
177  virtual void do_function_call_if(
178  const exprt &lhs,
179  const if_exprt &function,
180  const exprt::operandst &arguments,
181  goto_programt &dest);
182 
183  virtual void do_function_call_symbol(
184  const exprt &lhs,
185  const symbol_exprt &function,
186  const exprt::operandst &arguments,
187  goto_programt &dest);
188 
189  virtual void do_function_call_symbol(const symbolt &symbol)
190  {
191  }
192 
193  virtual void do_function_call_other(
194  const exprt &lhs,
195  const exprt &function,
196  const exprt::operandst &arguments,
197  goto_programt &dest);
198 
199  //
200  // conversion
201  //
202  void convert_block(const code_blockt &code, goto_programt &dest);
203  void convert_decl(const code_declt &code, goto_programt &dest);
204  void convert_decl_type(const codet &code, goto_programt &dest);
205  void convert_expression(const code_expressiont &code, goto_programt &dest);
206  void convert_assign(const code_assignt &code, goto_programt &dest);
207  void convert_cpp_delete(const codet &code, goto_programt &dest);
208  void convert_loop_invariant(const codet &code, goto_programt::targett loop);
209  void convert_for(const code_fort &code, goto_programt &dest);
210  void convert_while(const code_whilet &code, goto_programt &dest);
211  void convert_dowhile(const codet &code, goto_programt &dest);
212  void convert_assume(const code_assumet &code, goto_programt &dest);
213  void convert_assert(const code_assertt &code, goto_programt &dest);
214  void convert_switch(const code_switcht &code, goto_programt &dest);
215  void convert_break(const code_breakt &code, goto_programt &dest);
216  void convert_return(const code_returnt &code, goto_programt &dest);
217  void convert_continue(const code_continuet &code, goto_programt &dest);
218  void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest);
219  void convert_init(const codet &code, goto_programt &dest);
220  void convert_goto(const codet &code, goto_programt &dest);
221  void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
222  void convert_skip(const codet &code, goto_programt &dest);
223  void convert_non_deterministic_goto(const codet &code, goto_programt &dest);
224  void convert_label(const code_labelt &code, goto_programt &dest);
225  void convert_gcc_local_label(const codet &code, goto_programt &dest);
226  void convert_switch_case(const code_switch_caset &code, goto_programt &dest);
227  void convert_gcc_switch_case_range(const codet &code, goto_programt &dest);
229  const code_function_callt &code,
230  goto_programt &dest);
231  void convert_specc_notify(const codet &code, goto_programt &dest);
232  void convert_specc_wait(const codet &code, goto_programt &dest);
233  void convert_specc_par(const codet &code, goto_programt &dest);
234  void convert_specc_event(const exprt &op,
235  std::set<irep_idt> &events);
236  void convert_start_thread(const codet &code, goto_programt &dest);
237  void convert_end_thread(const codet &code, goto_programt &dest);
238  void convert_atomic_begin(const codet &code, goto_programt &dest);
239  void convert_atomic_end(const codet &code, goto_programt &dest);
240  void convert_bp_enforce(const codet &code, goto_programt &dest);
241  void convert_bp_abortif(const codet &code, goto_programt &dest);
242  void convert_msc_try_finally(const codet &code, goto_programt &dest);
243  void convert_msc_try_except(const codet &code, goto_programt &dest);
244  void convert_msc_leave(const codet &code, goto_programt &dest);
245  void convert_try_catch(const codet &code, goto_programt &dest);
246  void convert_java_try_catch(const codet &code, goto_programt &dest);
247  void convert_CPROVER_try_catch(const codet &code, goto_programt &dest);
248  void convert_CPROVER_try_finally(const codet &code, goto_programt &dest);
249  void convert_CPROVER_throw(const codet &code, goto_programt &dest);
250  void convert_asm(const code_asmt &code, goto_programt &dest);
251 
252  void convert(const codet &code, goto_programt &dest);
253 
254  void copy(
255  const codet &code,
257  goto_programt &dest);
258 
259  //
260  // exceptions
261  //
262 
263  typedef std::vector<codet> destructor_stackt;
264 
267  const source_locationt &,
268  std::size_t stack_size,
269  goto_programt &dest);
271  const source_locationt &,
272  std::size_t stack_size,
273  goto_programt &dest,
275 
276  //
277  // gotos
278  //
279 
280  void finish_gotos(goto_programt &dest);
283 
284  typedef std::map<irep_idt,
285  std::pair<goto_programt::targett, destructor_stackt>>
287  typedef std::list<std::pair<goto_programt::targett, destructor_stackt>>
289  typedef std::list<goto_programt::targett> computed_gotost;
291  typedef std::list<std::pair<goto_programt::targett, caset> > casest;
292  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
293 
294  struct targetst
295  {
298 
303 
306 
309 
312 
314  return_set(false),
315  has_return_value(false),
316  break_set(false),
317  continue_set(false),
318  default_set(false),
319  throw_set(false),
320  leave_set(false)
321  {
322  }
323 
324  void set_break(goto_programt::targett _break_target)
325  {
326  break_set=true;
327  break_target=_break_target;
329  }
330 
331  void set_continue(goto_programt::targett _continue_target)
332  {
333  continue_set=true;
334  continue_target=_continue_target;
336  }
337 
338  void set_default(goto_programt::targett _default_target)
339  {
340  default_set=true;
341  default_target=_default_target;
342  }
343 
344  void set_return(goto_programt::targett _return_target)
345  {
346  return_set=true;
347  return_target=_return_target;
348  }
349 
350  void set_throw(goto_programt::targett _throw_target)
351  {
352  throw_set=true;
353  throw_target=_throw_target;
355  }
356 
357  void set_leave(goto_programt::targett _leave_target)
358  {
359  leave_set=true;
360  leave_target=_leave_target;
362  }
363  } targets;
364 
366  {
367  // for 'while', 'for', 'dowhile'
368 
370  {
375  }
376 
378  {
383  }
384 
388  };
389 
391  {
392  // for 'switch'
393 
395  {
403  }
404 
406  {
413  }
414 
418  std::size_t break_stack_size;
419 
422  };
423 
425  {
426  // for 'try...catch' and the like
427 
428  explicit throw_targett(const targetst &targets)
429  {
433  }
434 
436  {
439  }
440 
442  bool throw_set;
443  std::size_t throw_stack_size;
444  };
445 
447  {
448  // for 'try...leave...finally'
449 
450  explicit leave_targett(const targetst &targets)
451  {
455  }
456 
458  {
461  }
462 
464  bool leave_set;
465  std::size_t leave_stack_size;
466  };
467 
469  {
473  };
474  typedef std::list<guarded_gotot> guarded_gotost;
476 
478  const exprt &value,
479  const caset &case_op);
480 
481  // if(cond) { true_case } else { false_case }
482  void generate_ifthenelse(
483  const exprt &cond,
484  goto_programt &true_case,
485  goto_programt &false_case,
486  const source_locationt &,
487  goto_programt &dest);
488 
489  // if(guard) goto target_true; else goto target_false;
491  const exprt &guard,
492  goto_programt::targett target_true,
493  goto_programt::targett target_false,
494  const source_locationt &,
495  goto_programt &dest);
496 
497  // if(guard) goto target;
499  const exprt &guard,
500  goto_programt::targett target_true,
501  const source_locationt &,
502  goto_programt &dest);
503 
504  // turn a OP b OP c into a list a, b, c
505  static void collect_operands(
506  const exprt &expr,
507  const irep_idt &id,
508  std::list<exprt> &dest);
509 
510  //
511  // misc
512  //
513  irep_idt get_string_constant(const exprt &expr);
514  bool get_string_constant(const exprt &expr, irep_idt &);
515  exprt get_constant(const exprt &expr);
516 
517  // some built-in functions
518  void do_atomic_begin(
519  const exprt &lhs,
520  const exprt &rhs,
521  const exprt::operandst &arguments,
522  goto_programt &dest);
523  void do_atomic_end(
524  const exprt &lhs,
525  const exprt &rhs,
526  const exprt::operandst &arguments,
527  goto_programt &dest);
528  void do_create_thread(
529  const exprt &lhs,
530  const exprt &rhs,
531  const exprt::operandst &arguments,
532  goto_programt &dest);
533  void do_array_set(
534  const exprt &lhs,
535  const exprt &rhs,
536  const exprt::operandst &arguments,
537  goto_programt &dest);
538  void do_array_equal(
539  const exprt &lhs,
540  const exprt &rhs,
541  const exprt::operandst &arguments,
542  goto_programt &dest);
543  void do_array_op(
544  const irep_idt &id,
545  const exprt &lhs,
546  const exprt &rhs,
547  const exprt::operandst &arguments,
548  goto_programt &dest);
549  void do_printf(
550  const exprt &lhs,
551  const exprt &rhs,
552  const exprt::operandst &arguments,
553  goto_programt &dest);
554  void do_scanf(
555  const exprt &lhs,
556  const exprt &rhs,
557  const exprt::operandst &arguments,
558  goto_programt &dest);
559  void do_input(
560  const exprt &lhs,
561  const exprt &rhs,
562  const exprt::operandst &arguments,
563  goto_programt &dest);
564  void do_output(
565  const exprt &lhs,
566  const exprt &rhs,
567  const exprt::operandst &arguments,
568  goto_programt &dest);
569  void do_prob_coin(
570  const exprt &lhs,
571  const exprt &rhs,
572  const exprt::operandst &arguments,
573  goto_programt &dest);
574  void do_prob_uniform(
575  const exprt &lhs,
576  const exprt &rhs,
577  const exprt::operandst &arguments,
578  goto_programt &dest);
579 
580  exprt get_array_argument(const exprt &src);
581 };
582 
583 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest)
void convert_atomic_begin(const codet &code, goto_programt &dest)
break_continue_targetst(const targetst &targets)
throw_targett(const targetst &targets)
void convert_specc_event(const exprt &op, std::set< irep_idt > &events)
The type of an expression.
Definition: type.h:20
void convert_skip(const codet &code, goto_programt &dest)
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
exprt::operandst caset
A ‘switch’ instruction.
Definition: std_code.h:412
std::list< goto_programt::targett > computed_gotost
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
symbol_tablet & symbol_table
goto_programt::targett return_target
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest)
A continue for ‘for’ and ‘while’ loops.
Definition: std_code.h:898
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void remove_push_catch(side_effect_exprt &expr, goto_programt &dest)
struct goto_convertt::targetst targets
static bool has_sideeffect(const exprt &expr)
guarded_gotost guarded_gotos
void do_input(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
goto_programt::targett throw_target
goto_programt::targett break_target
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void convert_atomic_end(const codet &code, goto_programt &dest)
void convert_assign(const code_assignt &code, goto_programt &dest)
void convert_dowhile(const codet &code, goto_programt &dest)
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
void do_atomic_begin(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void convert_init(const codet &code, goto_programt &dest)
void do_array_equal(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
The trinary if-then-else operator.
Definition: std_expr.h:2771
void convert_goto(const codet &code, goto_programt &dest)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
virtual ~goto_convertt()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void convert_end_thread(const codet &code, goto_programt &dest)
An expression statement.
Definition: std_code.h:957
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void set_default(goto_programt::targett _default_target)
static bool has_function_call(const exprt &expr)
void convert_specc_wait(const codet &code, goto_programt &dest)
std::map< goto_programt::targett, casest::iterator > cases_mapt
goto_programt::targett throw_target
destructor_stackt destructor_stack
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
void goto_convert(const codet &code, goto_programt &dest)
void convert_switch(const code_switcht &code, goto_programt &dest)
void convert_decl_type(const codet &code, goto_programt &dest)
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
irep_idt get_string_constant(const exprt &expr)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
goto_convertt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void convert_bp_abortif(const codet &code, goto_programt &dest)
void convert_for(const code_fort &code, goto_programt &dest)
std::string tmp_symbol_prefix
goto_programt::targett ifiter
void convert_msc_try_finally(const codet &code, goto_programt &dest)
A declaration of a local variable.
Definition: std_code.h:192
symbol_exprt exception_flag()
void clean_expr_address_of(exprt &expr, goto_programt &dest)
goto_programt::targett leave_target
void convert_label(const code_labelt &code, goto_programt &dest)
void restore(targetst &targets)
goto_programt::targett default_target
exprt case_guard(const exprt &value, const caset &case_op)
void do_prob_coin(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest)
goto_programt::targett leave_target
The symbol table.
Definition: symbol_table.h:52
void convert_specc_notify(const codet &code, goto_programt &dest)
void do_prob_uniform(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void convert_continue(const code_continuet &code, goto_programt &dest)
void convert_while(const code_whilet &code, goto_programt &dest)
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest)
A label for branch targets.
Definition: std_code.h:760
A function call.
Definition: std_code.h:657
Guard Data Structure.
void convert_msc_leave(const codet &code, goto_programt &dest)
A ‘while’ instruction.
Definition: std_code.h:457
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_specc_par(const codet &code, goto_programt &dest)
void finish_computed_gotos(goto_programt &dest)
void convert_return(const code_returnt &code, goto_programt &dest)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
void restore(targetst &targets)
exprt get_array_argument(const exprt &src)
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void goto_convert_rec(const codet &code, goto_programt &dest)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
void do_array_op(const irep_idt &id, const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
std::vector< exprt > operandst
Definition: expr.h:49
void do_printf(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void convert_function_call(const code_function_callt &code, goto_programt &dest)
void remove_post(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void convert_assert(const code_assertt &code, goto_programt &dest)
An assertion.
Definition: std_code.h:312
break_switch_targetst(const targetst &targets)
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest)
An assumption.
Definition: std_code.h:274
exprt get_constant(const exprt &expr)
void set_continue(goto_programt::targett _continue_target)
void convert_java_try_catch(const codet &code, goto_programt &dest)
goto_programt::targett gotoiter
void do_scanf(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_output(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
static bool needs_cleaning(const exprt &expr)
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
goto_programt::targett continue_target
std::vector< codet > destructor_stackt
void convert_decl(const code_declt &code, goto_programt &dest)
void new_name(symbolt &symbol)
void convert_try_catch(const codet &code, goto_programt &dest)
void finish_guarded_gotos(goto_programt &dest)
For each if(x) goto z; goto y; z: emitted, see if any destructor statements were inserted between got...
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest)
if(guard) goto target_true; else goto target_false;
void set_break(goto_programt::targett _break_target)
void set_leave(goto_programt::targett _leave_target)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
Definition: expr.h:46
const symbolt & lookup(const irep_idt &identifier)
A break for ‘for’ and ‘while’ loops.
Definition: std_code.h:876
void finish_gotos(goto_programt &dest)
void convert_break(const code_breakt &code, goto_programt &dest)
void convert_loop_invariant(const codet &code, goto_programt::targett loop)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest)
computed_gotost computed_gotos
void set_throw(goto_programt::targett _throw_target)
void do_array_set(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
An inline assembler statement.
Definition: std_code.h:920
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &)
unsigned temporary_counter
void convert_assume(const code_assumet &code, goto_programt &dest)
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
std::list< guarded_gotot > guarded_gotost
void convert_block(const code_blockt &code, goto_programt &dest)
virtual void do_function_call_symbol(const symbolt &symbol)
std::list< std::pair< goto_programt::targett, caset > > casest
Sequential composition.
Definition: std_code.h:63
An if-then-else.
Definition: std_code.h:350
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A switch-case.
Definition: std_code.h:817
dstringt irep_idt
Definition: irep.h:32
leave_targett(const targetst &targets)
A statement in a programming language.
Definition: std_code.h:19
void convert_msc_try_except(const codet &code, goto_programt &dest)
Return from a function.
Definition: std_code.h:714
A ‘for’ instruction.
Definition: std_code.h:547
void convert_bp_enforce(const codet &code, goto_programt &dest)
An expression containing a side effect.
Definition: std_code.h:997
void convert_expression(const code_expressiont &code, goto_programt &dest)
void convert_start_thread(const codet &code, goto_programt &dest)
#define stack(x)
Definition: parser.h:144
std::map< irep_idt, std::pair< goto_programt::targett, destructor_stackt > > labelst
void set_return(goto_programt::targett _return_target)
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
static void replace_new_object(const exprt &object, exprt &dest)
Concrete Goto Program.
void do_atomic_end(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Assignment.
Definition: std_code.h:144
void do_create_thread(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void convert_CPROVER_throw(const codet &code, goto_programt &dest)
std::list< std::pair< goto_programt::targett, destructor_stackt > > gotost
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest)
if(guard) true_case; else false_case;
void convert_non_deterministic_goto(const codet &code, goto_programt &dest)