#include <wrapped_interval.h>

Inheritance diagram for wrapped_interval:

Public Types
typedef std::function< uint64_t(uint64_t, uint64_t, uint64_t, uint64_t)>	warren_approximation_function

Public Member Functions
	wrapped_interval ()
	wrapped_interval (const type2tc &t)
BigInt	convert_to_wrap (const BigInt &b) const
void	set (bool is_upper, const BigInt &b) override
BigInt	get (bool is_upper) const override
bool	empty () const override
	Checks whether there are values that satisfy the the interval.
bool	is_top () const override
void	make_le_than (const BigInt &v) override
void	make_le_than (const wrapped_interval &rhs)
void	make_ge_than (const BigInt &v) override
void	make_ge_than (const wrapped_interval &rhs)
BigInt	get_min () const
BigInt	get_max () const
BigInt	cardinality () const
bool	contains (const BigInt &e) const override
bool	is_equal (const wrapped_interval &rhs) const
bool	is_included (const wrapped_interval &rhs) const
void	approx_union_with (const interval_templatet< BigInt > &i) override
std::vector< wrapped_interval >	ssplit () const
std::vector< wrapped_interval >	nsplit () const
bool	most_significant_bit (const BigInt &b) const
wrapped_interval	zero_extension (const type2tc &cast) const
wrapped_interval	left_shift (unsigned k) const
wrapped_interval	logical_right_shift (unsigned k) const
wrapped_interval	arithmetic_right_shift (unsigned k) const
std::pair< BigInt, BigInt >	get_interval_bounds () const
	Computes the minimum and maximum value inside the interval.
wrapped_interval	sign_extension (const type2tc &cast) const
wrapped_interval	trunc (const type2tc &cast) const
const BigInt &	get_upper_bound () const
Public Member Functions inherited from interval_templatet< BigInt >
virtual	~interval_templatet ()=default
	interval_templatet ()=default
	interval_templatet (const type2tc &)
	interval_templatet (const BigInt &x)
	interval_templatet (const BigInt &l, const BigInt &u)
BigInt	get_lower () const
BigInt	get_upper () const
BigInt	adjust (const BigInt &v) const
void	set_upper (const BigInt &b)
void	set_lower (const BigInt &b)
void	dump () const
virtual bool	is_le_than (const BigInt &a, const BigInt &b) const
bool	is_bottom () const
bool	singleton () const
	There is only one value that satisfies.
void	make_sound_le (interval_templatet< BigInt > &v)
void	join (const interval_templatet< BigInt > &i)
	Union or disjunction.
void	meet (const interval_templatet< BigInt > &i)
	Intersection or conjunction.
void	intersect_with (const interval_templatet &i)
bool	is_subseteq (const interval_templatet &other) const
virtual void	approx_union_with (const interval_templatet &i)
interval_templatet< BigInt >	interval_bitand (const interval_templatet< BigInt > &, const interval_templatet< BigInt > &) const
interval_templatet< BigInt >	interval_bitor (const interval_templatet< BigInt > &, const interval_templatet< BigInt > &) const
interval_templatet< BigInt >	interval_bitxor (const interval_templatet< BigInt > &, const interval_templatet< BigInt > &) const
interval_templatet< BigInt >	interval_logical_right_shift (const interval_templatet< BigInt > &, const interval_templatet< BigInt > &) const
interval_templatet< BigInt >	interval_left_shift (const interval_templatet< BigInt > &, const interval_templatet< BigInt > &) const
interval_templatet< BigInt >	interval_arithmetic_right_shift (const interval_templatet< BigInt > &, const interval_templatet< BigInt > &) const
bool	has_changed (const interval_templatet< BigInt > &i)
	This is just to check if a value has changed.
void	make_lower_interval ()
	Generates an interval of the form (-infinity, 0].
signed_max_or signed_max_right_shift interval_templatet< BigInt >	interval_arithmetic_right_shift (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs) const

Static Public Member Functions
static bool	is_representable (const type2tc &t)
static wrapped_interval	complement (const wrapped_interval &w)
static bool	wrapped_le (const BigInt &b, const BigInt &a, const BigInt &c, const type2tc &t)
	b <=_a c iff b -_w a <= c -_w a
static wrapped_interval	extend (const wrapped_interval &s, const wrapped_interval &t)
static wrapped_interval	gap (const wrapped_interval &s, const wrapped_interval &t)
static wrapped_interval	bigger (const wrapped_interval &s, const wrapped_interval &t)
static wrapped_interval	over_join (std::vector< wrapped_interval > &r)
	Over union.
static wrapped_interval	over_join (const wrapped_interval &s, const wrapped_interval &t)
static wrapped_interval	under_meet (const wrapped_interval &s, const wrapped_interval &t)
static std::vector< wrapped_interval >	intersection (const wrapped_interval &s, const wrapped_interval &t)
static wrapped_interval	over_meet (const wrapped_interval &s, const wrapped_interval &t)
	Over meet.
static wrapped_interval	extrapolate_to (const wrapped_interval &f1, const wrapped_interval &f2)
static wrapped_interval	north_pole (const type2tc &t)
static wrapped_interval	south_pole (const type2tc &t)
static wrapped_interval	difference (const wrapped_interval &s, const wrapped_interval &t)
static std::vector< wrapped_interval >	cut (const wrapped_interval &u)
static BigInt	trunc (const BigInt &b, unsigned k)
static wrapped_interval	cast (const wrapped_interval &old, const type2tc &new_type)
static wrapped_interval	left_shift (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	logical_right_shift (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	arithmetic_right_shift (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	equality (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	invert_bool (const wrapped_interval &i)
static wrapped_interval	not_equal (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	less_than (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	less_than_equal (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	greater_than_equal (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	greater_than (const wrapped_interval &lhs, const wrapped_interval &rhs)
static std::vector< wrapped_interval >	multiply_us (const wrapped_interval &lhs, const wrapped_interval &rhs)
static wrapped_interval	amb (const wrapped_interval &rhs)
static wrapped_interval	bitnot (const wrapped_interval &w)
static wrapped_interval	ternary_if (const wrapped_interval &cond, const wrapped_interval &true_value, const wrapped_interval &false_value)
Static Public Member Functions inherited from interval_templatet< BigInt >
static interval_templatet< BigInt >	ternary_if (const interval_templatet< BigInt > &cond, const interval_templatet< BigInt > &true_value, const interval_templatet< BigInt > &false_value)
static bool	is_representable (const type2tc &)
	Whether an interval can be built for a value of type t; when it cannot, expressions over such values evaluate to top.
static interval_templatet< BigInt >	cast (const interval_templatet< BigInt > &, const type2tc &)
static interval_templatet< BigInt >	logical_right_shift (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	left_shift (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	arithmetic_right_shift (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	bitnot (const interval_templatet< BigInt > &w)
static interval_templatet< BigInt >	equality (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	invert_bool (const interval_templatet< BigInt > &i)
static interval_templatet< BigInt >	not_equal (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	less_than (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	less_than_equal (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	greater_than_equal (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static interval_templatet< BigInt >	greater_than (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs)
static void	contract_interval_le (interval_templatet< BigInt > &a, interval_templatet< BigInt > &b)
	Computer the contraction of "a" and "b" under a <= b.

Public Attributes
bool	bottom = false
type2tc	t
Public Attributes inherited from interval_templatet< BigInt >
std::optional< BigInt >	lower
	Bound value.
std::optional< BigInt >	upper
type2tc	type
	Type to be used for shift operations.

Protected Attributes
BigInt	upper_bound

Friends
wrapped_interval	operator- (const wrapped_interval &lhs)
wrapped_interval	operator+ (const wrapped_interval &lhs, const wrapped_interval &rhs)
wrapped_interval	operator- (const wrapped_interval &lhs, const wrapped_interval &rhs)
wrapped_interval	operator* (const wrapped_interval &lhs, const wrapped_interval &rhs)
wrapped_interval	operator% (const wrapped_interval &s, const wrapped_interval &t)
wrapped_interval	operator/ (const wrapped_interval &lhs, const wrapped_interval &rhs)
wrapped_interval	operator\| (const wrapped_interval &lhs, const wrapped_interval &rhs)
wrapped_interval	operator& (const wrapped_interval &lhs, const wrapped_interval &rhs)
wrapped_interval	operator^ (const wrapped_interval &lhs, const wrapped_interval &rhs)

Member Typedef Documentation

◆ warren_approximation_function

typedef std::function<uint64_t(uint64_t, uint64_t, uint64_t, uint64_t)> wrapped_interval::warren_approximation_function

Constructor & Destructor Documentation

◆ wrapped_interval() [1/2]

wrapped_interval::wrapped_interval ( )

inline

◆ wrapped_interval() [2/2]

wrapped_interval::wrapped_interval ( const type2tc & t )

inlineexplicit

Member Function Documentation

◆ amb()

wrapped_interval wrapped_interval::amb ( const wrapped_interval & rhs )

inlinestatic

◆ approx_union_with()

void wrapped_interval::approx_union_with ( const interval_templatet< BigInt > & i )

inlineoverride

◆ arithmetic_right_shift() [1/2]

wrapped_interval wrapped_interval::arithmetic_right_shift	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ arithmetic_right_shift() [2/2]

wrapped_interval wrapped_interval::arithmetic_right_shift ( unsigned k ) const

inline

◆ bigger()

wrapped_interval wrapped_interval::bigger	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ bitnot()

wrapped_interval wrapped_interval::bitnot ( const wrapped_interval & w )

inlinestatic

◆ cardinality()

BigInt wrapped_interval::cardinality ( ) const

inline

◆ cast()

wrapped_interval wrapped_interval::cast	(	const wrapped_interval &	old,
		const type2tc &	new_type )

inlinestatic

◆ complement()

wrapped_interval wrapped_interval::complement ( const wrapped_interval & w )

inlinestatic

◆ contains()

bool wrapped_interval::contains ( const BigInt & e ) const

inlineoverridevirtual

Reimplemented from interval_templatet< BigInt >.

◆ convert_to_wrap()

BigInt wrapped_interval::convert_to_wrap ( const BigInt & b ) const

inline

◆ cut()

std::vector< wrapped_interval > wrapped_interval::cut ( const wrapped_interval & u )

inlinestatic

◆ difference()

wrapped_interval wrapped_interval::difference	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ empty()

bool wrapped_interval::empty ( ) const

inlineoverridevirtual

Checks whether there are values that satisfy the the interval.

Reimplemented from interval_templatet< BigInt >.

◆ equality()

wrapped_interval wrapped_interval::equality	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ extend()

wrapped_interval wrapped_interval::extend	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ extrapolate_to()

wrapped_interval wrapped_interval::extrapolate_to	(	const wrapped_interval &	f1,
		const wrapped_interval &	f2 )

inlinestatic

◆ gap()

wrapped_interval wrapped_interval::gap	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ get()

BigInt wrapped_interval::get ( bool is_upper ) const

inlineoverridevirtual

Reimplemented from interval_templatet< BigInt >.

◆ get_interval_bounds()

std::pair< BigInt, BigInt > wrapped_interval::get_interval_bounds ( ) const

inline

Computes the minimum and maximum value inside the interval.

Examples (signed char):

get_interval_bounds([10, 127]) --> <10, 127>
get_interval_bounds([10, 128]) --> <-128, 127>
get_interval_bounds([10, 255]) --> <-128, 127>
get_interval_bounds([129, 130]) --> <-127, -126>
get_interval_bounds([255, 10]) --> <-1, 10>

Note: This is not to represent a range interval, wrapped can have holes! From the example: [10, 128] contains both <-128, 127> but it does not contain 9 or -127!

◆ get_max()

BigInt wrapped_interval::get_max ( ) const

inline

◆ get_min()

BigInt wrapped_interval::get_min ( ) const

inline

◆ get_upper_bound()

const BigInt & wrapped_interval::get_upper_bound ( ) const

inline

◆ greater_than()

wrapped_interval wrapped_interval::greater_than	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ greater_than_equal()

wrapped_interval wrapped_interval::greater_than_equal	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ intersection()

std::vector< wrapped_interval > wrapped_interval::intersection	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ invert_bool()

wrapped_interval wrapped_interval::invert_bool ( const wrapped_interval & i )

inlinestatic

◆ is_equal()

bool wrapped_interval::is_equal ( const wrapped_interval & rhs ) const

inline

◆ is_included()

bool wrapped_interval::is_included ( const wrapped_interval & rhs ) const

inline

◆ is_representable()

bool wrapped_interval::is_representable ( const type2tc & t )

inlinestatic

◆ is_top()

bool wrapped_interval::is_top ( ) const

inlineoverridevirtual

Reimplemented from interval_templatet< BigInt >.

◆ left_shift() [1/2]

wrapped_interval wrapped_interval::left_shift	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ left_shift() [2/2]

wrapped_interval wrapped_interval::left_shift ( unsigned k ) const

inline

◆ less_than()

wrapped_interval wrapped_interval::less_than	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ less_than_equal()

wrapped_interval wrapped_interval::less_than_equal	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ logical_right_shift() [1/2]

wrapped_interval wrapped_interval::logical_right_shift	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ logical_right_shift() [2/2]

wrapped_interval wrapped_interval::logical_right_shift ( unsigned k ) const

inline

◆ make_ge_than() [1/2]

void wrapped_interval::make_ge_than ( const BigInt & v )

inlineoverridevirtual

Reimplemented from interval_templatet< BigInt >.

◆ make_ge_than() [2/2]

void wrapped_interval::make_ge_than ( const wrapped_interval & rhs )

inline

◆ make_le_than() [1/2]

void wrapped_interval::make_le_than ( const BigInt & v )

inlineoverridevirtual

Reimplemented from interval_templatet< BigInt >.

◆ make_le_than() [2/2]

void wrapped_interval::make_le_than ( const wrapped_interval & rhs )

inline

◆ most_significant_bit()

bool wrapped_interval::most_significant_bit ( const BigInt & b ) const

inline

◆ multiply_us()

std::vector< wrapped_interval > wrapped_interval::multiply_us	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ north_pole()

wrapped_interval wrapped_interval::north_pole ( const type2tc & t )

inlinestatic

◆ not_equal()

wrapped_interval wrapped_interval::not_equal	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

inlinestatic

◆ nsplit()

std::vector< wrapped_interval > wrapped_interval::nsplit ( ) const

inline

◆ over_join() [1/2]

wrapped_interval wrapped_interval::over_join	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ over_join() [2/2]

wrapped_interval wrapped_interval::over_join ( std::vector< wrapped_interval > & r )

inlinestatic

Over union.

◆ over_meet()

wrapped_interval wrapped_interval::over_meet	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

Over meet.

◆ set()

void wrapped_interval::set	(	bool	is_upper,
		const BigInt &	b )

inlineoverridevirtual

Reimplemented from interval_templatet< BigInt >.

◆ sign_extension()

wrapped_interval wrapped_interval::sign_extension ( const type2tc & cast ) const

inline

◆ south_pole()

wrapped_interval wrapped_interval::south_pole ( const type2tc & t )

inlinestatic

◆ ssplit()

std::vector< wrapped_interval > wrapped_interval::ssplit ( ) const

inline

◆ ternary_if()

wrapped_interval wrapped_interval::ternary_if	(	const wrapped_interval &	cond,
		const wrapped_interval &	true_value,
		const wrapped_interval &	false_value )

inlinestatic

◆ trunc() [1/2]

BigInt wrapped_interval::trunc	(	const BigInt &	b,
		unsigned	k )

inlinestatic

◆ trunc() [2/2]

wrapped_interval wrapped_interval::trunc ( const type2tc & cast ) const

inline

◆ under_meet()

wrapped_interval wrapped_interval::under_meet	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

inlinestatic

◆ wrapped_le()

bool wrapped_interval::wrapped_le	(	const BigInt &	b,
		const BigInt &	a,
		const BigInt &	c,
		const type2tc &	t )

inlinestatic

b <=_a c iff b -_w a <= c -_w a

◆ zero_extension()

wrapped_interval wrapped_interval::zero_extension ( const type2tc & cast ) const

inline

◆ operator%

wrapped_interval operator%	(	const wrapped_interval &	s,
		const wrapped_interval &	t )

friend

◆ operator&

wrapped_interval operator&	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

◆ operator*

wrapped_interval operator*	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

◆ operator+

wrapped_interval operator+	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

◆ operator- [1/2]

wrapped_interval operator- ( const wrapped_interval & lhs )

friend

◆ operator- [2/2]

wrapped_interval operator-	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

◆ operator/

wrapped_interval operator/	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

◆ operator^

wrapped_interval operator^	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

◆ operator|

wrapped_interval operator\|	(	const wrapped_interval &	lhs,
		const wrapped_interval &	rhs )

friend

Member Data Documentation

◆ bottom

bool wrapped_interval::bottom = false

◆ t

type2tc wrapped_interval::t

◆ upper_bound

BigInt wrapped_interval::upper_bound

protected

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

src/goto-programs/abstract-interpretation/wrapped_interval.h

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Attributes

Friends

Member Typedef Documentation

◆ warren_approximation_function

Constructor & Destructor Documentation

◆ wrapped_interval() [1/2]

◆ wrapped_interval() [2/2]

Member Function Documentation

◆ amb()

◆ approx_union_with()

◆ arithmetic_right_shift() [1/2]

◆ arithmetic_right_shift() [2/2]

◆ bigger()

◆ bitnot()

◆ cardinality()

◆ cast()

◆ complement()

◆ contains()

◆ convert_to_wrap()

◆ cut()

◆ difference()

◆ empty()

◆ equality()

◆ extend()

◆ extrapolate_to()

◆ gap()

◆ get()

◆ get_interval_bounds()

◆ get_max()

◆ get_min()

◆ get_upper_bound()

◆ greater_than()

◆ greater_than_equal()

◆ intersection()

◆ invert_bool()

◆ is_equal()

◆ is_included()

◆ is_representable()

◆ is_top()

◆ left_shift() [1/2]

◆ left_shift() [2/2]

◆ less_than()

◆ less_than_equal()

◆ logical_right_shift() [1/2]

◆ logical_right_shift() [2/2]

◆ make_ge_than() [1/2]

◆ make_ge_than() [2/2]

◆ make_le_than() [1/2]

◆ make_le_than() [2/2]

◆ most_significant_bit()

◆ multiply_us()

◆ north_pole()

◆ not_equal()

◆ nsplit()

◆ over_join() [1/2]

◆ over_join() [2/2]

◆ over_meet()

◆ set()

◆ sign_extension()

◆ south_pole()

◆ ssplit()

◆ ternary_if()

◆ trunc() [1/2]

◆ trunc() [2/2]

◆ under_meet()

◆ wrapped_le()

◆ zero_extension()

Friends And Related Symbol Documentation

◆ operator%

◆ operator&

◆ operator*

◆ operator+

◆ operator- [1/2]

◆ operator- [2/2]

◆ operator/

◆ operator^