cbmc/destructor_8h_source.html

/*******************************************************************\


Module: Destructor Calls


Author: Daniel Kroening, kroening@kroening.com


\*******************************************************************/


#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H

#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H


#include <util/irep.h>


#include <list>


class goto_programt;

class namespacet;

class typet;


class code_function_callt

get_destructor(const namespacet &ns, const typet &type);


void destruct_locals(

  const std::list<irep_idt> &vars,

  goto_programt &dest,

  const namespacet &ns);


#endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_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

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

irep.h