cprover
goto_convert_functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs with Functions
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_FUNCTIONS_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_FUNCTIONS_H
16 
17 #include "goto_model.h"
18 #include "goto_convert_class.h"
19 
20 // convert it all!
21 void goto_convert(
22  symbol_tablet &symbol_table,
23  goto_functionst &functions,
24  message_handlert &message_handler);
25 
26 // convert it all!
27 void goto_convert(
28  symbol_tablet &symbol_table,
29  goto_modelt &dest,
30  message_handlert &message_handler);
31 
32 // just convert a specific function
33 void goto_convert(
34  const irep_idt &identifier,
35  symbol_tablet &symbol_table,
36  goto_functionst &functions,
37  message_handlert &message_handler);
38 
40 {
41 public:
42  void goto_convert();
43  void convert_function(const irep_idt &identifier);
44 
46  symbol_tablet &_symbol_table,
47  goto_functionst &_functions,
48  message_handlert &_message_handler);
49 
50  virtual ~goto_convert_functionst();
51 
52 protected:
54 
55  static bool hide(const goto_programt &goto_program);
56 
57  //
58  // function calls
59  //
60  void add_return(
62  const source_locationt &);
63 };
64 
65 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_FUNCTIONS_H
Symbol Table + CFG.
Program Transformation.
The symbol table.
Definition: symbol_table.h:52
goto_function_templatet< goto_programt > goto_functiont
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
static bool hide(const goto_programt &goto_program)
void goto_convert(symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
goto_convert_functionst(symbol_tablet &_symbol_table, goto_functionst &_functions, message_handlert &_message_handler)
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
void convert_function(const irep_idt &identifier)