CBMC
destructor.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Destructor Calls
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
13
#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
14
15
class
namespacet
;
16
class
typet
;
17
18
class
code_function_callt
get_destructor
(
19
const
namespacet
&ns,
20
const
typet
&
type
);
21
22
#endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
typet
The type of an expression, extends irept.
Definition:
type.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:90
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:84
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition:
goto_instruction_code.h:271
get_destructor
class code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition:
destructor.cpp:18
src
goto-programs
destructor.h
Generated by
1.8.17