CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
function.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Function Entering and Exiting
4
5Author: 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
17class goto_modelt;
18class symbol_table_baset;
19
20class code_function_callt function_to_call(
21 symbol_table_baset &,
22 const irep_idt &id,
23 const irep_idt &argument);
24
25void function_enter(
26 goto_modelt &,
27 const irep_idt &id);
28
29void function_exit(
30 goto_modelt &,
31 const irep_idt &id);
32
33#endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:388
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