#include <value_set_abstract_object.h>

Inheritance diagram for value_set_abstract_objectt:

Collaboration diagram for value_set_abstract_objectt:

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

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

index_range_implementation_ptrt	index_range_implementation (const namespacet &ns) const override

value_range_implementation_ptrt	value_range_implementation () const override

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

constant_interval_exprt	to_interval () const override

abstract_value_pointert	constrain (const exprt &lower, const exprt &upper) const override

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

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

Public Member Functions inherited from abstract_value_objectt
	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

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.

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.

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.

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

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

Static Public Member Functions
static abstract_object_pointert	make_value_set (const abstract_object_sett &initial_values)

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.

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

Protected Member Functions
internal_abstract_object_pointert	mutable_clone () const override

abstract_object_pointert	merge_with_value (const abstract_value_pointert &other, const widen_modet &widen_mode) const override

abstract_object_pointert	meet_with_value (const abstract_value_pointert &other) const override

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

Protected Member Functions inherited from abstract_value_objectt
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.

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

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

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 Member Functions
void	set_values (const abstract_object_sett &other_values)
	Setter for updating the stored values.

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

void	set_top_internal () override

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

Protected Types inherited from abstract_value_objectt
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

Detailed Description

Definition at line 18 of file value_set_abstract_object.h.

Constructor & Destructor Documentation

◆ value_set_abstract_objectt() [1/2]

value_set_abstract_objectt::value_set_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 129 of file value_set_abstract_object.cpp.

◆ value_set_abstract_objectt() [2/2]

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

Definition at line 139 of file value_set_abstract_object.cpp.

Member Function Documentation

◆ constrain()

abstract_value_pointert value_set_abstract_objectt::constrain	(	const exprt &	lower,
		const exprt &	upper
	)		const

overridevirtual

Implements abstract_value_objectt.

Definition at line 309 of file value_set_abstract_object.cpp.

◆ get_values()

const abstract_object_sett & value_set_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 47 of file value_set_abstract_object.h.

◆ index_range_implementation()

index_range_implementation_ptrt value_set_abstract_objectt::index_range_implementation ( const namespacet & ns ) const

overridevirtual

Implements abstract_value_objectt.

Definition at line 167 of file value_set_abstract_object.cpp.

◆ make_value_set()

abstract_object_pointert value_set_abstract_objectt::make_value_set ( const abstract_object_sett & initial_values )

static

Definition at line 150 of file value_set_abstract_object.cpp.

◆ meet_with_value()

abstract_object_pointert value_set_abstract_objectt::meet_with_value ( const abstract_value_pointert & other ) const

overrideprotectedvirtual

Implements abstract_value_objectt.

Definition at line 236 of file value_set_abstract_object.cpp.

◆ merge_with_value()

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

overrideprotectedvirtual

Implements abstract_value_objectt.

Definition at line 209 of file value_set_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert value_set_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 60 of file value_set_abstract_object.h.

◆ output()

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

override

Definition at line 352 of file value_set_abstract_object.cpp.

◆ resolve_values()

abstract_object_pointert value_set_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 274 of file value_set_abstract_object.cpp.

◆ set_top_internal()

void value_set_abstract_objectt::set_top_internal ( )

overrideprivatevirtual

Reimplemented from abstract_objectt.

Definition at line 285 of file value_set_abstract_object.cpp.

◆ set_values()

void value_set_abstract_objectt::set_values ( const abstract_object_sett & other_values )

private

Setter for updating the stored values.

Parameters

other_values the new (non-empty) set of values

Definition at line 292 of file value_set_abstract_object.cpp.

◆ to_constant()

exprt value_set_abstract_objectt::to_constant ( ) const

overridevirtual

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 190 of file value_set_abstract_object.cpp.

◆ to_interval()

constant_interval_exprt value_set_abstract_objectt::to_interval ( ) const

overridevirtual

Implements abstract_value_objectt.

Definition at line 204 of file value_set_abstract_object.cpp.

◆ to_predicate_internal()

exprt value_set_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 333 of file value_set_abstract_object.cpp.

◆ value_range_implementation()

value_range_implementation_ptrt value_set_abstract_objectt::value_range_implementation ( ) const

overridevirtual

Implements abstract_value_objectt.

Definition at line 185 of file value_set_abstract_object.cpp.

Member Data Documentation

◆ max_value_set_size

const size_t value_set_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 54 of file value_set_abstract_object.h.

◆ values

abstract_object_sett value_set_abstract_objectt::values

private

Definition at line 87 of file value_set_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_abstract_object.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Public Member Functions

Static Public Member Functions

Static Public Attributes

Protected Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ value_set_abstract_objectt() [1/2]

◆ value_set_abstract_objectt() [2/2]

Member Function Documentation

◆ constrain()

◆ get_values()

◆ index_range_implementation()

◆ make_value_set()

◆ meet_with_value()

◆ merge_with_value()

◆ mutable_clone()

◆ output()

◆ resolve_values()

◆ set_top_internal()

◆ set_values()

◆ to_constant()

◆ to_interval()

◆ to_predicate_internal()

◆ value_range_implementation()

Member Data Documentation

◆ max_value_set_size

◆ values