#include <constant_pointer_abstract_object.h>

Inheritance diagram for constant_pointer_abstract_objectt:

Collaboration diagram for constant_pointer_abstract_objectt:

Public Member Functions
	constant_pointer_abstract_objectt (const typet &type, bool top, bool bottom)

	constant_pointer_abstract_objectt (const typet &type, const constant_pointer_abstract_objectt &old)

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

exprt	to_constant () const override
	To try and find a constant expression for this abstract object.

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
	Print the value of the pointer.

abstract_object_pointert	read_dereference (const abstract_environmentt &env, const namespacet &ns) const override
	A helper function to dereference a value from a pointer.

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
	A helper function to evaluate writing to a pointers value.

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

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

	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.

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.

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.

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

virtual	~abstract_objectt ()

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

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

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

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

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

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

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.

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

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

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

virtual size_t	internal_hash () const

virtual bool	internal_equality (const abstract_object_pointert &other) const

Protected Member Functions
abstract_object_pointert	merge (const abstract_object_pointert &op1, const widen_modet &widen_mode) const override
	Set this abstract object to be the result of merging this abstract object.

internal_abstract_object_pointert	mutable_clone () const 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 ()

Private Types
typedef sharing_ptrt< constant_pointer_abstract_objectt >	constant_pointer_abstract_pointert

Private Member Functions
bool	same_target (abstract_object_pointert other) const

exprt	offset () const

exprt	offset_from (abstract_object_pointert other) const

abstract_object_pointert	merge_constant_pointers (const constant_pointer_abstract_pointert &other, const widen_modet &widen_mode) const
	Merges two constant pointers.

Private Attributes
write_stackt	value_stack

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 abstract_objectt
template<class T >
using	internal_sharing_ptrt = std::shared_ptr< T >

typedef internal_sharing_ptrt< class abstract_objectt >	internal_abstract_object_pointert

Detailed Description

Definition at line 19 of file constant_pointer_abstract_object.h.

Member Typedef Documentation

◆ constant_pointer_abstract_pointert

typedef sharing_ptrt<constant_pointer_abstract_objectt> constant_pointer_abstract_objectt::constant_pointer_abstract_pointert

private

Definition at line 23 of file constant_pointer_abstract_object.h.

Constructor & Destructor Documentation

◆ constant_pointer_abstract_objectt() [1/3]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt	(	const typet &	type,
		bool	top,
		bool	bottom
	)

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

Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true

Definition at line 22 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [2/3]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt	(	const typet &	type,
		const constant_pointer_abstract_objectt &	old
	)

Definition at line 31 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [3/3]

constant_pointer_abstract_objectt::constant_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 we evaluate expr
ns	the current namespace

Definition at line 39 of file constant_pointer_abstract_object.cpp.

Member Function Documentation

◆ get_statistics()

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

overridevirtual

Reimplemented from abstract_pointer_objectt.

Definition at line 286 of file constant_pointer_abstract_object.cpp.

◆ merge()

abstract_object_pointert constant_pointer_abstract_objectt::merge	(	const abstract_object_pointert &	op1,
		const widen_modet &	widen_mode
	)		const

overrideprotectedvirtual

Set this abstract object to be the result of merging this abstract object.

This calls the merge_constant_pointers if we are trying to merge a constant pointer we use the constant pointer constant pointer merge

Parameters

op1	the pointer being merged
widen_mode	Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 57 of file constant_pointer_abstract_object.cpp.

◆ merge_constant_pointers()

abstract_object_pointert constant_pointer_abstract_objectt::merge_constant_pointers	(	const constant_pointer_abstract_pointert &	other,
		const widen_modet &	widen_mode
	)		const

private

Merges two constant pointers.

If they are pointing at the same value, we merge, otherwise we set to top.

Parameters

other	the pointer being merged
widen_mode	Indicates if this is a widening merge

Returns: Returns a new abstract object that is the result of the merge unless the merge is the same as this abstract object, in which case it returns this.

Definition at line 112 of file constant_pointer_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert constant_pointer_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 143 of file constant_pointer_abstract_object.h.

◆ offset()

exprt constant_pointer_abstract_objectt::offset ( ) const

private

Definition at line 90 of file constant_pointer_abstract_object.cpp.

◆ offset_from()

exprt constant_pointer_abstract_objectt::offset_from ( abstract_object_pointert other ) const

private

Definition at line 97 of file constant_pointer_abstract_object.cpp.

◆ output()

void constant_pointer_abstract_objectt::output	(	std::ostream &	out,
		const ai_baset &	ai,
		const namespacet &	ns
	)		const

override

Print the value of the pointer.

Either NULL if nullpointer or ptr -> ( output of what the pointer is pointing to).

Parameters

out	the stream to write to
ai	the domain in which this object appears given as ai_baset so that the interface is the same across all domains
ns	the current namespace

Definition at line 142 of file constant_pointer_abstract_object.cpp.

◆ ptr_comparison_expr()

exprt constant_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 353 of file constant_pointer_abstract_object.cpp.

◆ ptr_diff()

abstract_object_pointert constant_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 301 of file constant_pointer_abstract_object.cpp.

◆ read_dereference()

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

overridevirtual

A helper function to dereference a value from a pointer.

Providing the pointer can only be pointing at one thing, returns an abstract object representing that thing. If null or top will return top.

Parameters

env	the environment
ns	the namespace

Returns: An abstract object representing the value this pointer is pointing to

Implements abstract_pointer_objectt.

Definition at line 189 of file constant_pointer_abstract_object.cpp.

◆ same_target()

bool constant_pointer_abstract_objectt::same_target ( abstract_object_pointert other ) const

private

Definition at line 69 of file constant_pointer_abstract_object.cpp.

◆ to_constant()

exprt constant_pointer_abstract_objectt::to_constant ( ) const

overridevirtual

To try and find a constant expression for this abstract object.

Returns: Returns an expression representing the value if it can. Returns a nil expression if it can be more than one value. Returns null_pointer expression if it must be null Returns an address_of_exprt with the value set to the result of to_constant called on whatever abstract object this pointer is pointing to.

Reimplemented from abstract_objectt.

Definition at line 128 of file constant_pointer_abstract_object.cpp.

◆ to_predicate_internal()

exprt constant_pointer_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 387 of file constant_pointer_abstract_object.cpp.

◆ typecast()

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

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 257 of file constant_pointer_abstract_object.cpp.

◆ write_dereference()

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

A helper function to evaluate writing to a pointers value.

If the pointer can only be pointing to one element that it overwrites that element (or merges if merging_write) with the new value. If don't know what we are pointing to, we delegate to the parent.

Parameters

environment	the environment
ns	the namespace
stack	the remaining stack
value	the value to write to the dereferenced pointer
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 207 of file constant_pointer_abstract_object.cpp.

Member Data Documentation

◆ value_stack

write_stackt constant_pointer_abstract_objectt::value_stack

private

Definition at line 165 of file constant_pointer_abstract_object.h.

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

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

Public Member Functions

Protected Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ constant_pointer_abstract_pointert

Constructor & Destructor Documentation

◆ constant_pointer_abstract_objectt() [1/3]

◆ constant_pointer_abstract_objectt() [2/3]

◆ constant_pointer_abstract_objectt() [3/3]

Member Function Documentation

◆ get_statistics()

◆ merge()

◆ merge_constant_pointers()

◆ mutable_clone()

◆ offset()

◆ offset_from()

◆ output()

◆ ptr_comparison_expr()

◆ ptr_diff()

◆ read_dereference()

◆ same_target()

◆ to_constant()

◆ to_predicate_internal()

◆ typecast()

◆ write_dereference()

Member Data Documentation

◆ value_stack