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 (exprt lower, exprt upper, typet type)

	constant_interval_exprt (const typet &type)

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

bool	is_well_formed () 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_value_exprt	min () const

max_value_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

exprt &	with_source_location (source_locationt location) &
	Add the source location from `location`, if it is non-nil. More...

exprt &&	with_source_location (source_locationt location) &&
	Add the source location from `location`, if it is non-nil. More...

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

exprt &&	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	singleton (const exprt &x)

static bool	is_valid_bound (const exprt &expr)

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 constant_interval_exprt	operator+ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

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

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

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

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

const constant_interval_exprt	operator! (const constant_interval_exprt &lhs)

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

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

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

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

const 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_value_exprt for the lower bound or max_value_exprt for the upper bound Also, lower bound should always be <= upper bound

Definition at line 51 of file interval.h.

Constructor & Destructor Documentation

◆ constant_interval_exprt() [1/3]

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

inline

Definition at line 54 of file interval.h.

◆ constant_interval_exprt() [2/3]

constant_interval_exprt::constant_interval_exprt ( const typet & type )

inlineexplicit

Definition at line 64 of file interval.h.

◆ constant_interval_exprt() [3/3]

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

inline

Definition at line 72 of file interval.h.

Member Function Documentation

◆ abs()

exprt constant_interval_exprt::abs ( const exprt & expr )

static

Definition at line 1300 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 601 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 639 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 664 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 1738 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 356 of file interval.cpp.

◆ bitwise_not() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_not ( ) const

Definition at line 366 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 1718 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 1731 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 345 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 1724 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 334 of file interval.cpp.

◆ bottom() [1/2]

constant_interval_exprt constant_interval_exprt::bottom ( ) const

Definition at line 1058 of file interval.cpp.

◆ bottom() [2/2]

constant_interval_exprt constant_interval_exprt::bottom ( const typet & type )

static

Definition at line 1048 of file interval.cpp.

◆ contains()

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

Definition at line 1427 of file interval.cpp.

◆ contains_extreme() [1/2]

bool constant_interval_exprt::contains_extreme ( const exprt expr )

static

Definition at line 1830 of file interval.cpp.

◆ contains_extreme() [2/2]

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

static

Definition at line 1848 of file interval.cpp.

◆ contains_zero()

bool constant_interval_exprt::contains_zero ( ) const

Definition at line 1871 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 1794 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 1687 of file interval.cpp.

◆ divide() [2/2]

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

Definition at line 135 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 1773 of file interval.cpp.

◆ equal() [2/3]

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

Definition at line 431 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 1315 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 815 of file interval.cpp.

◆ eval() [2/2]

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

Definition at line 793 of file interval.cpp.

◆ generate_division_expression()

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

staticprivate

Definition at line 684 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 572 of file interval.cpp.

◆ generate_modulo_expression()

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

staticprivate

Definition at line 739 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 899 of file interval.cpp.

◆ get_extreme()

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

static

Definition at line 497 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 471 of file interval.cpp.

◆ get_lower()

const exprt & constant_interval_exprt::get_lower ( ) const

Definition at line 27 of file interval.cpp.

◆ get_max() [1/2]

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

static

Definition at line 960 of file interval.cpp.

◆ get_max() [2/2]

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

static

Definition at line 975 of file interval.cpp.

◆ get_min() [1/2]

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

static

Definition at line 965 of file interval.cpp.

◆ get_min() [2/2]

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

static

Definition at line 970 of file interval.cpp.

◆ get_upper()

const exprt & constant_interval_exprt::get_upper ( ) const

Definition at line 32 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 1752 of file interval.cpp.

◆ greater_than() [2/3]

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

Definition at line 397 of file interval.cpp.

◆ greater_than() [3/3]

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

static

Definition at line 1405 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 1766 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 425 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 1415 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 951 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 939 of file interval.cpp.

◆ has_no_lower_bound()

bool constant_interval_exprt::has_no_lower_bound ( ) const

Definition at line 1211 of file interval.cpp.

◆ has_no_upper_bound()

bool constant_interval_exprt::has_no_upper_bound ( ) const

Definition at line 1206 of file interval.cpp.

◆ increment() [1/2]

constant_interval_exprt constant_interval_exprt::increment ( ) const

Definition at line 459 of file interval.cpp.

◆ increment() [2/2]

constant_interval_exprt constant_interval_exprt::increment ( const constant_interval_exprt & a )

static

Definition at line 1788 of file interval.cpp.

◆ is_bitvector() [1/4]

bool constant_interval_exprt::is_bitvector ( ) const

Definition at line 1191 of file interval.cpp.

◆ is_bitvector() [2/4]

bool constant_interval_exprt::is_bitvector ( const constant_interval_exprt & interval )

static

Definition at line 1160 of file interval.cpp.

◆ is_bitvector() [3/4]

bool constant_interval_exprt::is_bitvector ( const exprt & expr )

static

Definition at line 1176 of file interval.cpp.

◆ is_bitvector() [4/4]

bool constant_interval_exprt::is_bitvector ( const typet & type )

static

Definition at line 1126 of file interval.cpp.

◆ is_bottom() [1/2]

bool constant_interval_exprt::is_bottom ( ) const

Definition at line 1037 of file interval.cpp.

◆ is_bottom() [2/2]

bool constant_interval_exprt::is_bottom ( const constant_interval_exprt & a )

static

Definition at line 1815 of file interval.cpp.

◆ is_definitely_false()

tvt constant_interval_exprt::is_definitely_false ( ) const

Definition at line 223 of file interval.cpp.

◆ is_definitely_true()

tvt constant_interval_exprt::is_definitely_true ( ) const

Definition at line 217 of file interval.cpp.

◆ is_empty() [1/2]

bool constant_interval_exprt::is_empty ( ) const

Definition at line 1855 of file interval.cpp.

◆ is_empty() [2/2]

bool constant_interval_exprt::is_empty ( const constant_interval_exprt & a )

static

Definition at line 1799 of file interval.cpp.

◆ is_extreme() [1/2]

bool constant_interval_exprt::is_extreme ( const exprt & expr )

static

Definition at line 1196 of file interval.cpp.

◆ is_extreme() [2/2]

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

static

Definition at line 1201 of file interval.cpp.

◆ is_false()

tvt constant_interval_exprt::is_false ( const constant_interval_exprt & a )

static

Definition at line 1935 of file interval.cpp.

◆ is_float() [1/4]

bool constant_interval_exprt::is_float ( ) const

Definition at line 1070 of file interval.cpp.

◆ is_float() [2/4]

bool constant_interval_exprt::is_float ( const constant_interval_exprt & interval )

static

Definition at line 1121 of file interval.cpp.

◆ is_float() [3/4]

bool constant_interval_exprt::is_float ( const exprt & expr )

static

Definition at line 1116 of file interval.cpp.

◆ is_float() [4/4]

bool constant_interval_exprt::is_float ( const typet & type )

static

Definition at line 1101 of file interval.cpp.

◆ is_int() [1/4]

bool constant_interval_exprt::is_int ( ) const

Definition at line 1065 of file interval.cpp.

◆ is_int() [2/4]

bool constant_interval_exprt::is_int ( const constant_interval_exprt & interval )

static

Definition at line 1111 of file interval.cpp.

◆ is_int() [3/4]

bool constant_interval_exprt::is_int ( const exprt & expr )

static

Definition at line 1106 of file interval.cpp.

◆ is_int() [4/4]

bool constant_interval_exprt::is_int ( const typet & type )

static

Definition at line 1096 of file interval.cpp.

◆ is_max() [1/2]

bool constant_interval_exprt::is_max ( const constant_interval_exprt & a )

static

Definition at line 1825 of file interval.cpp.

◆ is_max() [2/2]

bool constant_interval_exprt::is_max ( const exprt & expr )

static

Definition at line 1216 of file interval.cpp.

◆ is_min() [1/2]

bool constant_interval_exprt::is_min ( const constant_interval_exprt & a )

static

Definition at line 1820 of file interval.cpp.

◆ is_min() [2/2]

bool constant_interval_exprt::is_min ( const exprt & expr )

static

Definition at line 1221 of file interval.cpp.

◆ is_negative() [1/3]

bool constant_interval_exprt::is_negative ( ) const

Definition at line 1925 of file interval.cpp.

◆ is_negative() [2/3]

bool constant_interval_exprt::is_negative ( const constant_interval_exprt & interval )

static

Definition at line 1909 of file interval.cpp.

◆ is_negative() [3/3]

bool constant_interval_exprt::is_negative ( const exprt & expr )

static

Definition at line 1280 of file interval.cpp.

◆ is_numeric() [1/4]

bool constant_interval_exprt::is_numeric ( ) const

Definition at line 1080 of file interval.cpp.

◆ is_numeric() [2/4]

bool constant_interval_exprt::is_numeric ( const constant_interval_exprt & interval )

static

Definition at line 1090 of file interval.cpp.

◆ is_numeric() [3/4]

bool constant_interval_exprt::is_numeric ( const exprt & expr )

static

Definition at line 1085 of file interval.cpp.

◆ is_numeric() [4/4]

bool constant_interval_exprt::is_numeric ( const typet & type )

static

Definition at line 1075 of file interval.cpp.

◆ is_positive() [1/3]

bool constant_interval_exprt::is_positive ( ) const

Definition at line 1915 of file interval.cpp.

◆ is_positive() [2/3]

bool constant_interval_exprt::is_positive ( const constant_interval_exprt & interval )

static

Definition at line 1898 of file interval.cpp.

◆ is_positive() [3/3]

bool constant_interval_exprt::is_positive ( const exprt & expr )

static

Definition at line 1226 of file interval.cpp.

◆ is_signed() [1/4]

bool constant_interval_exprt::is_signed ( ) const

Definition at line 1181 of file interval.cpp.

◆ is_signed() [2/4]

bool constant_interval_exprt::is_signed ( const constant_interval_exprt & interval )

static

Definition at line 1149 of file interval.cpp.

◆ is_signed() [3/4]

bool constant_interval_exprt::is_signed ( const exprt & expr )

static

Definition at line 1166 of file interval.cpp.

◆ is_signed() [4/4]

bool constant_interval_exprt::is_signed ( const typet & type )

static

Definition at line 1134 of file interval.cpp.

◆ is_single_value_interval() [1/2]

bool constant_interval_exprt::is_single_value_interval ( ) const

Definition at line 1865 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 1804 of file interval.cpp.

◆ is_top() [1/2]

bool constant_interval_exprt::is_top ( ) const

Definition at line 1032 of file interval.cpp.

◆ is_top() [2/2]

bool constant_interval_exprt::is_top ( const constant_interval_exprt & a )

static

Definition at line 1810 of file interval.cpp.

◆ is_true()

tvt constant_interval_exprt::is_true ( const constant_interval_exprt & a )

static

Definition at line 1930 of file interval.cpp.

◆ is_unsigned() [1/4]

bool constant_interval_exprt::is_unsigned ( ) const

Definition at line 1186 of file interval.cpp.

◆ is_unsigned() [2/4]

bool constant_interval_exprt::is_unsigned ( const constant_interval_exprt & interval )

static

Definition at line 1154 of file interval.cpp.

◆ is_unsigned() [3/4]

bool constant_interval_exprt::is_unsigned ( const exprt & expr )

static

Definition at line 1171 of file interval.cpp.

◆ is_unsigned() [4/4]

bool constant_interval_exprt::is_unsigned ( const typet & type )

static

Definition at line 1141 of file interval.cpp.

◆ is_valid_bound()

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

inlinestatic

Definition at line 104 of file interval.h.

◆ is_well_formed()

bool constant_interval_exprt::is_well_formed ( ) const

inline

Definition at line 78 of file interval.h.

◆ is_zero() [1/3]

bool constant_interval_exprt::is_zero ( ) const

Definition at line 1920 of file interval.cpp.

◆ is_zero() [2/3]

bool constant_interval_exprt::is_zero ( const constant_interval_exprt & interval )

static

Definition at line 1904 of file interval.cpp.

◆ is_zero() [3/3]

bool constant_interval_exprt::is_zero ( const exprt & expr )

static

Definition at line 1251 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 1702 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 301 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 1745 of file interval.cpp.

◆ less_than() [2/3]

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

Definition at line 376 of file interval.cpp.

◆ less_than() [3/3]

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

static

Definition at line 1358 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 1759 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 403 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 1410 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 1940 of file interval.cpp.

◆ logical_and() [2/2]

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

Definition at line 265 of file interval.cpp.

◆ logical_not() [1/2]

tvt constant_interval_exprt::logical_not ( ) const

Definition at line 283 of file interval.cpp.

◆ logical_not() [2/2]

tvt constant_interval_exprt::logical_not ( const constant_interval_exprt & a )

static

Definition at line 1961 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 1947 of file interval.cpp.

◆ logical_or() [2/2]

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

Definition at line 254 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 1954 of file interval.cpp.

◆ logical_xor() [2/2]

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

Definition at line 273 of file interval.cpp.

◆ max()

max_value_exprt constant_interval_exprt::max ( ) const

Definition at line 1027 of file interval.cpp.

◆ min()

min_value_exprt constant_interval_exprt::min ( ) const

Definition at line 1022 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 1673 of file interval.cpp.

◆ minus() [2/2]

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

Definition at line 112 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 1694 of file interval.cpp.

◆ modulo() [2/2]

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

Definition at line 152 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 1680 of file interval.cpp.

◆ multiply() [2/2]

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

Definition at line 124 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 1780 of file interval.cpp.

◆ not_equal() [2/3]

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

Definition at line 454 of file interval.cpp.

◆ not_equal() [3/3]

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

static

Definition at line 1422 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 1666 of file interval.cpp.

◆ plus() [2/2]

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

Definition at line 74 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 1709 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 318 of file interval.cpp.

◆ simplified_expr()

exprt constant_interval_exprt::simplified_expr ( exprt expr )

static

Definition at line 987 of file interval.cpp.

◆ simplified_interval()

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

static

Definition at line 982 of file interval.cpp.

◆ singleton()

static constant_interval_exprt constant_interval_exprt::singleton ( const exprt & x )

inlinestatic

Definition at line 99 of file interval.h.

◆ to_string()

std::string constant_interval_exprt::to_string ( ) const

Definition at line 1436 of file interval.cpp.

◆ top() [1/2]

constant_interval_exprt constant_interval_exprt::top ( ) const

Definition at line 1053 of file interval.cpp.

◆ top() [2/2]

constant_interval_exprt constant_interval_exprt::top ( const typet & type )

static

Definition at line 1043 of file interval.cpp.

◆ tvt_to_interval()

constant_interval_exprt constant_interval_exprt::tvt_to_interval ( const tvt & val )

static

Definition at line 1966 of file interval.cpp.

◆ typecast()

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

Definition at line 1627 of file interval.cpp.

◆ unary_minus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_minus ( ) const

Definition at line 42 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 1621 of file interval.cpp.

◆ unary_plus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_plus ( ) const

Definition at line 37 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 1615 of file interval.cpp.

◆ zero() [1/4]

constant_exprt constant_interval_exprt::zero ( ) const

Definition at line 1017 of file interval.cpp.

◆ zero() [2/4]

constant_exprt constant_interval_exprt::zero ( const constant_interval_exprt & interval )

static

Definition at line 1012 of file interval.cpp.

◆ zero() [3/4]

constant_exprt constant_interval_exprt::zero ( const exprt & expr )

static

Definition at line 1006 of file interval.cpp.

◆ zero() [4/4]

constant_exprt constant_interval_exprt::zero ( const typet & type )

static

Definition at line 997 of file interval.cpp.

Friends And Related Function Documentation

◆ operator!

const constant_interval_exprt operator! ( const constant_interval_exprt & lhs )

friend

Definition at line 1595 of file interval.cpp.

◆ operator!=

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

friend

Definition at line 1532 of file interval.cpp.

◆ operator%

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

friend

Definition at line 1567 of file interval.cpp.

◆ operator&

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

friend

Definition at line 1574 of file interval.cpp.

◆ operator*

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

friend

Definition at line 1560 of file interval.cpp.

◆ operator+

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

friend

Definition at line 1539 of file interval.cpp.

◆ operator-

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

friend

Definition at line 1546 of file interval.cpp.

◆ operator/

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

friend

Definition at line 1553 of file interval.cpp.

◆ operator<

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

friend

Definition at line 1497 of file interval.cpp.

◆ operator<< [1/2]

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

friend

Definition at line 1600 of file interval.cpp.

◆ operator<< [2/2]

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

friend

Definition at line 1443 of file interval.cpp.

◆ operator<=

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

friend

Definition at line 1511 of file interval.cpp.

◆ operator==

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

friend

Definition at line 1525 of file interval.cpp.

◆ operator>

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

friend

Definition at line 1504 of file interval.cpp.

◆ operator>=

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

friend

Definition at line 1518 of file interval.cpp.

◆ operator>>

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

friend

Definition at line 1607 of file interval.cpp.

◆ operator^

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

friend

Definition at line 1588 of file interval.cpp.

◆ operator|

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

friend

Definition at line 1581 of file interval.cpp.

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

/home/runner/work/cbmc/cbmc/src/util/interval.h
/home/runner/work/cbmc/cbmc/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/3]

◆ constant_interval_exprt() [2/3]

◆ constant_interval_exprt() [3/3]

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]

◆ is_float() [4/4]

◆ is_int() [1/4]