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 ()

Static Protected Member Functions

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

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

Private Types

using combine_fn = std::function< abstract_objectt::combine_result(const abstract_object_pointert &op1, const abstract_object_pointert &op2)>

using write_location_context_ptrt = std::shared_ptr< const write_location_contextt >

Private Member Functions

abstract_object_pointert combine (const write_location_context_ptrt &other, combine_fn fn) const

context_abstract_object_ptrt update_location_context_internal (const locationst &locations) const override

Private Attributes

locationst last_written_locations

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

- Protected Attributes inherited from context_abstract_objectt

abstract_object_pointert child_abstract_object

Detailed Description

General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt.

Instances of this class are constructed with an abstract_object_pointert, to which most operations are delegated, while at the same time this class handles the tracking of the 'last_written_location' information.

Instances of this class are best constructed via the templated version of this, 'context_abstract_objectt<T>' which provides the same constructors as the standard 'abstract_objectt' class.

Definition at line 34 of file write_location_context.h.

Member Typedef Documentation

◆ combine_fn

using write_location_contextt::combine_fn = std::function<abstract_objectt::combine_result( const abstract_object_pointert &op1, const abstract_object_pointert &op2)>

private

Definition at line 95 of file write_location_context.h.

◆ write_location_context_ptrt

using write_location_contextt::write_location_context_ptrt = std::shared_ptr<const write_location_contextt>

private

Definition at line 98 of file write_location_context.h.

Constructor & Destructor Documentation

◆ write_location_contextt() [1/2]

write_location_contextt::write_location_contextt ( const abstract_object_pointert child,

const typet & type,

bool top,

bool bottom

)

inline

Definition at line 37 of file write_location_context.h.

◆ write_location_contextt() [2/2]

write_location_contextt::write_location_contextt ( const abstract_object_pointert child,

const exprt & expr,

const abstract_environmentt & environment,

const namespacet & ns

)

inlineexplicit

Definition at line 46 of file write_location_context.h.

◆ ~write_location_contextt()

virtual write_location_contextt::~write_location_contextt ( )

inlinevirtual

Definition at line 55 of file write_location_context.h.

Member Function Documentation

◆ abstract_object_merge_internal()

abstract_object_pointert write_location_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 163 of file write_location_context.cpp.

◆ combine()

abstract_object_pointert write_location_contextt::combine ( const write_location_context_ptrt & other,

combine_fn fn

) const

private

Definition at line 119 of file write_location_context.cpp.

◆ get_last_written_locations()

context_abstract_objectt::locationst write_location_contextt::get_last_written_locations ( ) const

protectedvirtual

Definition at line 14 of file write_location_context.cpp.

◆ get_location_union()

context_abstract_objectt::locationst write_location_contextt::get_location_union ( const locationst & locations ) const

Construct the union of the location set of the current object, and a the provided location set.

Parameters: locations the set of locations to be unioned with this context

Returns: the union of this objects location set, and 'locations'

Definition at line 235 of file write_location_context.cpp.

◆ has_been_modified()

bool write_location_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 253 of file write_location_context.cpp.

◆ meet()

abstract_object_pointert write_location_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 108 of file write_location_context.cpp.

◆ merge()

abstract_object_pointert write_location_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 79 of file write_location_context.cpp.

◆ mutable_clone()

internal_abstract_object_pointert write_location_contextt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 69 of file write_location_context.h.

◆ output()

void write_location_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 214 of file write_location_context.cpp.

◆ output_last_written_locations()

void write_location_contextt::output_last_written_locations ( std::ostream & out,

const locationst & locations

)

staticprotected

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

Parameters: out the stream on which to output the locations

locations the set of locations to output

Definition at line 331 of file write_location_context.cpp.

◆ set_last_written_locations()

void write_location_contextt::set_last_written_locations ( const locationst & locations )

protected

Sets the last written locations for this context.

Parameters: locations the locations to set

Definition at line 200 of file write_location_context.cpp.

◆ update_location_context_internal()

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

overrideprivatevirtual

Implements context_abstract_objectt.

Definition at line 186 of file write_location_context.cpp.

◆ write()

abstract_object_pointert write_location_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

overrideprotectedvirtual

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 35 of file write_location_context.cpp.

Member Data Documentation

◆ last_written_locations

locationst write_location_contextt::last_written_locations

private

Definition at line 105 of file write_location_context.h.

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

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