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 #include <util/irep.h>
16 
17 #include <list>
18 
19 class goto_programt;
20 class namespacet;
21 class typet;
22 
23 class code_function_callt
24 get_destructor(const namespacet &ns, const typet &type);
25 
26 void destruct_locals(
27  const std::list<irep_idt> &vars,
28  goto_programt &dest,
29  const namespacet &ns);
30 
31 #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition: goto_instruction_code.h:271
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
typet
The type of an expression, extends irept.
Definition: type.h:29
destruct_locals
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition: destructor.cpp:62
get_destructor
class code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:21