Information the decision procedure holds about each object. More...

Collaboration diagram for decision_procedure_objectt:

Public Attributes
exprt	base_expression
	The expression for the root of the object.

std::size_t	unique_id = 0
	Number which uniquely identifies this particular object.

exprt	size
	Expression which evaluates to the size of the object in bytes.

bool	is_dynamic = false
	This is true for heap allocated objects and false for stack allocated.

Detailed Description

Information the decision procedure holds about each object.

Definition at line 40 of file object_tracking.h.

Member Data Documentation

exprt decision_procedure_objectt::base_expression

The expression for the root of the object.

This is expression equivalent to dereferencing a pointer to this object with a zero offset.

Definition at line 44 of file object_tracking.h.

bool decision_procedure_objectt::is_dynamic = false

This is true for heap allocated objects and false for stack allocated.

Definition at line 50 of file object_tracking.h.

exprt decision_procedure_objectt::size

Expression which evaluates to the size of the object in bytes.

Definition at line 48 of file object_tracking.h.

std::size_t decision_procedure_objectt::unique_id = 0

Number which uniquely identifies this particular object.

Definition at line 46 of file object_tracking.h.

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