#include <abstract_value_object.h>

Inheritance diagram for abstract_value_objectt:

Collaboration diagram for abstract_value_objectt:

Public Member Functions
	abstract_value_objectt (const typet &type, bool tp, bool bttm)

	abstract_value_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

index_ranget	index_range (const namespacet &ns) const

value_ranget	value_range () const

virtual constant_interval_exprt	to_interval () const =0

abstract_object_pointert	expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
	Interface for transforms. More...

virtual sharing_ptrt< const abstract_value_objectt >	constrain (const exprt &lower, const exprt &upper) const =0

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 final
	A helper function to evaluate writing to a component of an abstract object. More...

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 const typet &	type () const
	Get the real type of the variable this abstract object is representing. More...

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

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

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

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

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

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

virtual void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
	Print the value of the abstract object. More...

virtual bool	has_been_modified (const abstract_object_pointert &before) const
	Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More...

virtual abstract_object_pointert	write_location_context (const locationt &location) const
	Update the write location context for an abstract object. 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	unwrap_context () 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

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

Protected Types
using	abstract_value_pointert = sharing_ptrt< const abstract_value_objectt >

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
abstract_object_pointert	merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const final
	Attempts to do a value/value merge if both are constants, otherwise falls back to the parent merge. More...

abstract_object_pointert	meet (const abstract_object_pointert &other) const final
	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_with_value (const abstract_value_pointert &other, const widen_modet &widen_mode) const =0

virtual abstract_object_pointert	meet_with_value (const abstract_value_pointert &other) const =0

virtual index_range_implementation_ptrt	index_range_implementation (const namespacet &ns) const =0

virtual value_range_implementation_ptrt	value_range_implementation () const =0

sharing_ptrt< const abstract_value_objectt >	as_value (const abstract_object_pointert &obj) const

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

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

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 239 of file abstract_value_object.h.

Member Typedef Documentation

◆ abstract_value_pointert

using abstract_value_objectt::abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>

protected

Definition at line 298 of file abstract_value_object.h.

Constructor & Destructor Documentation

◆ abstract_value_objectt() [1/2]

abstract_value_objectt::abstract_value_objectt	(	const typet &	type,
		bool	tp,
		bool	bttm
	)

inline

Definition at line 243 of file abstract_value_object.h.

◆ abstract_value_objectt() [2/2]

abstract_value_objectt::abstract_value_objectt	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

inline

Definition at line 248 of file abstract_value_object.h.

Member Function Documentation

◆ as_value()

abstract_value_pointert abstract_value_objectt::as_value ( const abstract_object_pointert & obj ) const

protected

Definition at line 697 of file abstract_value_object.cpp.

◆ constrain()

virtual sharing_ptrt<const abstract_value_objectt> abstract_value_objectt::constrain	(	const exprt &	lower,
		const exprt &	upper
	)		const

pure virtual

Implemented in value_set_abstract_objectt, interval_abstract_valuet, and constant_abstract_valuet.

◆ expression_transform()

abstract_object_pointert abstract_value_objectt::expression_transform	(	const exprt &	expr,
		const std::vector< abstract_object_pointert > &	operands,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)		const

finalvirtual

Interface for transforms.

Parameters

expr	the expression to evaluate and find the result of it. This will be the symbol referred to be op0()
operands	an abstract_object (pointer) that represent the possible values of each operand
environment	the abstract environment in which the expression is being evaluated
ns	the current variable namespace

Returns: Returns the abstract_object representing the result of this expression to the maximum precision available.

Reimplemented from abstract_objectt.

Definition at line 172 of file abstract_value_object.cpp.

◆ index_range()

index_ranget abstract_value_objectt::index_range ( const namespacet & ns ) const

inline

Definition at line 256 of file abstract_value_object.h.

◆ index_range_implementation()

virtual index_range_implementation_ptrt abstract_value_objectt::index_range_implementation ( const namespacet & ns ) const

protectedpure virtual

Implemented in value_set_abstract_objectt, interval_abstract_valuet, and constant_abstract_valuet.

◆ meet()

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

finalprotectedvirtual

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 205 of file abstract_value_object.cpp.

◆ meet_with_value()

virtual abstract_object_pointert abstract_value_objectt::meet_with_value ( const abstract_value_pointert & other ) const

protectedpure virtual

Implemented in value_set_abstract_objectt, interval_abstract_valuet, and constant_abstract_valuet.

◆ merge()

abstract_object_pointert abstract_value_objectt::merge	(	const abstract_object_pointert &	other,
		const widen_modet &	widen_mode
	)		const

finalprotectedvirtual

Attempts to do a value/value merge if both are constants, otherwise falls back to the parent merge.

Parameters

other	the abstract object to merge with
widen_mode	Indicates if this is a widening merge

Returns: Returns the result of the merge

Reimplemented from abstract_objectt.

Definition at line 192 of file abstract_value_object.cpp.

◆ merge_with_value()

virtual abstract_object_pointert abstract_value_objectt::merge_with_value	(	const abstract_value_pointert &	other,
		const widen_modet &	widen_mode
	)		const

protectedpure virtual

Implemented in value_set_abstract_objectt, interval_abstract_valuet, and constant_abstract_valuet.

◆ to_interval()

virtual constant_interval_exprt abstract_value_objectt::to_interval ( ) const

pure virtual

Implemented in value_set_abstract_objectt, interval_abstract_valuet, and constant_abstract_valuet.

◆ value_range()

value_ranget abstract_value_objectt::value_range ( ) const

inline

Definition at line 261 of file abstract_value_object.h.

◆ value_range_implementation()

virtual value_range_implementation_ptrt abstract_value_objectt::value_range_implementation ( ) const

protectedpure virtual

Implemented in value_set_abstract_objectt, interval_abstract_valuet, and constant_abstract_valuet.

◆ write()

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

finalvirtual

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.

Definition at line 181 of file abstract_value_object.cpp.

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

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

Public Member Functions

Protected Types

Protected Member Functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ abstract_value_pointert

Constructor & Destructor Documentation

◆ abstract_value_objectt() [1/2]

◆ abstract_value_objectt() [2/2]

Member Function Documentation

◆ as_value()

◆ constrain()

◆ expression_transform()

◆ index_range()

◆ index_range_implementation()

◆ meet()

◆ meet_with_value()

◆ merge()

◆ merge_with_value()

◆ to_interval()

◆ value_range()

◆ value_range_implementation()

◆ write()