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}.

virtual abstract_object_pointert merge_location_context (const locationt &location) const

Update the merge location context for an abstract object.

abstract_object_pointert make_top () const

abstract_object_pointert clear_top () const

virtual abstract_object_pointert visit_sub_elements (const abstract_object_visitort &visitor) const

Apply a visitor operation to all sub elements of this abstract_object.

virtual size_t internal_hash () const

virtual bool internal_equality (const abstract_object_pointert &other) const

Protected Types

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 Member Functions

void set_child (const abstract_object_pointert &child)

void set_top_internal () override

void set_not_top_internal () override

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.

bool has_been_modified (const abstract_object_pointert &before) const override

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

exprt to_predicate_internal (const exprt &name) const override

to_predicate implementation - derived classes will override

virtual context_abstract_object_ptrt update_location_context_internal (const locationst &locations) const =0

- Protected Member Functions inherited from abstract_objectt

virtual internal_abstract_object_pointert mutable_clone () const

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.

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

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

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

Protected Attributes

abstract_object_pointert child_abstract_object

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.

Detailed Description

Definition at line 21 of file context_abstract_object.h.

Member Typedef Documentation

◆ context_abstract_object_ptrt

using context_abstract_objectt::context_abstract_object_ptrt = std::shared_ptr<context_abstract_objectt>

protected

Definition at line 102 of file context_abstract_object.h.

◆ locationst

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

protected

Definition at line 127 of file context_abstract_object.h.

Constructor & Destructor Documentation

◆ context_abstract_objectt() [1/2]

context_abstract_objectt::context_abstract_objectt ( const abstract_object_pointert child,

const typet & type,

bool top,

bool bottom

)

inline

Definition at line 26 of file context_abstract_object.h.

◆ context_abstract_objectt() [2/2]

context_abstract_objectt::context_abstract_objectt ( const abstract_object_pointert child,

const exprt & expr,

const abstract_environmentt & environment,

const namespacet & ns

)

inlineexplicit

Definition at line 36 of file context_abstract_object.h.

◆ ~context_abstract_objectt()

virtual context_abstract_objectt::~context_abstract_objectt ( )

inlinevirtual

Definition at line 46 of file context_abstract_object.h.

Member Function Documentation

◆ envelop()

abstract_object_pointert context_abstract_objectt::envelop ( abstract_object_pointert & child ) const

Definition at line 120 of file context_abstract_object.cpp.

◆ expression_transform()

abstract_object_pointert context_abstract_objectt::expression_transform ( const exprt & expr,

const std::vector< abstract_object_pointert > & operands,

const abstract_environmentt & environment,

const namespacet & ns

) const

overridevirtual

Try to resolve an expression with the maximum level of precision available.

Parameters: expr the expression to evaluate and find the result of. This will be the symbol referred to be op0()

operands the operands to use instead of expr.operands()

environment the abstract environment in which to resolve 'expr'

ns the current namespace

Returns: the resolved expression

Reimplemented from abstract_objectt.

Definition at line 83 of file context_abstract_object.cpp.

◆ get_child()

abstract_object_pointert context_abstract_objectt::get_child ( ) const

Definition at line 15 of file context_abstract_object.cpp.

◆ get_statistics()

void context_abstract_objectt::get_statistics ( abstract_object_statisticst & statistics,

abstract_object_visitedt & visited,

const abstract_environmentt & env,

const namespacet & ns

) const

overridevirtual

Reimplemented from abstract_objectt.

Definition at line 179 of file context_abstract_object.cpp.

◆ has_been_modified()

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

overrideprotectedvirtual

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 abstract_objectt.

Reimplemented in data_dependency_contextt, and write_location_contextt.

Definition at line 157 of file context_abstract_object.cpp.

◆ is_bottom()

bool context_abstract_objectt::is_bottom ( ) const

inlineoverridevirtual

Find out if the abstract object is bottom.

Returns: Returns true if the abstract object is representing the bottom.

Reimplemented from abstract_objectt.

Definition at line 60 of file context_abstract_object.h.

◆ is_top()

bool context_abstract_objectt::is_top ( ) const

inlineoverridevirtual

Find out if the abstract object is top.

Returns: Returns true if the abstract object is representing the top (i.e. we don't know anything about the value).

Reimplemented from abstract_objectt.

Definition at line 55 of file context_abstract_object.h.

◆ output()

void context_abstract_objectt::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 abstract_objectt.

Reimplemented in data_dependency_contextt, liveness_contextt, and write_location_contextt.

Definition at line 141 of file context_abstract_object.cpp.

◆ set_child()

void context_abstract_objectt::set_child ( const abstract_object_pointert & child )

protected

Definition at line 20 of file context_abstract_object.cpp.

◆ set_not_top_internal()

void context_abstract_objectt::set_not_top_internal ( )

overrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 31 of file context_abstract_object.cpp.

◆ set_top_internal()

void context_abstract_objectt::set_top_internal ( )

overrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 25 of file context_abstract_object.cpp.

◆ to_constant()

exprt context_abstract_objectt::to_constant ( ) const

inlineoverridevirtual

Converts to a constant expression if possible.

Returns: Returns an exprt representing the value if the value is known and constant. Otherwise returns the nil expression

If abstract element represents a single value, then that value, otherwise nil. E.G. if it is an interval then this will be x if it is [x,x] This is the (sort of) dual to the constant_exprt constructor that allows an object to be built from a value.

Reimplemented from abstract_objectt.

Definition at line 65 of file context_abstract_object.h.

◆ to_predicate_internal()

exprt context_abstract_objectt::to_predicate_internal ( const exprt & name ) const

overrideprotectedvirtual

to_predicate implementation - derived classes will override

Parameters: name - the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

Reimplemented from abstract_objectt.

Definition at line 174 of file context_abstract_object.cpp.

◆ type()

const typet & context_abstract_objectt::type ( ) const

inlineoverridevirtual

Get the real type of the variable this abstract object is representing.

Returns: The program type this abstract object represents

Reimplemented from abstract_objectt.

Definition at line 50 of file context_abstract_object.h.

◆ unwrap_context()

abstract_object_pointert context_abstract_objectt::unwrap_context ( ) const

overridevirtual

Reimplemented from abstract_objectt.

Definition at line 169 of file context_abstract_object.cpp.

◆ update_location_context_internal()

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

protectedpure virtual

Implemented in data_dependency_contextt, liveness_contextt, and write_location_contextt.

◆ write()

abstract_object_pointert context_abstract_objectt::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 abstract_objectt.

Reimplemented in data_dependency_contextt, liveness_contextt, and write_location_contextt.

Definition at line 53 of file context_abstract_object.cpp.

◆ write_location_context()

abstract_object_pointert context_abstract_objectt::write_location_context ( const locationt & location ) const

overridevirtual

Update the location context for an abstract object.

Parameters: location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented from abstract_objectt.

Definition at line 108 of file context_abstract_object.cpp.

Member Data Documentation

◆ child_abstract_object

abstract_object_pointert context_abstract_objectt::child_abstract_object

protected

Definition at line 106 of file context_abstract_object.h.

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

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