cprover
|
Represents an interval of values. More...
#include <interval.h>
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. | |
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 |
![]() | |
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 |
![]() | |
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. | |
const typet & | type () const |
bool | has_operands () const |
Return true if there is at least one operand. | |
operandst & | operands () |
const operandst & | operands () const |
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. | |
void | add_to_operands (const exprt &expr) |
Add the given argument to the end of exprt 's operands. | |
void | add_to_operands (exprt &&expr) |
Add the given argument to the end of exprt 's operands. | |
void | copy_to_operands (const exprt &e1, const exprt &e2) |
Copy the given arguments to the end of exprt 's operands. | |
void | add_to_operands (const exprt &e1, const exprt &e2) |
Add the given arguments to the end of exprt 's operands. | |
void | add_to_operands (exprt &&e1, exprt &&e2) |
Add the given arguments to the end of exprt 's operands. | |
void | add_to_operands (const exprt &e1, const exprt &e2, const exprt &e3) |
Add the given arguments to the end of exprt 's operands. | |
void | copy_to_operands (const exprt &e1, const exprt &e2, const exprt &e3) |
Copy the given arguments to the end of exprt 's operands. | |
void | add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3) |
Add the given arguments to the end of exprt 's operands. | |
bool | is_constant () const |
Return whether the expression is a constant. | |
bool | is_true () const |
Return whether the expression is a constant representing true . | |
bool | is_false () const |
Return whether the expression is a constant representing false . | |
bool | is_zero () const |
Return whether the expression is a constant representing 0. | |
bool | is_one () const |
Return whether the expression is a constant representing 1. | |
bool | is_boolean () const |
Return whether the expression represents a Boolean. | |
const source_locationt & | find_source_location () const |
Get a source_locationt from the expression or from its operands (non-recursively). | |
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. | |
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. | |
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 |
![]() | |
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 | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation | |
int | compare (const irept &i) const |
defines ordering on the internal representation comments are ignored | |
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 |
![]() | |
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. | |
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 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 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). | |
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. | |
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) | |
![]() | |
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 | |
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). | |
static void | append_multiply_expression_max (const exprt &expr, std::vector< exprt > &collection) |
Appends interval bounds that could arise from MAX * expr. | |
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. | |
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) |
Additional Inherited Members | |
![]() | |
typedef std::vector< exprt > | operandst |
![]() | |
using | baset = tree_implementationt |
![]() | |
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. | |
![]() | |
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 |
![]() | |
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 |
![]() | |
void | detach () |
![]() | |
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. | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
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.
|
inline |
Definition at line 50 of file interval.h.
|
inline |
Definition at line 59 of file interval.h.
|
inlineexplicit |
Definition at line 64 of file interval.h.
|
inlineexplicit |
Definition at line 69 of file interval.h.
|
inline |
Definition at line 74 of file interval.h.
Definition at line 1299 of file interval.cpp.
|
staticprivate |
Adds all possible values that may arise from multiplication (more than one, in case of past the type boundary results).
lower | lhs of multiplication |
upper | rhs of multiplication |
collection | vector of possible values |
Definition at line 600 of file interval.cpp.
|
staticprivate |
Appends interval bounds that could arise from MAX * expr.
Accommodates for overflows by over-approximating.
expr | the unknown side of multiplication |
collection | vector of collected bounds |
Definition at line 638 of file interval.cpp.
|
staticprivate |
Appends interval bounds that could arise from MIN * other.
Accommodates for overflows by over-approximating.
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.
|
static |
Definition at line 1737 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::bitwise_and | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 357 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::bitwise_not | ( | ) | const |
Definition at line 367 of file interval.cpp.
|
static |
Definition at line 1717 of file interval.cpp.
|
static |
Definition at line 1730 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::bitwise_or | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 346 of file interval.cpp.
|
static |
Definition at line 1723 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::bitwise_xor | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 335 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::bottom | ( | ) | const |
Definition at line 1057 of file interval.cpp.
|
static |
Definition at line 1047 of file interval.cpp.
bool constant_interval_exprt::contains | ( | const constant_interval_exprt & | interval | ) | const |
Definition at line 1426 of file interval.cpp.
|
static |
Definition at line 1829 of file interval.cpp.
Definition at line 1847 of file interval.cpp.
bool constant_interval_exprt::contains_zero | ( | ) | const |
Definition at line 1870 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::decrement | ( | ) | const |
Definition at line 465 of file interval.cpp.
|
static |
Definition at line 1793 of file interval.cpp.
|
static |
Definition at line 1686 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::divide | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 137 of file interval.cpp.
|
static |
Definition at line 1772 of file interval.cpp.
tvt constant_interval_exprt::equal | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 432 of file interval.cpp.
END SET OF ARITHMETIC OPERATORS.
Definition at line 1314 of file interval.cpp.
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.
constant_interval_exprt constant_interval_exprt::eval | ( | const irep_idt & | unary_operator | ) | const |
Definition at line 792 of file interval.cpp.
|
staticprivate |
Definition at line 683 of file interval.cpp.
|
staticprivate |
Definition at line 571 of file interval.cpp.
|
staticprivate |
Definition at line 738 of file interval.cpp.
|
staticprivate |
Definition at line 898 of file interval.cpp.
Definition at line 496 of file interval.cpp.
|
static |
Definition at line 470 of file interval.cpp.
const exprt & constant_interval_exprt::get_lower | ( | ) | const |
Definition at line 29 of file interval.cpp.
Definition at line 959 of file interval.cpp.
Definition at line 974 of file interval.cpp.
Definition at line 964 of file interval.cpp.
Definition at line 969 of file interval.cpp.
const exprt & constant_interval_exprt::get_upper | ( | ) | const |
Definition at line 34 of file interval.cpp.
|
static |
Definition at line 1751 of file interval.cpp.
tvt constant_interval_exprt::greater_than | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 398 of file interval.cpp.
Definition at line 1404 of file interval.cpp.
|
static |
Definition at line 1765 of file interval.cpp.
tvt constant_interval_exprt::greater_than_or_equal | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 426 of file interval.cpp.
Definition at line 1414 of file interval.cpp.
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.
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.
bool constant_interval_exprt::has_no_lower_bound | ( | ) | const |
Definition at line 1210 of file interval.cpp.
bool constant_interval_exprt::has_no_upper_bound | ( | ) | const |
Definition at line 1205 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::increment | ( | ) | const |
Definition at line 460 of file interval.cpp.
|
static |
Definition at line 1787 of file interval.cpp.
bool constant_interval_exprt::is_bitvector | ( | ) | const |
Definition at line 1190 of file interval.cpp.
|
static |
Definition at line 1159 of file interval.cpp.
|
static |
Definition at line 1175 of file interval.cpp.
|
static |
Definition at line 1125 of file interval.cpp.
bool constant_interval_exprt::is_bottom | ( | ) | const |
Definition at line 1036 of file interval.cpp.
|
static |
Definition at line 1814 of file interval.cpp.
tvt constant_interval_exprt::is_definitely_false | ( | ) | const |
Definition at line 224 of file interval.cpp.
tvt constant_interval_exprt::is_definitely_true | ( | ) | const |
Definition at line 218 of file interval.cpp.
bool constant_interval_exprt::is_empty | ( | ) | const |
Definition at line 1854 of file interval.cpp.
|
static |
Definition at line 1798 of file interval.cpp.
|
static |
Definition at line 1195 of file interval.cpp.
Definition at line 1200 of file interval.cpp.
|
static |
Definition at line 1934 of file interval.cpp.
bool constant_interval_exprt::is_float | ( | ) | const |
Definition at line 1069 of file interval.cpp.
|
static |
Definition at line 1120 of file interval.cpp.
|
static |
Definition at line 1115 of file interval.cpp.
|
static |
Definition at line 1100 of file interval.cpp.
bool constant_interval_exprt::is_int | ( | ) | const |
Definition at line 1064 of file interval.cpp.
|
static |
Definition at line 1110 of file interval.cpp.
|
static |
Definition at line 1105 of file interval.cpp.
|
static |
Definition at line 1095 of file interval.cpp.
|
static |
Definition at line 1824 of file interval.cpp.
|
static |
Definition at line 1215 of file interval.cpp.
|
static |
Definition at line 1819 of file interval.cpp.
|
static |
Definition at line 1220 of file interval.cpp.
bool constant_interval_exprt::is_negative | ( | ) | const |
Definition at line 1924 of file interval.cpp.
|
static |
Definition at line 1908 of file interval.cpp.
|
static |
Definition at line 1279 of file interval.cpp.
bool constant_interval_exprt::is_numeric | ( | ) | const |
Definition at line 1079 of file interval.cpp.
|
static |
Definition at line 1089 of file interval.cpp.
|
static |
Definition at line 1084 of file interval.cpp.
|
static |
Definition at line 1074 of file interval.cpp.
bool constant_interval_exprt::is_positive | ( | ) | const |
Definition at line 1914 of file interval.cpp.
|
static |
Definition at line 1897 of file interval.cpp.
|
static |
Definition at line 1225 of file interval.cpp.
bool constant_interval_exprt::is_signed | ( | ) | const |
Definition at line 1180 of file interval.cpp.
|
static |
Definition at line 1148 of file interval.cpp.
|
static |
Definition at line 1165 of file interval.cpp.
|
static |
Definition at line 1133 of file interval.cpp.
bool constant_interval_exprt::is_single_value_interval | ( | ) | const |
Definition at line 1864 of file interval.cpp.
|
static |
Definition at line 1803 of file interval.cpp.
bool constant_interval_exprt::is_top | ( | ) | const |
Definition at line 1031 of file interval.cpp.
|
static |
Definition at line 1809 of file interval.cpp.
|
static |
Definition at line 1929 of file interval.cpp.
bool constant_interval_exprt::is_unsigned | ( | ) | const |
Definition at line 1185 of file interval.cpp.
|
static |
Definition at line 1153 of file interval.cpp.
|
static |
Definition at line 1170 of file interval.cpp.
|
static |
Definition at line 1140 of file interval.cpp.
|
inline |
Definition at line 100 of file interval.h.
|
inline |
Definition at line 79 of file interval.h.
bool constant_interval_exprt::is_zero | ( | ) | const |
Definition at line 1919 of file interval.cpp.
|
static |
Definition at line 1903 of file interval.cpp.
|
static |
Definition at line 1250 of file interval.cpp.
|
static |
Definition at line 1701 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::left_shift | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 302 of file interval.cpp.
|
static |
Definition at line 1744 of file interval.cpp.
tvt constant_interval_exprt::less_than | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 377 of file interval.cpp.
Definition at line 1357 of file interval.cpp.
|
static |
Definition at line 1758 of file interval.cpp.
tvt constant_interval_exprt::less_than_or_equal | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 404 of file interval.cpp.
Definition at line 1409 of file interval.cpp.
|
static |
Definition at line 1939 of file interval.cpp.
tvt constant_interval_exprt::logical_and | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 266 of file interval.cpp.
tvt constant_interval_exprt::logical_not | ( | ) | const |
Definition at line 284 of file interval.cpp.
|
static |
Definition at line 1960 of file interval.cpp.
|
static |
Definition at line 1946 of file interval.cpp.
tvt constant_interval_exprt::logical_or | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 255 of file interval.cpp.
|
static |
Definition at line 1953 of file interval.cpp.
tvt constant_interval_exprt::logical_xor | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 274 of file interval.cpp.
max_exprt constant_interval_exprt::max | ( | ) | const |
Definition at line 1026 of file interval.cpp.
min_exprt constant_interval_exprt::min | ( | ) | const |
Definition at line 1021 of file interval.cpp.
|
static |
Definition at line 1672 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::minus | ( | const constant_interval_exprt & | other | ) | const |
Definition at line 114 of file interval.cpp.
|
static |
Definition at line 1693 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::modulo | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 154 of file interval.cpp.
|
static |
Definition at line 1679 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::multiply | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 126 of file interval.cpp.
|
static |
Definition at line 1779 of file interval.cpp.
tvt constant_interval_exprt::not_equal | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 455 of file interval.cpp.
Definition at line 1421 of file interval.cpp.
|
static |
Definition at line 1665 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::plus | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 76 of file interval.cpp.
|
static |
Definition at line 1708 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::right_shift | ( | const constant_interval_exprt & | o | ) | const |
Definition at line 319 of file interval.cpp.
Definition at line 986 of file interval.cpp.
|
static |
Definition at line 981 of file interval.cpp.
std::string constant_interval_exprt::to_string | ( | ) | const |
Definition at line 1435 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::top | ( | ) | const |
Definition at line 1052 of file interval.cpp.
|
static |
Definition at line 1042 of file interval.cpp.
|
static |
Definition at line 1965 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::typecast | ( | const typet & | type | ) | const |
Definition at line 1626 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::unary_minus | ( | ) | const |
Definition at line 44 of file interval.cpp.
|
static |
Definition at line 1620 of file interval.cpp.
constant_interval_exprt constant_interval_exprt::unary_plus | ( | ) | const |
Definition at line 39 of file interval.cpp.
|
static |
Definition at line 1614 of file interval.cpp.
constant_exprt constant_interval_exprt::zero | ( | ) | const |
Definition at line 1016 of file interval.cpp.
|
static |
Definition at line 1011 of file interval.cpp.
|
static |
Definition at line 1005 of file interval.cpp.
|
static |
Definition at line 996 of file interval.cpp.
|
friend |
Definition at line 1594 of file interval.cpp.
|
friend |
Definition at line 1531 of file interval.cpp.
|
friend |
Definition at line 1566 of file interval.cpp.
|
friend |
Definition at line 1573 of file interval.cpp.
|
friend |
Definition at line 1559 of file interval.cpp.
|
friend |
Definition at line 1538 of file interval.cpp.
|
friend |
Definition at line 1545 of file interval.cpp.
|
friend |
Definition at line 1552 of file interval.cpp.
|
friend |
Definition at line 1496 of file interval.cpp.
|
friend |
Definition at line 1599 of file interval.cpp.
|
friend |
Definition at line 1442 of file interval.cpp.
|
friend |
Definition at line 1510 of file interval.cpp.
|
friend |
Definition at line 1524 of file interval.cpp.
|
friend |
Definition at line 1503 of file interval.cpp.
|
friend |
Definition at line 1517 of file interval.cpp.
|
friend |
Definition at line 1606 of file interval.cpp.
|
friend |
Definition at line 1587 of file interval.cpp.
|
friend |
Definition at line 1580 of file interval.cpp.