cprover
Loading...
Searching...
No Matches
goto_convert_functions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs with Functions
4
5Author: Daniel Kroening
6
7Date: 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_convert_class.h"
18#include "goto_functions.h"
19
20class goto_modelt;
21
22// convert it all!
23void goto_convert(
25 goto_functionst &functions,
27
28// convert it all!
29void goto_convert(
32
33// just convert a specific function
34void goto_convert(
35 const irep_idt &identifier,
37 goto_functionst &functions,
39
41{
42public:
43 void goto_convert(goto_functionst &functions);
45 const irep_idt &identifier,
47
51
53
54protected:
55 static bool hide(const goto_programt &);
56
57 //
58 // function calls
59 //
60 void add_return(
62 const typet &return_type,
63 const source_locationt &);
64};
65
66#endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_FUNCTIONS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
void add_return(goto_functionst::goto_functiont &, const typet &return_type, const source_locationt &)
void goto_convert(goto_functionst &functions)
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
static bool hide(const goto_programt &)
A collection of goto functions.
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
A generic container class for the GOTO intermediate representation of one function.
mstreamt & result() const
Definition message.h:409
The symbol table base class interface.
The type of an expression, extends irept.
Definition type.h:29
Program Transformation.
void goto_convert(symbol_table_baset &symbol_table, goto_functionst &functions, message_handlert &)
Goto Programs with Functions.