#include <interval_abstract_value.h>

Inheritance diagram for interval_abstract_valuet:

Collaboration diagram for interval_abstract_valuet:

Public Member Functions
	interval_abstract_valuet (const typet &t, bool tp, bool bttm)

	interval_abstract_valuet (const constant_interval_exprt &e)

	interval_abstract_valuet (const exprt &lower, const exprt &upper)

	interval_abstract_valuet (const exprt &e, const abstract_environmentt &environment, const namespacet &ns)

	~interval_abstract_valuet () override=default

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

size_t	internal_hash () const override

bool	internal_equality (const abstract_object_pointert &other) const override

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

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.

Static Public Member Functions
template<typename... Args>
static std::shared_ptr< interval_abstract_valuet >	make_interval (Args &&... args)

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 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
	Merge another interval abstract object with this one.

abstract_object_pointert	meet_with_value (const abstract_value_pointert &other) const override
	Meet another interval abstract object with this one.

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

Private Attributes
constant_interval_exprt	interval

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 21 of file interval_abstract_value.h.

Constructor & Destructor Documentation

◆ interval_abstract_valuet() [1/4]

interval_abstract_valuet::interval_abstract_valuet	(	const typet &	t,
		bool	tp,
		bool	bttm
	)

Definition at line 229 of file interval_abstract_value.cpp.

◆ interval_abstract_valuet() [2/4]

interval_abstract_valuet::interval_abstract_valuet ( const constant_interval_exprt & e )

explicit

Definition at line 252 of file interval_abstract_value.cpp.

◆ interval_abstract_valuet() [3/4]

interval_abstract_valuet::interval_abstract_valuet	(	const exprt &	lower,
		const exprt &	upper
	)

Definition at line 259 of file interval_abstract_value.cpp.

◆ interval_abstract_valuet() [4/4]

interval_abstract_valuet::interval_abstract_valuet	(	const exprt &	e,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

Definition at line 266 of file interval_abstract_value.cpp.

◆ ~interval_abstract_valuet()

interval_abstract_valuet::~interval_abstract_valuet ( )

overridedefault

Member Function Documentation

◆ constrain()

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

overridevirtual

Implements abstract_value_objectt.

Definition at line 441 of file interval_abstract_value.cpp.

◆ get_statistics()

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

overridevirtual

Reimplemented from abstract_objectt.

Definition at line 469 of file interval_abstract_value.cpp.

◆ index_range_implementation()

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

overridevirtual

Implements abstract_value_objectt.

Definition at line 421 of file interval_abstract_value.cpp.

◆ internal_equality()

bool interval_abstract_valuet::internal_equality ( const abstract_object_pointert & other ) const

overridevirtual

Reimplemented from abstract_objectt.

Definition at line 309 of file interval_abstract_value.cpp.

◆ internal_hash()

size_t interval_abstract_valuet::internal_hash ( ) const

overridevirtual

Reimplemented from abstract_objectt.

Definition at line 304 of file interval_abstract_value.cpp.

◆ make_interval()

template<typename... Args>

static std::shared_ptr< interval_abstract_valuet > interval_abstract_valuet::make_interval ( Args &&... args )

inlinestatic

Definition at line 36 of file interval_abstract_value.h.

◆ meet_with_value()

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

overrideprotectedvirtual

Meet another interval abstract object with this one.

Parameters

other The interval abstract object to meet with

Returns: This if the other interval subsumes this, other if this subsumes other. Otherwise, a new interval abstract object with the intersection interval (of this and other)

Implements abstract_value_objectt.

Definition at line 397 of file interval_abstract_value.cpp.

◆ merge_with_value()

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

overrideprotectedvirtual

Merge another interval abstract object with this one.

Parameters

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

Returns: This if the other interval is subsumed by this, other if this is subsumed by other. Otherwise, a new interval abstract object with the smallest interval that subsumes both this and other

Implements abstract_value_objectt.

Definition at line 371 of file interval_abstract_value.cpp.

◆ mutable_clone()

internal_abstract_object_pointert interval_abstract_valuet::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 73 of file interval_abstract_value.h.

◆ output()

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

override

Definition at line 317 of file interval_abstract_value.cpp.

◆ set_top_internal()

void interval_abstract_valuet::set_top_internal ( )

overrideprivatevirtual

Reimplemented from abstract_objectt.

Definition at line 299 of file interval_abstract_value.cpp.

◆ to_constant()

exprt interval_abstract_valuet::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 278 of file interval_abstract_value.cpp.

◆ to_interval()

constant_interval_exprt interval_abstract_valuet::to_interval ( ) const

inlineoverridevirtual

Implements abstract_value_objectt.

Definition at line 50 of file interval_abstract_value.h.

◆ to_predicate_internal()

exprt interval_abstract_valuet::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 458 of file interval_abstract_value.cpp.

◆ value_range_implementation()

value_range_implementation_ptrt interval_abstract_valuet::value_range_implementation ( ) const

overridevirtual

Implements abstract_value_objectt.

Definition at line 436 of file interval_abstract_value.cpp.

Member Data Documentation

◆ interval

constant_interval_exprt interval_abstract_valuet::interval

private

Definition at line 99 of file interval_abstract_value.h.

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

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

Public Member Functions

Static Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ interval_abstract_valuet() [1/4]

◆ interval_abstract_valuet() [2/4]

◆ interval_abstract_valuet() [3/4]

◆ interval_abstract_valuet() [4/4]

◆ ~interval_abstract_valuet()

Member Function Documentation

◆ constrain()

◆ get_statistics()

◆ index_range_implementation()

◆ internal_equality()

◆ internal_hash()

◆ make_interval()

◆ meet_with_value()

◆ merge_with_value()

◆ mutable_clone()

◆ output()

◆ set_top_internal()

◆ to_constant()

◆ to_interval()

◆ to_predicate_internal()

◆ value_range_implementation()

Member Data Documentation

◆ interval