Go to the documentation of this file.
91 "We just excluded this case");
103 "We just excluded that case");
200 "Zero should be between a negative and a positive value");
223 if(
type().
id() == ID_bool)
244 "If an interval contains zero its lower bound can't be positive"
245 " and its upper bound can't be negative");
472 std::vector<exprt> results;
479 for(
auto result : results)
494 std::vector<exprt> values,
500 if(values.size() == 0)
505 if(values.size() == 1)
507 return *(values.begin());
510 if(values.size() == 2)
514 return get_min(values.front(), values.back());
518 return get_max(values.front(), values.back());
526 if((min_value &&
is_min(v)) || (!min_value &&
is_max(v)))
532 for(
auto left : values)
534 bool all_left_OP_right =
true;
536 for(
auto right : values)
545 all_left_OP_right =
false;
549 if(all_left_OP_right)
572 std::vector<exprt> &collection)
574 if(operation == ID_mult)
578 else if(operation == ID_div)
582 else if(operation == ID_mod)
586 else if(operation == ID_shl || operation == ID_ashr)
600 std::vector<exprt> &collection)
624 "We ruled out extreme cases beforehand");
637 std::vector<exprt> &collection)
647 collection.push_back(expr);
663 std::vector<exprt> &collection)
670 collection.push_back(
min);
672 collection.push_back(other);
723 is_signed(
rhs),
"We think this is a signed integer for some reason?");
729 "We ruled out extreme cases beforehand");
783 "We ruled out extreme values beforehand");
791 if(
id == ID_unary_plus)
795 if(
id == ID_unary_minus)
815 if(binary_operator == ID_plus)
819 if(binary_operator == ID_minus)
823 if(binary_operator == ID_mult)
827 if(binary_operator == ID_div)
831 if(binary_operator == ID_mod)
835 if(binary_operator == ID_shl)
839 if(binary_operator == ID_ashr)
843 if(binary_operator == ID_bitor)
847 if(binary_operator == ID_bitand)
851 if(binary_operator == ID_bitxor)
855 if(binary_operator == ID_lt)
859 if(binary_operator == ID_le)
863 if(binary_operator == ID_gt)
867 if(binary_operator == ID_ge)
871 if(binary_operator == ID_equal)
875 if(binary_operator == ID_notequal)
879 if(binary_operator == ID_and)
883 if(binary_operator == ID_or)
887 if(binary_operator == ID_xor)
900 PRECONDITION(operation == ID_shl || operation == ID_ashr);
928 "We ruled out extreme cases beforehand");
998 "The value created from 0 should be zero or false");
1099 return src.
id() == ID_floatbv;
1109 return interval.
is_int();
1124 return t.
id() == ID_bv || t.
id() == ID_signedbv || t.
id() == ID_unsignedbv ||
1125 t.
id() == ID_c_bool ||
1131 return t.
id() == ID_signedbv ||
1137 return t.
id() == ID_bv || t.
id() == ID_unsignedbv || t.
id() == ID_c_bool ||
1138 t.
id() == ID_c_enum ||
1211 return expr.
id() == ID_max;
1216 return expr.
id() == ID_min;
1281 is_signed(expr),
"We don't support anything other than integers yet");
1319 "Best we can do now is a==b?, but this is covered by the above, so "
1383 "These cases should have all been handled before this point");
1393 "We have excluded all of these cases in the code above");
1417 return !
equal(a, b);
1431 std::stringstream out;
1445 out << integer2string(*numeric_cast<mp_integer>(i.
get_lower()));
1475 out << integer2string(*numeric_cast<mp_integer>(i.
get_upper()));
1543 return lhs.
minus(rhs);
1637 if(e.id() == ID_min || e.id() == ID_max)
1832 if(it->has_operands())
tvt is_definitely_true() const
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
constant_interval_exprt unary_plus() const
bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
const typet & subtype() const
const constant_interval_exprt operator^(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
constant_interval_exprt right_shift(const constant_interval_exprt &o) const
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
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)
constant_interval_exprt decrement() const
bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
The type of an expression, extends irept.
static exprt simplified_expr(exprt expr)
static exprt get_max(const exprt &a, const exprt &b)
static bool is_bottom(const constant_interval_exprt &a)
+∞ upper bound for intervals
bool contains(const constant_interval_exprt &interval) const
static void append_multiply_expression_max(const exprt &expr, std::vector< exprt > &collection)
Appends interval bounds that could arise from MAX * expr.
The plus expression Associativity is not specified.
Base class for all expressions.
static bool is_extreme(const exprt &expr)
Generic base class for unary expressions.
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
-∞ upper bound for intervals
bool is_true() const
Return whether the expression is a constant representing true.
const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool is_bitvector() const
Represents an interval of values.
constant_exprt zero() const
tvt greater_than(const constant_interval_exprt &o) const
bool is_false() const
Return whether the expression is a constant representing false.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
tvt not_equal(const constant_interval_exprt &o) const
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
typet & type()
Return the type of the expression.
bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
constant_interval_exprt bitwise_not() const
static bool contains_extreme(const exprt expr)
constant_interval_exprt multiply(const constant_interval_exprt &o) const
static bool is_max(const constant_interval_exprt &a)
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
#define forall_operands(it, expr)
bool is_single_value_interval() const
#define PRECONDITION(CONDITION)
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.
constant_interval_exprt eval(const irep_idt &unary_operator) const
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
constant_interval_exprt plus(const constant_interval_exprt &o) const
constant_interval_exprt bottom() const
Binary multiplication Associativity is not specified.
exprt simplify_expr(exprt src, const namespacet &ns)
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
constant_interval_exprt increment() const
constant_interval_exprt modulo(const constant_interval_exprt &o) const
tvt less_than(const constant_interval_exprt &o) const
The unary minus expression.
tvt logical_or(const constant_interval_exprt &o) const
const irep_idt & id() const
The Boolean constant false.
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)
constant_interval_exprt minus(const constant_interval_exprt &other) const
bool is_zero() const
Return whether the expression is a constant representing 0.
static bool is_top(const constant_interval_exprt &a)
bool has_no_upper_bound() const
A base class for shift operators.
#define POSTCONDITION(CONDITION)
constant_interval_exprt(const exprt &lower, const exprt &upper, const typet type)
static exprt get_extreme(std::vector< exprt > values, bool min=true)
bool has_no_lower_bound() const
bool contains_zero() const
const irep_idt & get(const irep_namet &name) const
constant_interval_exprt typecast(const typet &type) const
const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool operator<=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
static constant_interval_exprt tvt_to_interval(const tvt &val)
tvt less_than_or_equal(const constant_interval_exprt &o) const
std::ostream & operator<<(std::ostream &out, const constant_interval_exprt &i)
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
const exprt & get_lower() const
static bool is_min(const constant_interval_exprt &a)
static exprt abs(const exprt &expr)
tvt is_definitely_false() const
bool is_one() const
Return whether the expression is a constant representing 1.
const exprt & get_upper() const
static exprt get_min(const exprt &a, const exprt &b)
constant_interval_exprt top() const
const constant_interval_exprt operator-(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Semantic type conversion.
tvt greater_than_or_equal(const constant_interval_exprt &o) const
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 ...
The Boolean constant true.
A constant literal expression.
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
constant_interval_exprt divide(const constant_interval_exprt &o) const
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
API to expression classes.
tvt logical_and(const constant_interval_exprt &o) const
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
constant_interval_exprt unary_minus() const
tvt logical_xor(const constant_interval_exprt &o) const
std::string to_string() const
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
tvt equal(const constant_interval_exprt &o) const