Loading...

Searching...

No Matches

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.

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.

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.

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.