Loading...

Searching...

No Matches

object_tracking.cpp File Reference

#include "object_tracking.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/string_constant.h>

+ Include dependency graph for object_tracking.cpp:

[フレーム]

Go to the source code of this file.

Functions

exprt make_invalid_pointer_expr ()

Create the invalid pointer constant.

exprt find_object_base_expression (const address_of_exprt &address_of)

The model of addresses we use consists of a unique object identifier and an offset.

static decision_procedure_objectt make_null_object ()

static decision_procedure_objectt make_invalid_pointer_object ()

smt_object_mapt initial_smt_object_map ()

Constructs an initial object map containing the null object.

static bool is_dynamic (const exprt &object)

This function returns true for heap allocated objects or false for stack allocated objects.

void track_expression_objects (const exprt &expression, const namespacet &ns, smt_object_mapt &object_map)

Finds all the object expressions in the given expression and adds them to the object map for cases where the map does not contain them already.

bool objects_are_already_tracked (const exprt &expression, const smt_object_mapt &object_map)

Finds whether all base object expressions in the given expression are already tracked in the given object map.

Function Documentation

◆ find_object_base_expression()

exprt find_object_base_expression ( const address_of_exprt & address_of )

The model of addresses we use consists of a unique object identifier and an offset.

In order to encode the offset identifiers we need to assign unique identifiers to the objects. This function finds the base object expression in an address of expression for which a unique identifier needs to be assigned.

Definition at line 18 of file object_tracking.cpp.

◆ initial_smt_object_map()

smt_object_mapt initial_smt_object_map ( )

Constructs an initial object map containing the null object.

The null object must be added at construction in order to ensure it is allocated a unique identifier of 0.

Definition at line 69 of file object_tracking.cpp.

◆ is_dynamic()

static bool is_dynamic ( const exprt & object )

static

This function returns true for heap allocated objects or false for stack allocated objects.

Definition at line 85 of file object_tracking.cpp.

◆ make_invalid_pointer_expr()

exprt make_invalid_pointer_expr ( )

Create the invalid pointer constant.

Definition at line 13 of file object_tracking.cpp.

◆ make_invalid_pointer_object()

static decision_procedure_objectt make_invalid_pointer_object ( )

static

Definition at line 57 of file object_tracking.cpp.

◆ make_null_object()

static decision_procedure_objectt make_null_object ( )

static

Definition at line 47 of file object_tracking.cpp.

◆ objects_are_already_tracked()

bool objects_are_already_tracked ( const exprt & expression,

const smt_object_mapt & object_map

)

Finds whether all base object expressions in the given expression are already tracked in the given object map.

This supports writing invariants on the base object expressions already being tracked in the map in contexts where the map is const.

Definition at line 120 of file object_tracking.cpp.

◆ track_expression_objects()

void track_expression_objects ( const exprt & expression,

const namespacet & ns,

smt_object_mapt & object_map

)

Finds all the object expressions in the given expression and adds them to the object map for cases where the map does not contain them already.

Parameters: expression The expression within which to find and base object expressions.

ns The namespace used to look up the size of object types.

object_map The map into which any new tracking information should be inserted.

Definition at line 99 of file object_tracking.cpp.