CBMC
|
Utility functions that compute root object expressions for assigns clause targets and LHS expressions. More...
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. More... | |
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.