#include <value_set_pointer_abstract_object.h>

Inheritance diagram for value_set_pointer_abstract_objectt:

Collaboration diagram for value_set_pointer_abstract_objectt:

Public Member Functions
	value_set_pointer_abstract_objectt (const typet &new_type, bool top, bool bottom, const abstract_object_sett &new_values)

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

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

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

const abstract_object_sett &	get_values () const override
	Getter for the set of stored abstract objects. More...

void	set_values (const abstract_object_sett &other_values)
	Setter for updating the stored values. More...

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 &new_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

void	output (std::ostream &out, const ai_baset &ai, 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...

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

Static Public Attributes
static const size_t	max_value_set_size = 10
	The threshold size for value-sets: past this threshold the object is either converted to interval or marked as `top`. More...

Protected Member Functions
internal_abstract_object_pointert	mutable_clone () const override

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

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

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

Private Member Functions
abstract_object_pointert	resolve_values (const abstract_object_sett &new_values) const
	Update the set of stored values to `new_values`. More...

Private Attributes
abstract_object_sett	values

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

Detailed Description

Definition at line 18 of file value_set_pointer_abstract_object.h.

Constructor & Destructor Documentation

◆ value_set_pointer_abstract_objectt() [1/3]

value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt	(	const typet &	new_type,
		bool	top,
		bool	bottom,
		const abstract_object_sett &	new_values
	)

Definition at line 33 of file value_set_pointer_abstract_object.cpp.

◆ value_set_pointer_abstract_objectt() [2/3]

value_set_pointer_abstract_objectt::value_set_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 42 of file value_set_pointer_abstract_object.cpp.

◆ value_set_pointer_abstract_objectt() [3/3]

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

Definition at line 52 of file value_set_pointer_abstract_object.cpp.

Member Function Documentation

◆ get_values()

const abstract_object_sett& value_set_pointer_abstract_objectt::get_values ( ) const

inlineoverridevirtual

Getter for the set of stored abstract objects.

Returns: the values represented by this abstract object

Implements value_set_tag.

Definition at line 46 of file value_set_pointer_abstract_object.h.

◆ merge()

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

overrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 213 of file value_set_pointer_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert value_set_pointer_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 91 of file value_set_pointer_abstract_object.h.

◆ output()

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

override

Definition at line 255 of file value_set_pointer_abstract_object.cpp.

◆ ptr_comparison_expr()

exprt value_set_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 160 of file value_set_pointer_abstract_object.cpp.

◆ ptr_diff()

abstract_object_pointert value_set_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 127 of file value_set_pointer_abstract_object.cpp.

◆ read_dereference()

abstract_object_pointert value_set_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 62 of file value_set_pointer_abstract_object.cpp.

◆ resolve_values()

abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values ( const abstract_object_sett & new_values ) const

private

Update the set of stored values to new_values.

Build a new abstract object of the right type if necessary.

Parameters

new_values potentially new set of values

Returns: the abstract object representing new_values (either 'this' or something new)

Definition at line 189 of file value_set_pointer_abstract_object.cpp.

◆ set_values()

void value_set_pointer_abstract_objectt::set_values ( const abstract_object_sett & other_values )

Setter for updating the stored values.

Parameters

other_values the new (non-empty) set of values

Definition at line 247 of file value_set_pointer_abstract_object.cpp.

◆ to_constant()

exprt value_set_pointer_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 37 of file value_set_pointer_abstract_object.h.

◆ to_predicate_internal()

exprt value_set_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 228 of file value_set_pointer_abstract_object.cpp.

◆ typecast()

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

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 107 of file value_set_pointer_abstract_object.cpp.

◆ write_dereference()

abstract_object_pointert value_set_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 83 of file value_set_pointer_abstract_object.cpp.

Member Data Documentation

◆ max_value_set_size

const size_t value_set_pointer_abstract_objectt::max_value_set_size = 10

static

The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top.

Definition at line 57 of file value_set_pointer_abstract_object.h.

◆ values

abstract_object_sett value_set_pointer_abstract_objectt::values

private

Definition at line 110 of file value_set_pointer_abstract_object.h.

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

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

Public Member Functions

Static Public Attributes

Protected Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ value_set_pointer_abstract_objectt() [1/3]

◆ value_set_pointer_abstract_objectt() [2/3]

◆ value_set_pointer_abstract_objectt() [3/3]

Member Function Documentation

◆ get_values()

◆ merge()

◆ mutable_clone()

◆ output()

◆ ptr_comparison_expr()

◆ ptr_diff()

◆ read_dereference()

◆ resolve_values()

◆ set_values()

◆ to_constant()

◆ to_predicate_internal()

◆ typecast()

◆ write_dereference()

Member Data Documentation

◆ max_value_set_size

◆ values