CBMC
function.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Function Entering and Exiting
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_H
13 #define CPROVER_GOTO_INSTRUMENT_FUNCTION_H
14 
15 #include <util/irep.h>
16 
17 class goto_modelt;
18 class symbol_table_baset;
19 
20 class code_function_callt function_to_call(
21  symbol_table_baset &,
22  const irep_idt &id,
23  const irep_idt &argument);
24 
25 void function_enter(
26  goto_modelt &,
27  const irep_idt &id);
28 
29 void function_exit(
30  goto_modelt &,
31  const irep_idt &id);
32 
33 #endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_H
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition: goto_instruction_code.h:271
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
goto_modelt
Definition: goto_model.h:27
irept::id
const irep_idt & id() const
Definition: irep.h:384
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
function_to_call
class code_function_callt function_to_call(symbol_table_baset &, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:22
function_exit
void function_exit(goto_modelt &, const irep_idt &id)
Definition: function.cpp:102
function_enter
void function_enter(goto_modelt &, const irep_idt &id)
Definition: function.cpp:77