#include <context_abstract_object.h>

Inheritance diagram for context_abstract_objectt:

Collaboration diagram for context_abstract_objectt:

Public Member Functions
	context_abstract_objectt (const abstract_object_pointert child, const typet &type, bool top, bool bottom)

	context_abstract_objectt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

virtual	~context_abstract_objectt ()

const typet &	type () const override
	Get the real type of the variable this abstract object is representing. More...

bool	is_top () const override
	Find out if the abstract object is top. More...

bool	is_bottom () const override
	Find out if the abstract object is bottom. More...

exprt	to_constant () const override
	Converts to a constant expression if possible. More...

abstract_object_pointert	expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
	Try to resolve an expression with the maximum level of precision available. More...

abstract_object_pointert	write_location_context (const locationt &location) const override
	Update the location context for an abstract object. More...

void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
	Output a representation of the value of this abstract object. More...

abstract_object_pointert	envelop (abstract_object_pointert &child) const

abstract_object_pointert	unwrap_context () const override

void	get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override

abstract_object_pointert	get_child () const

Public Member Functions inherited from abstract_objectt
	abstract_objectt (const typet &type, bool top, bool bottom)
	Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...

	abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Construct an abstract object from the expression. More...

virtual	~abstract_objectt ()

virtual bool	verify () const
	Verify the internal structure of an abstract_object is correct. More...

exprt	to_predicate (const exprt &name) const
	Converts to an invariant expression. More...

virtual abstract_object_pointert	meet (const abstract_object_pointert &other) const
	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}. More...

virtual abstract_object_pointert	merge_location_context (const locationt &location) const
	Update the merge location context for an abstract object. More...

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

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

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

exprt	to_predicate_internal (const exprt &name) const override
	to_predicate implementation - derived classes will override More...

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

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

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

abstract_object_pointert	abstract_object_meet (const abstract_object_pointert &other) const
	Helper function for base meet. More...

bool	should_use_base_meet (const abstract_object_pointert &other) const
	Helper function to decide if base meet implementation should be used. More...

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

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

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 write_location_contextt, and data_dependency_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 write_location_contextt, liveness_contextt, and data_dependency_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 write_location_contextt, liveness_contextt, and data_dependency_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 write_location_contextt, liveness_contextt, and data_dependency_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

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ context_abstract_object_ptrt

◆ locationst

Constructor & Destructor Documentation

◆ context_abstract_objectt() [1/2]

◆ context_abstract_objectt() [2/2]

◆ ~context_abstract_objectt()

Member Function Documentation

◆ envelop()

◆ expression_transform()

◆ get_child()

◆ get_statistics()

◆ has_been_modified()

◆ is_bottom()

◆ is_top()

◆ output()

◆ set_child()

◆ set_not_top_internal()

◆ set_top_internal()

◆ to_constant()

◆ to_predicate_internal()

◆ type()

◆ unwrap_context()

◆ update_location_context_internal()

◆ write()

◆ write_location_context()

Member Data Documentation

◆ child_abstract_object