Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.

abstract_object_pointert abstract_object_merge_internal (const abstract_object_pointert &other) const override

Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.

- Protected Member Functions inherited from write_location_contextt

internal_abstract_object_pointert mutable_clone () const override

abstract_object_pointert merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const override

Create a new abstract object that is the result of merging this abstract object with a given abstract_object.

abstract_object_pointert meet (const abstract_object_pointert &other) const override

Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.

abstract_object_pointert abstract_object_merge_internal (const abstract_object_pointert &other) const override

Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.

abstract_object_pointert write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override

A helper function to evaluate writing to a component of an abstract object.

virtual locationst get_last_written_locations () const

void set_last_written_locations (const locationst &locations)

Sets the last written locations for this context.

- Protected Member Functions inherited from context_abstract_objectt

void set_child (const abstract_object_pointert &child)

void set_top_internal () override

void set_not_top_internal () override

exprt to_predicate_internal (const exprt &name) const override

to_predicate implementation - derived classes will override

- Protected Member Functions inherited from abstract_objectt

abstract_object_pointert abstract_object_merge (const abstract_object_pointert &other) const

Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

bool should_use_base_merge (const abstract_object_pointert &other) const

To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific.

abstract_object_pointert abstract_object_meet (const abstract_object_pointert &other) const

Helper function for base meet.

bool should_use_base_meet (const abstract_object_pointert &other) const

Helper function to decide if base meet implementation should be used.

void set_top ()

void set_not_top ()

void set_not_bottom ()

Private Types

using data_dependency_context_ptrt = std::shared_ptr< const data_dependency_contextt >

typedef std::set< goto_programt::const_targett, location_ordert > dependenciest

Private Member Functions

abstract_object_pointert combine (const data_dependency_context_ptrt &other, const data_dependency_context_ptrt &parent) const

abstract_object_pointert insert_data_deps (const dependenciest &dependencies) const

Insert the given set of data dependencies into the data dependencies set for this data_dependency_context object.

context_abstract_object_ptrt update_location_context_internal (const locationst &locations) const override

void set_data_deps (const locationst &locations)

Set the given set of data dependencies for from the locations.

void set_data_deps (const dependenciest &dependences)

Set the given set of data dependencies for this data_dependency_context object.

Private Attributes

dependenciest data_deps

dependenciest data_dominators

Additional Inherited Members

- Public Types inherited from abstract_objectt

typedef goto_programt::const_targett locationt

typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_mapt

- Static Public Member Functions inherited from abstract_objectt

static void dump_map (std::ostream out, const shared_mapt &m)

static void dump_map_diff (std::ostream out, const shared_mapt &m1, const shared_mapt &m2)

Dump all elements in m1 that are different or missing in m2.

static combine_result merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)

static combine_result merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode)

static combine_result meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2)

Interface method for the meet operation.

- Protected Types inherited from context_abstract_objectt

using context_abstract_object_ptrt = std::shared_ptr< context_abstract_objectt >

typedef std::set< locationt, goto_programt::target_less_than > locationst

- Protected Types inherited from abstract_objectt

template<class T >

using internal_sharing_ptrt = std::shared_ptr< T >

typedef internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert

- Static Protected Member Functions inherited from write_location_contextt

static void output_last_written_locations (std::ostream &out, const locationst &locations)

Internal helper function to format and output a given set of locations.

- Protected Attributes inherited from context_abstract_objectt

abstract_object_pointert child_abstract_object

Detailed Description

Definition at line 19 of file data_dependency_context.h.

Member Typedef Documentation

◆ data_dependency_context_ptrt

using data_dependency_contextt::data_dependency_context_ptrt = std::shared_ptr<const data_dependency_contextt>

private

Definition at line 73 of file data_dependency_context.h.

◆ dependenciest

typedef std::set<goto_programt::const_targett, location_ordert> data_dependency_contextt::dependenciest

private

Definition at line 90 of file data_dependency_context.h.

Constructor & Destructor Documentation

◆ data_dependency_contextt() [1/2]

data_dependency_contextt::data_dependency_contextt ( const abstract_object_pointert child,

const typet & type,

bool top,

bool bottom

)

inline

Definition at line 24 of file data_dependency_context.h.

◆ data_dependency_contextt() [2/2]

data_dependency_contextt::data_dependency_contextt ( const abstract_object_pointert child,

const exprt & expr,

const abstract_environmentt & environment,

const namespacet & ns

)

inlineexplicit

Definition at line 33 of file data_dependency_context.h.

Member Function Documentation

◆ abstract_object_merge_internal()

abstract_object_pointert data_dependency_contextt::abstract_object_merge_internal ( const abstract_object_pointert & other ) const

overrideprotectedvirtual

Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.

As such, this function gives the ability to perform additional work for a merge.

For the dependency context, this additional work is the tracking of last_written_locations across the merge

Parameters: other the object to merge with this

Returns: the result of the merge

Reimplemented from abstract_objectt.

Definition at line 308 of file data_dependency_context.cpp.

◆ combine()

abstract_object_pointert data_dependency_contextt::combine ( const data_dependency_context_ptrt & other,

const data_dependency_context_ptrt & parent

) const

private

Definition at line 260 of file data_dependency_context.cpp.

◆ get_data_dependencies()

std::set< goto_programt::const_targett, goto_programt::target_less_than > data_dependency_contextt::get_data_dependencies ( ) const

Return the set of data dependencies associated with this node.

Returns: set of data dependencies

Definition at line 331 of file data_dependency_context.cpp.

◆ get_data_dominators()

std::set< goto_programt::const_targett, goto_programt::target_less_than > data_dependency_contextt::get_data_dominators ( ) const

Return the set of data dominators associated with this node.

Returns: set of data dominators

Definition at line 346 of file data_dependency_context.cpp.

◆ has_been_modified()

bool data_dependency_contextt::has_been_modified ( const abstract_object_pointert & before ) const

overridevirtual

Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

Parameters: before the abstract_object_pointert to use as a reference to compare against

Returns: true if 'this' is considered to have been modified in comparison to 'before', false otherwise.

Reimplemented from context_abstract_objectt.

Definition at line 28 of file data_dependency_context.cpp.

◆ insert_data_deps()

abstract_object_pointert data_dependency_contextt::insert_data_deps ( const dependenciest & dependencies ) const

private

Insert the given set of data dependencies into the data dependencies set for this data_dependency_context object.

Parameters: dependencies the set of dependencies to add

Returns: a new data_dependency_context if new dependencies were added, or 'this' if no addtional dependencies were added.

Definition at line 82 of file data_dependency_context.cpp.

◆ meet()

abstract_object_pointert data_dependency_contextt::meet ( const abstract_object_pointert & other ) const

overrideprotectedvirtual

Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.

Parameters: other pointer to the abstract object to meet

Returns: the resulting abstract object pointer

Reimplemented from abstract_objectt.

Definition at line 243 of file data_dependency_context.cpp.

◆ merge()

abstract_object_pointert data_dependency_contextt::merge ( const abstract_object_pointert & other,

const widen_modet & widen_mode

) const

overrideprotectedvirtual

Create a new abstract object that is the result of merging this abstract object with a given abstract_object.

Parameters: other the abstract object to merge with

widen_mode Indicates if this is a widening merge

Returns: the result of the merge, or 'this' if the merge would not change the current abstract object

Reimplemented from abstract_objectt.

Definition at line 223 of file data_dependency_context.cpp.

◆ mutable_clone()

internal_abstract_object_pointert data_dependency_contextt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 61 of file data_dependency_context.h.

◆ output()

void data_dependency_contextt::output ( std::ostream & out,

const class ai_baset & ai,

const namespacet & ns

) const

overridevirtual

Output a representation of the value of this abstract object.

Parameters: out the stream to write to

ai the abstract interpreter that contains the abstract domain (that contains the object ... )

ns the current namespace

Reimplemented from context_abstract_objectt.

Definition at line 355 of file data_dependency_context.cpp.

◆ set_data_deps() [1/2]

void data_dependency_contextt::set_data_deps ( const dependenciest & dependencies )

private

Set the given set of data dependencies for this data_dependency_context object.

Parameters: dependencies the set of dependencies to set

Definition at line 159 of file data_dependency_context.cpp.

◆ set_data_deps() [2/2]

void data_dependency_contextt::set_data_deps ( const locationst & locations )

private

Set the given set of data dependencies for from the locations.

Parameters: locations the write locations

Definition at line 146 of file data_dependency_context.cpp.

◆ update_location_context_internal()

context_abstract_objectt::context_abstract_object_ptrt data_dependency_contextt::update_location_context_internal ( const locationst & locations ) const

overrideprivatevirtual

Implements context_abstract_objectt.

Definition at line 131 of file data_dependency_context.cpp.

◆ write()

abstract_object_pointert data_dependency_contextt::write ( abstract_environmentt & environment,

const namespacet & ns,

const std::stack< exprt > & stack,

const exprt & specifier,

const abstract_object_pointert & value,

bool merging_write

) const

overridevirtual

A helper function to evaluate writing to a component of an abstract object.

More precise abstractions may override this to update what they are storing for a specific component.

Parameters: environment the abstract environment

ns the current namespace

stack the remaining stack of expressions on the LHS to evaluate

specifier the expression uses to access a specific component

value the value we are trying to write to the component

merging_write if true, this and all future writes will be merged with the current value

Returns: the abstract_objectt representing the result of writing to a specific component.

Reimplemented from context_abstract_objectt.

Definition at line 194 of file data_dependency_context.cpp.

Member Data Documentation

◆ data_deps

dependenciest data_dependency_contextt::data_deps

private

Definition at line 91 of file data_dependency_context.h.

◆ data_dominators

dependenciest data_dependency_contextt::data_dominators

private

Definition at line 92 of file data_dependency_context.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/data_dependency_context.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/data_dependency_context.cpp