|
CBMC
|
Utility functions that compute root object expressions for assigns clause targets and LHS expressions. More...
Include dependency graph for dfcc_root_object.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| std::unordered_set< exprt, irep_hash > | dfcc_root_objects (const exprt &expr) |
| Computes a set of root object expressions from an lvalue or assigns clause target expression. | |
Utility functions that compute root object expressions for assigns clause targets and LHS expressions.
Definition in file dfcc_root_object.h.
Computes a set of root object expressions from an lvalue or assigns clause target expression.
A root object expression is a simpler expression that denotes the object that contains the memory location refered to by the initial expression.
Definition at line 133 of file dfcc_root_object.cpp.