goto_symext::allocated_obj Class Reference

Records for dynamically allocated blobs of memory. More...

#include <goto_symex.h>

Public Member Functions
	allocated_obj (const expr2tc &s, const guard2tc &g, const bool a, const std::string n)

Public Attributes
expr2tc	obj
	Symbol identifying the pointer that was allocated.
guard2tc	alloc_guard
	Guard when allocation occured.
bool	auto_deallocd
	Record if the object is automatically desallocated (allocated with alloca).
std::string	name
	The object name.

Detailed Description

Records for dynamically allocated blobs of memory.

Constructor & Destructor Documentation

allocated_obj()

goto_symext::allocated_obj::allocated_obj ( const expr2tc & s, const guard2tc & g, const bool a, const std::string n )

inline

Member Data Documentation

alloc_guard

guard2tc goto_symext::allocated_obj::alloc_guard

Guard when allocation occured.

auto_deallocd

bool goto_symext::allocated_obj::auto_deallocd

Record if the object is automatically desallocated (allocated with alloca).

name

std::string goto_symext::allocated_obj::name

The object name.

obj

expr2tc goto_symext::allocated_obj::obj

Symbol identifying the pointer that was allocated.

Must have ptr type

---

The documentation for this class was generated from the following file:

• src/goto-symex/engine/goto_symex.h