CBMC
dfcc_root_object.h File Reference

Utility functions that compute root object expressions for assigns clause targets and LHS expressions. More...

#include <util/irep.h>
#include <unordered_set>
+ 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_hashdfcc_root_objects (const exprt &expr)
 Computes a set of root object expressions from an lvalue or assigns clause target expression. More...
 

Detailed Description

Utility functions that compute root object expressions for assigns clause targets and LHS expressions.

Definition in file dfcc_root_object.h.

Function Documentation

◆ dfcc_root_objects()

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.

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.