#include <two_value_pointer_abstract_object.h>

Inheritance diagram for two_value_pointer_abstract_objectt:

Collaboration diagram for two_value_pointer_abstract_objectt:

Public Member Functions
	two_value_pointer_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...

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

abstract_object_pointert	read_dereference (const abstract_environmentt &env, const namespacet &ns) const override
	A helper function to read elements from an array. More...

abstract_object_pointert	write_dereference (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const override
	Evaluate writing to a pointer's value. More...

abstract_object_pointert	typecast (const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const override

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

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

Public Member Functions inherited from abstract_pointer_objectt
	abstract_pointer_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_pointer_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

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

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

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

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

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

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

Detailed Description

Definition at line 13 of file two_value_pointer_abstract_object.h.

Constructor & Destructor Documentation

◆ two_value_pointer_abstract_objectt() [1/2]

two_value_pointer_abstract_objectt::two_value_pointer_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.

Parameters

type	the type the abstract_object is representing
top	is the abstract_object starting as top
bottom	is the abstract_object starting as bottom

Definition at line 14 of file two_value_pointer_abstract_object.cpp.

◆ two_value_pointer_abstract_objectt() [2/2]

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

Parameters

expr	the expression to use as the starting pointer for an abstract object
environment	the environment in which the pointer is being created
ns	the current namespace

Definition at line 22 of file two_value_pointer_abstract_object.cpp.

Member Function Documentation

◆ ptr_comparison_expr()

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

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 76 of file two_value_pointer_abstract_object.cpp.

◆ ptr_diff()

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

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 67 of file two_value_pointer_abstract_object.cpp.

◆ read_dereference()

abstract_object_pointert two_value_pointer_abstract_objectt::read_dereference	(	const abstract_environmentt &	env,
		const namespacet &	ns
	)		const

overridevirtual

A helper function to read elements from an array.

More precise abstractions may override this to provide more precise results.

Parameters

env	the environment
ns	the namespace

Returns: An abstract object representing the value being pointed to

Implements abstract_pointer_objectt.

Definition at line 30 of file two_value_pointer_abstract_object.cpp.

◆ typecast()

abstract_object_pointert two_value_pointer_abstract_objectt::typecast	(	const typet &	new_type,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)		const

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 57 of file two_value_pointer_abstract_object.cpp.

◆ write_dereference()

abstract_object_pointert two_value_pointer_abstract_objectt::write_dereference	(	abstract_environmentt &	environment,
		const namespacet &	ns,
		const std::stack< exprt > &	stack,
		const abstract_object_pointert &	value,
		bool	merging_write
	)		const

overridevirtual

Evaluate writing to a pointer's value.

More precise abstractions may override this provide more precise results.

Parameters

environment	the abstract environment
ns	the namespace
stack	the remaining stack of expressions on the LHS to evaluate
value	the value we are trying to assign to what the pointer is pointing to
merging_write	is it a merging write (i.e. we aren't certain we are writing to this particular pointer therefore the value should be merged with whatever is already there or we are certain we are writing to this pointer so therefore the value can be replaced

Returns: A modified abstract object representing this pointer after it has been written to.

Implements abstract_pointer_objectt.

Definition at line 40 of file two_value_pointer_abstract_object.cpp.

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

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

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ two_value_pointer_abstract_objectt() [1/2]

◆ two_value_pointer_abstract_objectt() [2/2]

Member Function Documentation

◆ ptr_comparison_expr()

◆ ptr_diff()

◆ read_dereference()

◆ typecast()

◆ write_dereference()