Represents an interval of values. More...

#include <interval.h>

Inheritance diagram for constant_interval_exprt:

Collaboration diagram for constant_interval_exprt:

Public Member Functions
	constant_interval_exprt (const exprt &lower, const exprt &upper, const typet type)

	constant_interval_exprt (const constant_interval_exprt &x)

	constant_interval_exprt (const exprt &x)

	constant_interval_exprt (const typet &type)

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

bool	is_well_formed () const

bool	is_valid_bound (const exprt &expr) const

const exprt &	get_lower () const

const exprt &	get_upper () const

constant_interval_exprt	handle_constant_unary_expression (const irep_idt &op) const
	SET OF ARITHMETIC OPERATORS. More...

constant_interval_exprt	handle_constant_binary_expression (const constant_interval_exprt &other, const irep_idt &) const

constant_interval_exprt	eval (const irep_idt &unary_operator) const

constant_interval_exprt	eval (const irep_idt &binary_operator, const constant_interval_exprt &o) const

constant_interval_exprt	unary_plus () const

constant_interval_exprt	unary_minus () const

constant_interval_exprt	typecast (const typet &type) const

tvt	is_definitely_true () const

tvt	is_definitely_false () const

tvt	logical_and (const constant_interval_exprt &o) const

tvt	logical_or (const constant_interval_exprt &o) const

tvt	logical_xor (const constant_interval_exprt &o) const

tvt	logical_not () const

constant_interval_exprt	plus (const constant_interval_exprt &o) const

constant_interval_exprt	minus (const constant_interval_exprt &other) const

constant_interval_exprt	multiply (const constant_interval_exprt &o) const

constant_interval_exprt	divide (const constant_interval_exprt &o) const

constant_interval_exprt	modulo (const constant_interval_exprt &o) const

constant_interval_exprt	left_shift (const constant_interval_exprt &o) const

constant_interval_exprt	right_shift (const constant_interval_exprt &o) const

constant_interval_exprt	bitwise_not () const

constant_interval_exprt	bitwise_xor (const constant_interval_exprt &o) const

constant_interval_exprt	bitwise_or (const constant_interval_exprt &o) const

constant_interval_exprt	bitwise_and (const constant_interval_exprt &o) const

tvt	less_than (const constant_interval_exprt &o) const

tvt	greater_than (const constant_interval_exprt &o) const

tvt	less_than_or_equal (const constant_interval_exprt &o) const

tvt	greater_than_or_equal (const constant_interval_exprt &o) const

tvt	equal (const constant_interval_exprt &o) const

tvt	not_equal (const constant_interval_exprt &o) const

constant_interval_exprt	increment () const

constant_interval_exprt	decrement () const

bool	is_empty () const

bool	is_single_value_interval () const

std::string	to_string () const

bool	is_top () const

bool	is_bottom () const

constant_interval_exprt	top () const

constant_interval_exprt	bottom () const

bool	has_no_lower_bound () const

bool	has_no_upper_bound () const

min_exprt	min () const

max_exprt	max () const

constant_exprt	zero () const

bool	is_numeric () const

bool	is_int () const

bool	is_float () const

bool	is_bitvector () const

bool	is_signed () const

bool	is_unsigned () const

bool	contains_zero () const

bool	contains (const constant_interval_exprt &interval) const

bool	is_positive () const

bool	is_zero () const

bool	is_negative () const

Public Member Functions inherited from binary_exprt
	binary_exprt (const exprt &_lhs, const irep_idt &_id, exprt _rhs)

	binary_exprt (exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)

exprt &	lhs ()

const exprt &	lhs () const

exprt &	rhs ()

const exprt &	rhs () const

const exprt &	op2 () const =delete

exprt &	op2 ()=delete

const exprt &	op3 () const =delete

exprt &	op3 ()=delete

exprt &	op0 ()

const exprt &	op0 () const

exprt &	op1 ()

const exprt &	op1 () const

Public Member Functions inherited from exprt
	exprt ()

	exprt (const irep_idt &_id)

	exprt (irep_idt _id, typet _type)

	exprt (irep_idt _id, typet _type, operandst &&_operands)

	exprt (const irep_idt &id, typet type, source_locationt loc)

typet &	type ()
	Return the type of the expression. More...

const typet &	type () const

bool	has_operands () const
	Return true if there is at least one operand. More...

operandst &	operands ()

const operandst &	operands () const

template<typename T >
T &	with_source_location (const exprt &other) &
	Add the source location from `other`, if it has any. More...

template<typename T >
T &&	with_source_location (const exprt &other) &&
	Add the source location from `other`, if it has any. More...

void	reserve_operands (operandst::size_type n)

void	copy_to_operands (const exprt &expr)
	Copy the given argument to the end of `exprt`'s operands. More...

void	add_to_operands (const exprt &expr)
	Add the given argument to the end of `exprt`'s operands. More...

void	add_to_operands (exprt &&expr)
	Add the given argument to the end of `exprt`'s operands. More...

void	add_to_operands (exprt &&e1, exprt &&e2)
	Add the given arguments to the end of `exprt`'s operands. More...

void	add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3)
	Add the given arguments to the end of `exprt`'s operands. More...

bool	is_constant () const
	Return whether the expression is a constant. More...

bool	is_true () const
	Return whether the expression is a constant representing `true`. More...

bool	is_false () const
	Return whether the expression is a constant representing `false`. More...

bool	is_zero () const
	Return whether the expression is a constant representing 0. More...

bool	is_one () const
	Return whether the expression is a constant representing 1. More...

bool	is_boolean () const
	Return whether the expression represents a Boolean. More...

const source_locationt &	find_source_location () const
	Get a source_locationt from the expression or from its operands (non-recursively). More...

const source_locationt &	source_location () const

source_locationt &	add_source_location ()

void	drop_source_location ()

void	visit (class expr_visitort &visitor)
	These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children have been visited. More...

void	visit (class const_expr_visitort &visitor) const

void	visit_pre (std::function< void(exprt &)>)

void	visit_pre (std::function< void(const exprt &)>) const

void	visit_post (std::function< void(exprt &)>)
	These are post-order traversal visitors, i.e., the visitor is executed on a node after its children have been visited. More...

void	visit_post (std::function< void(const exprt &)>) const

depth_iteratort	depth_begin ()

depth_iteratort	depth_end ()

const_depth_iteratort	depth_begin () const

const_depth_iteratort	depth_end () const

const_depth_iteratort	depth_cbegin () const

const_depth_iteratort	depth_cend () const

depth_iteratort	depth_begin (std::function< exprt &()> mutate_root) const

const_unique_depth_iteratort	unique_depth_begin () const

const_unique_depth_iteratort	unique_depth_end () const

const_unique_depth_iteratort	unique_depth_cbegin () const

const_unique_depth_iteratort	unique_depth_cend () const

Public Member Functions inherited from irept
bool	is_nil () const

bool	is_not_nil () const

	irept (const irep_idt &_id)

	irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)

	irept ()=default

const irep_idt &	id () const

const std::string &	id_string () const

void	id (const irep_idt &_data)

const irept &	find (const irep_idt &name) const

irept &	add (const irep_idt &name)

irept &	add (const irep_idt &name, irept irep)

const std::string &	get_string (const irep_idt &name) const

const irep_idt &	get (const irep_idt &name) const

bool	get_bool (const irep_idt &name) const

signed int	get_int (const irep_idt &name) const

std::size_t	get_size_t (const irep_idt &name) const

long long	get_long_long (const irep_idt &name) const

void	set (const irep_idt &name, const irep_idt &value)

void	set (const irep_idt &name, irept irep)

void	set (const irep_idt &name, const long long value)

void	set_size_t (const irep_idt &name, const std::size_t value)

void	remove (const irep_idt &name)

void	move_to_sub (irept &irep)

void	move_to_named_sub (const irep_idt &name, irept &irep)

bool	operator== (const irept &other) const

bool	operator!= (const irept &other) const

void	swap (irept &irep)

bool	operator< (const irept &other) const
	defines ordering on the internal representation More...

bool	ordering (const irept &other) const
	defines ordering on the internal representation More...

int	compare (const irept &i) const
	defines ordering on the internal representation comments are ignored More...

void	clear ()

void	make_nil ()

subt &	get_sub ()

const subt &	get_sub () const

named_subt &	get_named_sub ()

const named_subt &	get_named_sub () const

std::size_t	hash () const

std::size_t	full_hash () const

bool	full_eq (const irept &other) const

std::string	pretty (unsigned indent=0, unsigned max_indent=0) const

Public Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
	sharing_treet (irep_idt _id)

	sharing_treet (irep_idt _id, named_subt _named_sub, subt _sub)

	sharing_treet ()

	sharing_treet (const sharing_treet &irep)

	sharing_treet (sharing_treet &&irep)

sharing_treet &	operator= (const sharing_treet &irep)

sharing_treet &	operator= (sharing_treet &&irep)

	~sharing_treet ()

const dt &	read () const

dt &	write ()

Static Public Member Functions
static constant_interval_exprt	tvt_to_interval (const tvt &val)

static bool	equal (const exprt &a, const exprt &b)
	END SET OF ARITHMETIC OPERATORS. More...

static bool	not_equal (const exprt &a, const exprt &b)

static bool	less_than (const exprt &a, const exprt &b)

static bool	less_than_or_equal (const exprt &a, const exprt &b)

static bool	greater_than (const exprt &a, const exprt &b)

static bool	greater_than_or_equal (const exprt &a, const exprt &b)

static tvt	is_true (const constant_interval_exprt &a)

static tvt	is_false (const constant_interval_exprt &a)

static tvt	logical_and (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	logical_or (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	logical_xor (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	logical_not (const constant_interval_exprt &a)

static constant_interval_exprt	unary_plus (const constant_interval_exprt &a)

static constant_interval_exprt	unary_minus (const constant_interval_exprt &a)

static constant_interval_exprt	plus (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	minus (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	multiply (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	divide (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	modulo (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	left_shift (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	right_shift (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	bitwise_not (const constant_interval_exprt &a)

static constant_interval_exprt	bitwise_xor (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	bitwise_or (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	bitwise_and (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	less_than (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	greater_than (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	less_than_or_equal (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	greater_than_or_equal (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	equal (const constant_interval_exprt &a, const constant_interval_exprt &b)

static tvt	not_equal (const constant_interval_exprt &a, const constant_interval_exprt &b)

static constant_interval_exprt	increment (const constant_interval_exprt &a)

static constant_interval_exprt	decrement (const constant_interval_exprt &a)

static bool	is_empty (const constant_interval_exprt &a)

static bool	is_single_value_interval (const constant_interval_exprt &a)

static bool	is_top (const constant_interval_exprt &a)

static bool	is_bottom (const constant_interval_exprt &a)

static bool	is_min (const constant_interval_exprt &a)

static bool	is_max (const constant_interval_exprt &a)

static constant_interval_exprt	top (const typet &type)

static constant_interval_exprt	bottom (const typet &type)

static bool	is_min (const exprt &expr)

static bool	is_max (const exprt &expr)

static constant_exprt	zero (const typet &type)

static constant_exprt	zero (const exprt &expr)

static constant_exprt	zero (const constant_interval_exprt &interval)

static constant_interval_exprt	get_extremes (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)

static exprt	get_extreme (std::vector< exprt > values, bool min=true)

static exprt	get_max (const exprt &a, const exprt &b)

static exprt	get_min (const exprt &a, const exprt &b)

static exprt	get_min (std::vector< exprt > &values)

static exprt	get_max (std::vector< exprt > &values)

static constant_interval_exprt	simplified_interval (exprt &l, exprt &r)

static exprt	simplified_expr (exprt expr)

static bool	is_numeric (const typet &type)

static bool	is_numeric (const exprt &expr)

static bool	is_numeric (const constant_interval_exprt &interval)

static bool	is_int (const typet &type)

static bool	is_int (const exprt &expr)

static bool	is_int (const constant_interval_exprt &interval)

static bool	is_float (const typet &type)

static bool	is_float (const exprt &expr)

static bool	is_float (const constant_interval_exprt &interval)

static bool	is_bitvector (const typet &type)

static bool	is_bitvector (const constant_interval_exprt &interval)

static bool	is_bitvector (const exprt &expr)

static bool	is_signed (const typet &type)

static bool	is_signed (const exprt &expr)

static bool	is_signed (const constant_interval_exprt &interval)

static bool	is_unsigned (const typet &type)

static bool	is_unsigned (const exprt &expr)

static bool	is_unsigned (const constant_interval_exprt &interval)

static bool	is_extreme (const exprt &expr)

static bool	is_extreme (const exprt &expr1, const exprt &expr2)

static bool	contains_extreme (const exprt expr)

static bool	contains_extreme (const exprt expr1, const exprt expr2)

static bool	is_positive (const exprt &expr)

static bool	is_positive (const constant_interval_exprt &interval)

static bool	is_zero (const exprt &expr)

static bool	is_zero (const constant_interval_exprt &interval)

static bool	is_negative (const exprt &expr)

static bool	is_negative (const constant_interval_exprt &interval)

static exprt	abs (const exprt &expr)

Static Public Member Functions inherited from binary_exprt
static void	check (const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

static void	validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

Static Public Member Functions inherited from exprt
static void	check (const exprt &, const validation_modet)
	Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked). More...

static void	validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
	Check that the expression is well-formed, assuming that its subexpressions and type have all ready been checked for well-formedness. More...

static void	validate_full (const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
	Check that the expression is well-formed (full check, including checks of all subexpressions and the type) More...

Static Public Member Functions inherited from irept
static bool	is_comment (const irep_idt &name)

static std::size_t	number_of_non_comments (const named_subt &)
	count the number of named_sub elements that are not comments More...

Static Private Member Functions
static void	generate_expression (const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)

static void	append_multiply_expression (const exprt &lower, const exprt &upper, std::vector< exprt > &collection)
	Adds all possible values that may arise from multiplication (more than one, in case of past the type boundary results). More...

static void	append_multiply_expression_max (const exprt &expr, std::vector< exprt > &collection)
	Appends interval bounds that could arise from MAX * expr. More...

static void	append_multiply_expression_min (const exprt &min, const exprt &other, std::vector< exprt > &collection)
	Appends interval bounds that could arise from MIN * other. More...

static exprt	generate_division_expression (const exprt &lhs, const exprt &rhs)

static exprt	generate_modulo_expression (const exprt &lhs, const exprt &rhs)

static exprt	generate_shift_expression (const exprt &lhs, const exprt &rhs, const irep_idt &operation)

Friends
bool	operator< (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

bool	operator> (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

bool	operator<= (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

bool	operator>= (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

bool	operator== (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

bool	operator!= (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator+ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator- (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator/ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator* (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator% (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator! (const constant_interval_exprt &lhs)

const friend constant_interval_exprt	operator& (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator\| (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator^ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator<< (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

const friend constant_interval_exprt	operator>> (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

std::ostream &	operator<< (std::ostream &out, const constant_interval_exprt &i)

Additional Inherited Members
Public Types inherited from exprt
typedef std::vector< exprt >	operandst

Public Types inherited from irept
using	baset = tree_implementationt

Public Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
using	dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true >

using	subt = typename dt::subt

using	named_subt = typename dt::named_subt

using	tree_implementationt = sharing_treet
	Used to refer to this class from derived classes. More...

Protected Member Functions inherited from expr_protectedt
	expr_protectedt (irep_idt _id, typet _type)

	expr_protectedt (irep_idt _id, typet _type, operandst _operands)

exprt &	op0 ()

const exprt &	op0 () const

exprt &	op1 ()

const exprt &	op1 () const

exprt &	op2 ()

const exprt &	op2 () const

exprt &	op3 ()

const exprt &	op3 () const

Protected Member Functions inherited from exprt
exprt &	op0 ()

exprt &	op1 ()

exprt &	op2 ()

exprt &	op3 ()

const exprt &	op0 () const

const exprt &	op1 () const

const exprt &	op2 () const

const exprt &	op3 () const

exprt &	add_expr (const irep_idt &name)

const exprt &	find_expr (const irep_idt &name) const

Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
void	detach ()

Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
static void	remove_ref (dt *old_data)

static void	nonrecursive_destructor (dt *old_data)
	Does the same as remove_ref, but using an explicit stack instead of recursion. More...

Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
dt *	data

Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
static dt	empty_d

Detailed Description

Represents an interval of values.

Bounds should be constant expressions or min_exprt for the lower bound or max_exprt for the upper bound Also, lower bound should always be <= upper bound

Definition at line 47 of file interval.h.

Constructor & Destructor Documentation

◆ constant_interval_exprt() [1/5]

constant_interval_exprt::constant_interval_exprt	(	const exprt &	lower,
		const exprt &	upper,
		const typet	type
	)

inline

Definition at line 50 of file interval.h.

◆ constant_interval_exprt() [2/5]

constant_interval_exprt::constant_interval_exprt ( const constant_interval_exprt & x )

inline

Definition at line 59 of file interval.h.

◆ constant_interval_exprt() [3/5]

constant_interval_exprt::constant_interval_exprt ( const exprt & x )

inlineexplicit

Definition at line 64 of file interval.h.

◆ constant_interval_exprt() [4/5]

constant_interval_exprt::constant_interval_exprt ( const typet & type )

inlineexplicit

Definition at line 69 of file interval.h.

◆ constant_interval_exprt() [5/5]

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

inline

Definition at line 74 of file interval.h.

Member Function Documentation

◆ abs()

exprt constant_interval_exprt::abs ( const exprt & expr )

static

Definition at line 1299 of file interval.cpp.

◆ append_multiply_expression()

void constant_interval_exprt::append_multiply_expression	(	const exprt &	lower,
		const exprt &	upper,
		std::vector< exprt > &	collection
	)

staticprivate

Adds all possible values that may arise from multiplication (more than one, in case of past the type boundary results).

Parameters

lower	lhs of multiplication
upper	rhs of multiplication
collection	vector of possible values

Definition at line 600 of file interval.cpp.

◆ append_multiply_expression_max()

void constant_interval_exprt::append_multiply_expression_max	(	const exprt &	expr,
		std::vector< exprt > &	collection
	)

staticprivate

Appends interval bounds that could arise from MAX * expr.

Accommodates for overflows by over-approximating.

Parameters

expr	the unknown side of multiplication
collection	vector of collected bounds

Definition at line 638 of file interval.cpp.

◆ append_multiply_expression_min()

void constant_interval_exprt::append_multiply_expression_min	(	const exprt &	min,
		const exprt &	other,
		std::vector< exprt > &	collection
	)

staticprivate

Appends interval bounds that could arise from MIN * other.

Accommodates for overflows by over-approximating.

Parameters

min	the side known to be MIN for a given type
other	the side of unknown value
collection	reference to the vector of collected boundaries

Definition at line 663 of file interval.cpp.

◆ bitwise_and() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_and	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1737 of file interval.cpp.

◆ bitwise_and() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_and ( const constant_interval_exprt & o ) const

Definition at line 357 of file interval.cpp.

◆ bitwise_not() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_not ( ) const

Definition at line 367 of file interval.cpp.

◆ bitwise_not() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_not ( const constant_interval_exprt & a )

static

Definition at line 1717 of file interval.cpp.

◆ bitwise_or() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_or	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1730 of file interval.cpp.

◆ bitwise_or() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_or ( const constant_interval_exprt & o ) const

Definition at line 346 of file interval.cpp.

◆ bitwise_xor() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_xor	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1723 of file interval.cpp.

◆ bitwise_xor() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_xor ( const constant_interval_exprt & o ) const

Definition at line 335 of file interval.cpp.

◆ bottom() [1/2]

constant_interval_exprt constant_interval_exprt::bottom ( ) const

Definition at line 1057 of file interval.cpp.

◆ bottom() [2/2]

constant_interval_exprt constant_interval_exprt::bottom ( const typet & type )

static

Definition at line 1047 of file interval.cpp.

◆ contains()

bool constant_interval_exprt::contains ( const constant_interval_exprt & interval ) const

Definition at line 1426 of file interval.cpp.

◆ contains_extreme() [1/2]

bool constant_interval_exprt::contains_extreme ( const exprt expr )

static

Definition at line 1829 of file interval.cpp.

◆ contains_extreme() [2/2]

bool constant_interval_exprt::contains_extreme	(	const exprt	expr1,
		const exprt	expr2
	)

static

Definition at line 1847 of file interval.cpp.

◆ contains_zero()

bool constant_interval_exprt::contains_zero ( ) const

Definition at line 1870 of file interval.cpp.

◆ decrement() [1/2]

constant_interval_exprt constant_interval_exprt::decrement ( ) const

Definition at line 465 of file interval.cpp.

◆ decrement() [2/2]

constant_interval_exprt constant_interval_exprt::decrement ( const constant_interval_exprt & a )

static

Definition at line 1793 of file interval.cpp.

◆ divide() [1/2]

constant_interval_exprt constant_interval_exprt::divide	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1686 of file interval.cpp.

◆ divide() [2/2]

constant_interval_exprt constant_interval_exprt::divide ( const constant_interval_exprt & o ) const

Definition at line 137 of file interval.cpp.

◆ equal() [1/3]

tvt constant_interval_exprt::equal	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1772 of file interval.cpp.

◆ equal() [2/3]

tvt constant_interval_exprt::equal ( const constant_interval_exprt & o ) const

Definition at line 432 of file interval.cpp.

◆ equal() [3/3]

bool constant_interval_exprt::equal	(	const exprt &	a,
		const exprt &	b
	)

static

END SET OF ARITHMETIC OPERATORS.

Definition at line 1314 of file interval.cpp.

◆ eval() [1/2]

constant_interval_exprt constant_interval_exprt::eval	(	const irep_idt &	binary_operator,
		const constant_interval_exprt &	o
	)		const

Definition at line 814 of file interval.cpp.

◆ eval() [2/2]

constant_interval_exprt constant_interval_exprt::eval ( const irep_idt & unary_operator ) const

Definition at line 792 of file interval.cpp.

◆ generate_division_expression()

exprt constant_interval_exprt::generate_division_expression	(	const exprt &	lhs,
		const exprt &	rhs
	)

staticprivate

Definition at line 683 of file interval.cpp.

◆ generate_expression()

void constant_interval_exprt::generate_expression	(	const exprt &	lhs,
		const exprt &	rhs,
		const irep_idt &	operation,
		std::vector< exprt > &	collection
	)

staticprivate

Definition at line 571 of file interval.cpp.

◆ generate_modulo_expression()

exprt constant_interval_exprt::generate_modulo_expression	(	const exprt &	lhs,
		const exprt &	rhs
	)

staticprivate

Definition at line 738 of file interval.cpp.

◆ generate_shift_expression()

exprt constant_interval_exprt::generate_shift_expression	(	const exprt &	lhs,
		const exprt &	rhs,
		const irep_idt &	operation
	)

staticprivate

Definition at line 898 of file interval.cpp.

◆ get_extreme()

exprt constant_interval_exprt::get_extreme	(	std::vector< exprt >	values,
		bool	min = `true`
	)

static

Definition at line 496 of file interval.cpp.

◆ get_extremes()

constant_interval_exprt constant_interval_exprt::get_extremes	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs,
		const irep_idt &	operation
	)

static

Definition at line 470 of file interval.cpp.

◆ get_lower()

const exprt & constant_interval_exprt::get_lower ( ) const

Definition at line 29 of file interval.cpp.

◆ get_max() [1/2]

exprt constant_interval_exprt::get_max	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 959 of file interval.cpp.

◆ get_max() [2/2]

exprt constant_interval_exprt::get_max ( std::vector< exprt > & values )

static

Definition at line 974 of file interval.cpp.

◆ get_min() [1/2]

exprt constant_interval_exprt::get_min	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 964 of file interval.cpp.

◆ get_min() [2/2]

exprt constant_interval_exprt::get_min ( std::vector< exprt > & values )

static

Definition at line 969 of file interval.cpp.

◆ get_upper()

const exprt & constant_interval_exprt::get_upper ( ) const

Definition at line 34 of file interval.cpp.

◆ greater_than() [1/3]

tvt constant_interval_exprt::greater_than	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1751 of file interval.cpp.

◆ greater_than() [2/3]

tvt constant_interval_exprt::greater_than ( const constant_interval_exprt & o ) const

Definition at line 398 of file interval.cpp.

◆ greater_than() [3/3]

bool constant_interval_exprt::greater_than	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 1404 of file interval.cpp.

◆ greater_than_or_equal() [1/3]

tvt constant_interval_exprt::greater_than_or_equal	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1765 of file interval.cpp.

◆ greater_than_or_equal() [2/3]

tvt constant_interval_exprt::greater_than_or_equal ( const constant_interval_exprt & o ) const

Definition at line 426 of file interval.cpp.

◆ greater_than_or_equal() [3/3]

bool constant_interval_exprt::greater_than_or_equal	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 1414 of file interval.cpp.

◆ handle_constant_binary_expression()

constant_interval_exprt constant_interval_exprt::handle_constant_binary_expression	(	const constant_interval_exprt &	other,
		const irep_idt &	op
	)		const

Definition at line 950 of file interval.cpp.

◆ handle_constant_unary_expression()

constant_interval_exprt constant_interval_exprt::handle_constant_unary_expression ( const irep_idt & op ) const

SET OF ARITHMETIC OPERATORS.

Definition at line 938 of file interval.cpp.

◆ has_no_lower_bound()

bool constant_interval_exprt::has_no_lower_bound ( ) const

Definition at line 1210 of file interval.cpp.

◆ has_no_upper_bound()

bool constant_interval_exprt::has_no_upper_bound ( ) const

Definition at line 1205 of file interval.cpp.

◆ increment() [1/2]

constant_interval_exprt constant_interval_exprt::increment ( ) const

Definition at line 460 of file interval.cpp.

◆ increment() [2/2]

constant_interval_exprt constant_interval_exprt::increment ( const constant_interval_exprt & a )

static

Definition at line 1787 of file interval.cpp.

◆ is_bitvector() [1/4]

bool constant_interval_exprt::is_bitvector ( ) const

Definition at line 1190 of file interval.cpp.

◆ is_bitvector() [2/4]

bool constant_interval_exprt::is_bitvector ( const constant_interval_exprt & interval )

static

Definition at line 1159 of file interval.cpp.

◆ is_bitvector() [3/4]

bool constant_interval_exprt::is_bitvector ( const exprt & expr )

static

Definition at line 1175 of file interval.cpp.

◆ is_bitvector() [4/4]

bool constant_interval_exprt::is_bitvector ( const typet & type )

static

Definition at line 1125 of file interval.cpp.

◆ is_bottom() [1/2]

bool constant_interval_exprt::is_bottom ( ) const

Definition at line 1036 of file interval.cpp.

◆ is_bottom() [2/2]

bool constant_interval_exprt::is_bottom ( const constant_interval_exprt & a )

static

Definition at line 1814 of file interval.cpp.

◆ is_definitely_false()

tvt constant_interval_exprt::is_definitely_false ( ) const

Definition at line 224 of file interval.cpp.

◆ is_definitely_true()

tvt constant_interval_exprt::is_definitely_true ( ) const

Definition at line 218 of file interval.cpp.

◆ is_empty() [1/2]

bool constant_interval_exprt::is_empty ( ) const

Definition at line 1854 of file interval.cpp.

◆ is_empty() [2/2]

bool constant_interval_exprt::is_empty ( const constant_interval_exprt & a )

static

Definition at line 1798 of file interval.cpp.

◆ is_extreme() [1/2]

bool constant_interval_exprt::is_extreme ( const exprt & expr )

static

Definition at line 1195 of file interval.cpp.

◆ is_extreme() [2/2]

bool constant_interval_exprt::is_extreme	(	const exprt &	expr1,
		const exprt &	expr2
	)

static

Definition at line 1200 of file interval.cpp.

◆ is_false()

tvt constant_interval_exprt::is_false ( const constant_interval_exprt & a )

static

Definition at line 1934 of file interval.cpp.

◆ is_float() [1/4]

bool constant_interval_exprt::is_float ( ) const

Definition at line 1069 of file interval.cpp.

◆ is_float() [2/4]

bool constant_interval_exprt::is_float ( const constant_interval_exprt & interval )

static

Definition at line 1120 of file interval.cpp.

◆ is_float() [3/4]

bool constant_interval_exprt::is_float ( const exprt & expr )

static

Definition at line 1115 of file interval.cpp.

◆ is_float() [4/4]

bool constant_interval_exprt::is_float ( const typet & type )

static

Definition at line 1100 of file interval.cpp.

◆ is_int() [1/4]

bool constant_interval_exprt::is_int ( ) const

Definition at line 1064 of file interval.cpp.

◆ is_int() [2/4]

bool constant_interval_exprt::is_int ( const constant_interval_exprt & interval )

static

Definition at line 1110 of file interval.cpp.

◆ is_int() [3/4]

bool constant_interval_exprt::is_int ( const exprt & expr )

static

Definition at line 1105 of file interval.cpp.

◆ is_int() [4/4]

bool constant_interval_exprt::is_int ( const typet & type )

static

Definition at line 1095 of file interval.cpp.

◆ is_max() [1/2]

bool constant_interval_exprt::is_max ( const constant_interval_exprt & a )

static

Definition at line 1824 of file interval.cpp.

◆ is_max() [2/2]

bool constant_interval_exprt::is_max ( const exprt & expr )

static

Definition at line 1215 of file interval.cpp.

◆ is_min() [1/2]

bool constant_interval_exprt::is_min ( const constant_interval_exprt & a )

static

Definition at line 1819 of file interval.cpp.

◆ is_min() [2/2]

bool constant_interval_exprt::is_min ( const exprt & expr )

static

Definition at line 1220 of file interval.cpp.

◆ is_negative() [1/3]

bool constant_interval_exprt::is_negative ( ) const

Definition at line 1924 of file interval.cpp.

◆ is_negative() [2/3]

bool constant_interval_exprt::is_negative ( const constant_interval_exprt & interval )

static

Definition at line 1908 of file interval.cpp.

◆ is_negative() [3/3]

bool constant_interval_exprt::is_negative ( const exprt & expr )

static

Definition at line 1279 of file interval.cpp.

◆ is_numeric() [1/4]

bool constant_interval_exprt::is_numeric ( ) const

Definition at line 1079 of file interval.cpp.

◆ is_numeric() [2/4]

bool constant_interval_exprt::is_numeric ( const constant_interval_exprt & interval )

static

Definition at line 1089 of file interval.cpp.

◆ is_numeric() [3/4]

bool constant_interval_exprt::is_numeric ( const exprt & expr )

static

Definition at line 1084 of file interval.cpp.

◆ is_numeric() [4/4]

bool constant_interval_exprt::is_numeric ( const typet & type )

static

Definition at line 1074 of file interval.cpp.

◆ is_positive() [1/3]

bool constant_interval_exprt::is_positive ( ) const

Definition at line 1914 of file interval.cpp.

◆ is_positive() [2/3]

bool constant_interval_exprt::is_positive ( const constant_interval_exprt & interval )

static

Definition at line 1897 of file interval.cpp.

◆ is_positive() [3/3]

bool constant_interval_exprt::is_positive ( const exprt & expr )

static

Definition at line 1225 of file interval.cpp.

◆ is_signed() [1/4]

bool constant_interval_exprt::is_signed ( ) const

Definition at line 1180 of file interval.cpp.

◆ is_signed() [2/4]

bool constant_interval_exprt::is_signed ( const constant_interval_exprt & interval )

static

Definition at line 1148 of file interval.cpp.

◆ is_signed() [3/4]

bool constant_interval_exprt::is_signed ( const exprt & expr )

static

Definition at line 1165 of file interval.cpp.

◆ is_signed() [4/4]

bool constant_interval_exprt::is_signed ( const typet & type )

static

Definition at line 1133 of file interval.cpp.

◆ is_single_value_interval() [1/2]

bool constant_interval_exprt::is_single_value_interval ( ) const

Definition at line 1864 of file interval.cpp.

◆ is_single_value_interval() [2/2]

bool constant_interval_exprt::is_single_value_interval ( const constant_interval_exprt & a )

static

Definition at line 1803 of file interval.cpp.

◆ is_top() [1/2]

bool constant_interval_exprt::is_top ( ) const

Definition at line 1031 of file interval.cpp.

◆ is_top() [2/2]

bool constant_interval_exprt::is_top ( const constant_interval_exprt & a )

static

Definition at line 1809 of file interval.cpp.

◆ is_true()

tvt constant_interval_exprt::is_true ( const constant_interval_exprt & a )

static

Definition at line 1929 of file interval.cpp.

◆ is_unsigned() [1/4]

bool constant_interval_exprt::is_unsigned ( ) const

Definition at line 1185 of file interval.cpp.

◆ is_unsigned() [2/4]

bool constant_interval_exprt::is_unsigned ( const constant_interval_exprt & interval )

static

Definition at line 1153 of file interval.cpp.

◆ is_unsigned() [3/4]

bool constant_interval_exprt::is_unsigned ( const exprt & expr )

static

Definition at line 1170 of file interval.cpp.

◆ is_unsigned() [4/4]

bool constant_interval_exprt::is_unsigned ( const typet & type )

static

Definition at line 1140 of file interval.cpp.

◆ is_valid_bound()

bool constant_interval_exprt::is_valid_bound ( const exprt & expr ) const

inline

Definition at line 100 of file interval.h.

◆ is_well_formed()

bool constant_interval_exprt::is_well_formed ( ) const

inline

Definition at line 79 of file interval.h.

◆ is_zero() [1/3]

bool constant_interval_exprt::is_zero ( ) const

Definition at line 1919 of file interval.cpp.

◆ is_zero() [2/3]

bool constant_interval_exprt::is_zero ( const constant_interval_exprt & interval )

static

Definition at line 1903 of file interval.cpp.

◆ is_zero() [3/3]

bool constant_interval_exprt::is_zero ( const exprt & expr )

static

Definition at line 1250 of file interval.cpp.

◆ left_shift() [1/2]

constant_interval_exprt constant_interval_exprt::left_shift	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1701 of file interval.cpp.

◆ left_shift() [2/2]

constant_interval_exprt constant_interval_exprt::left_shift ( const constant_interval_exprt & o ) const

Definition at line 302 of file interval.cpp.

◆ less_than() [1/3]

tvt constant_interval_exprt::less_than	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1744 of file interval.cpp.

◆ less_than() [2/3]

tvt constant_interval_exprt::less_than ( const constant_interval_exprt & o ) const

Definition at line 377 of file interval.cpp.

◆ less_than() [3/3]

bool constant_interval_exprt::less_than	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 1357 of file interval.cpp.

◆ less_than_or_equal() [1/3]

tvt constant_interval_exprt::less_than_or_equal	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1758 of file interval.cpp.

◆ less_than_or_equal() [2/3]

tvt constant_interval_exprt::less_than_or_equal ( const constant_interval_exprt & o ) const

Definition at line 404 of file interval.cpp.

◆ less_than_or_equal() [3/3]

bool constant_interval_exprt::less_than_or_equal	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 1409 of file interval.cpp.

◆ logical_and() [1/2]

tvt constant_interval_exprt::logical_and	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1939 of file interval.cpp.

◆ logical_and() [2/2]

tvt constant_interval_exprt::logical_and ( const constant_interval_exprt & o ) const

Definition at line 266 of file interval.cpp.

◆ logical_not() [1/2]

tvt constant_interval_exprt::logical_not ( ) const

Definition at line 284 of file interval.cpp.

◆ logical_not() [2/2]

tvt constant_interval_exprt::logical_not ( const constant_interval_exprt & a )

static

Definition at line 1960 of file interval.cpp.

◆ logical_or() [1/2]

tvt constant_interval_exprt::logical_or	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1946 of file interval.cpp.

◆ logical_or() [2/2]

tvt constant_interval_exprt::logical_or ( const constant_interval_exprt & o ) const

Definition at line 255 of file interval.cpp.

◆ logical_xor() [1/2]

tvt constant_interval_exprt::logical_xor	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1953 of file interval.cpp.

◆ logical_xor() [2/2]

tvt constant_interval_exprt::logical_xor ( const constant_interval_exprt & o ) const

Definition at line 274 of file interval.cpp.

◆ max()

max_exprt constant_interval_exprt::max ( ) const

Definition at line 1026 of file interval.cpp.

◆ min()

min_exprt constant_interval_exprt::min ( ) const

Definition at line 1021 of file interval.cpp.

◆ minus() [1/2]

constant_interval_exprt constant_interval_exprt::minus	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1672 of file interval.cpp.

◆ minus() [2/2]

constant_interval_exprt constant_interval_exprt::minus ( const constant_interval_exprt & other ) const

Definition at line 114 of file interval.cpp.

◆ modulo() [1/2]

constant_interval_exprt constant_interval_exprt::modulo	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1693 of file interval.cpp.

◆ modulo() [2/2]

constant_interval_exprt constant_interval_exprt::modulo ( const constant_interval_exprt & o ) const

Definition at line 154 of file interval.cpp.

◆ multiply() [1/2]

constant_interval_exprt constant_interval_exprt::multiply	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1679 of file interval.cpp.

◆ multiply() [2/2]

constant_interval_exprt constant_interval_exprt::multiply ( const constant_interval_exprt & o ) const

Definition at line 126 of file interval.cpp.

◆ not_equal() [1/3]

tvt constant_interval_exprt::not_equal	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1779 of file interval.cpp.

◆ not_equal() [2/3]

tvt constant_interval_exprt::not_equal ( const constant_interval_exprt & o ) const

Definition at line 455 of file interval.cpp.

◆ not_equal() [3/3]

bool constant_interval_exprt::not_equal	(	const exprt &	a,
		const exprt &	b
	)

static

Definition at line 1421 of file interval.cpp.

◆ plus() [1/2]

constant_interval_exprt constant_interval_exprt::plus	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1665 of file interval.cpp.

◆ plus() [2/2]

constant_interval_exprt constant_interval_exprt::plus ( const constant_interval_exprt & o ) const

Definition at line 76 of file interval.cpp.

◆ right_shift() [1/2]

constant_interval_exprt constant_interval_exprt::right_shift	(	const constant_interval_exprt &	a,
		const constant_interval_exprt &	b
	)

static

Definition at line 1708 of file interval.cpp.

◆ right_shift() [2/2]

constant_interval_exprt constant_interval_exprt::right_shift ( const constant_interval_exprt & o ) const

Definition at line 319 of file interval.cpp.

◆ simplified_expr()

exprt constant_interval_exprt::simplified_expr ( exprt expr )

static

Definition at line 986 of file interval.cpp.

◆ simplified_interval()

constant_interval_exprt constant_interval_exprt::simplified_interval	(	exprt &	l,
		exprt &	r
	)

static

Definition at line 981 of file interval.cpp.

◆ to_string()

std::string constant_interval_exprt::to_string ( ) const

Definition at line 1435 of file interval.cpp.

◆ top() [1/2]

constant_interval_exprt constant_interval_exprt::top ( ) const

Definition at line 1052 of file interval.cpp.

◆ top() [2/2]

constant_interval_exprt constant_interval_exprt::top ( const typet & type )

static

Definition at line 1042 of file interval.cpp.

◆ tvt_to_interval()

constant_interval_exprt constant_interval_exprt::tvt_to_interval ( const tvt & val )

static

Definition at line 1965 of file interval.cpp.

◆ typecast()

constant_interval_exprt constant_interval_exprt::typecast ( const typet & type ) const

Definition at line 1626 of file interval.cpp.

◆ unary_minus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_minus ( ) const

Definition at line 44 of file interval.cpp.

◆ unary_minus() [2/2]

constant_interval_exprt constant_interval_exprt::unary_minus ( const constant_interval_exprt & a )

static

Definition at line 1620 of file interval.cpp.

◆ unary_plus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_plus ( ) const

Definition at line 39 of file interval.cpp.

◆ unary_plus() [2/2]

constant_interval_exprt constant_interval_exprt::unary_plus ( const constant_interval_exprt & a )

static

Definition at line 1614 of file interval.cpp.

◆ zero() [1/4]

constant_exprt constant_interval_exprt::zero ( ) const

Definition at line 1016 of file interval.cpp.

◆ zero() [2/4]

constant_exprt constant_interval_exprt::zero ( const constant_interval_exprt & interval )

static

Definition at line 1011 of file interval.cpp.

◆ zero() [3/4]

constant_exprt constant_interval_exprt::zero ( const exprt & expr )

static

Definition at line 1005 of file interval.cpp.

◆ zero() [4/4]

constant_exprt constant_interval_exprt::zero ( const typet & type )

static

Definition at line 996 of file interval.cpp.

Friends And Related Function Documentation

◆ operator!

const friend constant_interval_exprt operator! ( const constant_interval_exprt & lhs )

friend

Definition at line 1594 of file interval.cpp.

◆ operator!=

bool operator!=	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1531 of file interval.cpp.

◆ operator%

const friend constant_interval_exprt operator%	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1566 of file interval.cpp.

◆ operator&

const friend constant_interval_exprt operator&	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1573 of file interval.cpp.

◆ operator*

const friend constant_interval_exprt operator*	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1559 of file interval.cpp.

◆ operator+

const friend constant_interval_exprt operator+	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1538 of file interval.cpp.

◆ operator-

const friend constant_interval_exprt operator-	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1545 of file interval.cpp.

◆ operator/

const friend constant_interval_exprt operator/	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1552 of file interval.cpp.

◆ operator<

bool operator<	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1496 of file interval.cpp.

◆ operator<< [1/2]

const friend constant_interval_exprt operator<<	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1599 of file interval.cpp.

◆ operator<< [2/2]

std::ostream& operator<<	(	std::ostream &	out,
		const constant_interval_exprt &	i
	)

friend

Definition at line 1442 of file interval.cpp.

◆ operator<=

bool operator<=	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1510 of file interval.cpp.

◆ operator==

bool operator==	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1524 of file interval.cpp.

◆ operator>

bool operator>	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1503 of file interval.cpp.

◆ operator>=

bool operator>=	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1517 of file interval.cpp.

◆ operator>>

const friend constant_interval_exprt operator>>	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1606 of file interval.cpp.

◆ operator^

const friend constant_interval_exprt operator^	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1587 of file interval.cpp.

◆ operator|

const friend constant_interval_exprt operator\|	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

friend

Definition at line 1580 of file interval.cpp.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/interval.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/interval.cpp

Public Member Functions

Static Public Member Functions

Static Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ constant_interval_exprt() [1/5]

◆ constant_interval_exprt() [2/5]

◆ constant_interval_exprt() [3/5]

◆ constant_interval_exprt() [4/5]

◆ constant_interval_exprt() [5/5]

Member Function Documentation

◆ abs()

◆ append_multiply_expression()

◆ append_multiply_expression_max()

◆ append_multiply_expression_min()

◆ bitwise_and() [1/2]

◆ bitwise_and() [2/2]

◆ bitwise_not() [1/2]

◆ bitwise_not() [2/2]

◆ bitwise_or() [1/2]

◆ bitwise_or() [2/2]

◆ bitwise_xor() [1/2]

◆ bitwise_xor() [2/2]

◆ bottom() [1/2]

◆ bottom() [2/2]

◆ contains()

◆ contains_extreme() [1/2]

◆ contains_extreme() [2/2]

◆ contains_zero()

◆ decrement() [1/2]

◆ decrement() [2/2]

◆ divide() [1/2]

◆ divide() [2/2]

◆ equal() [1/3]

◆ equal() [2/3]

◆ equal() [3/3]

◆ eval() [1/2]

◆ eval() [2/2]

◆ generate_division_expression()

◆ generate_expression()

◆ generate_modulo_expression()

◆ generate_shift_expression()

◆ get_extreme()

◆ get_extremes()

◆ get_lower()

◆ get_max() [1/2]

◆ get_max() [2/2]

◆ get_min() [1/2]

◆ get_min() [2/2]

◆ get_upper()

◆ greater_than() [1/3]

◆ greater_than() [2/3]

◆ greater_than() [3/3]

◆ greater_than_or_equal() [1/3]

◆ greater_than_or_equal() [2/3]

◆ greater_than_or_equal() [3/3]

◆ handle_constant_binary_expression()

◆ handle_constant_unary_expression()

◆ has_no_lower_bound()

◆ has_no_upper_bound()

◆ increment() [1/2]

◆ increment() [2/2]

◆ is_bitvector() [1/4]

◆ is_bitvector() [2/4]

◆ is_bitvector() [3/4]

◆ is_bitvector() [4/4]

◆ is_bottom() [1/2]

◆ is_bottom() [2/2]

◆ is_definitely_false()

◆ is_definitely_true()

◆ is_empty() [1/2]

◆ is_empty() [2/2]

◆ is_extreme() [1/2]

◆ is_extreme() [2/2]

◆ is_false()

◆ is_float() [1/4]

◆ is_float() [2/4]

◆ is_float() [3/4]