decision_procedure_objectt Struct Reference
Information the decision procedure holds about each object. More...
#include <object_tracking.h>
Collaboration diagram for decision_procedure_objectt:Public Attributes | |
| exprt | base_expression |
| The expression for the root of the object. More... | |
| std::size_t | unique_id = 0 |
| Number which uniquely identifies this particular object. More... | |
| exprt | size |
| Expression which evaluates to the size of the object in bytes. More... | |
| bool | is_dynamic = false |
| This is true for heap allocated objects and false for stack allocated. More... | |
Detailed Description
Information the decision procedure holds about each object.
Definition at line 40 of file object_tracking.h.
Member Data Documentation
◆ base_expression
| 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.
◆ is_dynamic
| 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.
◆ size
| 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.
◆ unique_id
| 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:
- /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/object_tracking.h
