dfcc_root_object.cpp File Reference

#include "dfcc_root_object.h"
#include <util/byte_operators.h>
#include <util/cprover_prefix.h>
#include <util/expr.h>
#include <util/expr_util.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <goto-programs/pointer_arithmetic.h>

Include dependency graph for dfcc_root_object.cpp:

Go to the source code of this file.

Functions
static void	root_objects_rec (const exprt &expr, std::unordered_set< exprt, irep_hash > &dest)
	Recursively computes a set of root object expressions for expr. More...
static exprt	slice_op_to_deref (const exprt &expr)
	Translates object slice expressions found in assigns clause targets to dereference expressions so that root objects can be computed. More...
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...

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.

root_objects_rec()

static void root_objects_rec ( const exprt &  expr, std::unordered_set< exprt, irep_hash > &  dest  )

static

Recursively computes a set of root object expressions for expr.

Definition at line 24 of file dfcc_root_object.cpp.

slice_op_to_deref()

static exprt slice_op_to_deref ( const exprt &  expr )

static

Translates object slice expressions found in assigns clause targets to dereference expressions so that root objects can be computed.

Definition at line 107 of file dfcc_root_object.cpp.