cprover
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 <
goto-programs/goto_model.h
>
16
17
class
code_function_callt
function_to_call
(
18
symbol_tablet
&,
19
const
irep_idt
&
id
,
20
const
irep_idt
&argument);
21
22
void
function_enter
(
23
goto_modelt
&,
24
const
irep_idt
&
id
);
25
26
void
function_exit
(
27
goto_modelt
&,
28
const
irep_idt
&
id
);
29
30
#endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
symbol_tablet
The symbol table.
Definition:
symbol_table.h:20
function_to_call
class code_function_callt function_to_call(symbol_tablet &, const irep_idt &id, const irep_idt &argument)
Definition:
function.cpp:21
function_exit
void function_exit(goto_modelt &, const irep_idt &id)
Definition:
function.cpp:97
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition:
goto_model.h:26
code_function_callt
codet representation of a function call statement.
Definition:
std_code.h:1183
irept::id
const irep_idt & id() const
Definition:
irep.h:418
function_enter
void function_enter(goto_modelt &, const irep_idt &id)
Definition:
function.cpp:72
goto-instrument
function.h
Generated by
1.8.20