94 "We just excluded this case");
106 "We just excluded that case");
203 "Zero should be between a negative and a positive value");
226 if(
type().
id() == ID_bool)
247 "If an interval contains zero its lower bound can't be positive"
248 " and its upper bound can't be negative");
475 std::vector<exprt> results;
482 for(
auto result : results)
497 std::vector<exprt> values,
503 if(values.size() == 0)
508 if(values.size() == 1)
510 return *(values.begin());
513 if(values.size() == 2)
517 return get_min(values.front(), values.back());
521 return get_max(values.front(), values.back());
529 if((min_value &&
is_min(v)) || (!min_value &&
is_max(v)))
535 for(
auto left : values)
537 bool all_left_OP_right =
true;
539 for(
auto right : values)
548 all_left_OP_right =
false;
552 if(all_left_OP_right)
575 std::vector<exprt> &collection)
577 if(operation == ID_mult)
581 else if(operation == ID_div)
585 else if(operation == ID_mod)
589 else if(operation == ID_shl || operation == ID_ashr)
603 std::vector<exprt> &collection)
627 "We ruled out extreme cases beforehand");
640 std::vector<exprt> &collection)
650 collection.push_back(expr);
666 std::vector<exprt> &collection)
673 collection.push_back(
min);
675 collection.push_back(other);
726 is_signed(
rhs),
"We think this is a signed integer for some reason?");
732 "We ruled out extreme cases beforehand");
786 "We ruled out extreme values beforehand");
794 if(
id == ID_unary_plus)
798 if(
id == ID_unary_minus)
818 if(binary_operator == ID_plus)
822 if(binary_operator == ID_minus)
826 if(binary_operator == ID_mult)
830 if(binary_operator == ID_div)
834 if(binary_operator == ID_mod)
838 if(binary_operator == ID_shl)
842 if(binary_operator == ID_ashr)
846 if(binary_operator == ID_bitor)
850 if(binary_operator == ID_bitand)
854 if(binary_operator == ID_bitxor)
858 if(binary_operator == ID_lt)
862 if(binary_operator == ID_le)
866 if(binary_operator == ID_gt)
870 if(binary_operator == ID_ge)
874 if(binary_operator == ID_equal)
878 if(binary_operator == ID_notequal)
882 if(binary_operator == ID_and)
886 if(binary_operator == ID_or)
890 if(binary_operator == ID_xor)
903 PRECONDITION(operation == ID_shl || operation == ID_ashr);
931 "We ruled out extreme cases beforehand");
1001 "The value created from 0 should be zero or false");
1102 return src.
id() == ID_floatbv;
1112 return interval.
is_int();
1127 return t.
id() == ID_bv || t.
id() == ID_signedbv || t.
id() == ID_unsignedbv ||
1128 t.
id() == ID_c_bool ||
1129 (t.
id() == ID_c_bit_field &&
1135 return t.
id() == ID_signedbv ||
1136 (t.
id() == ID_c_bit_field &&
1142 return t.
id() == ID_bv || t.
id() == ID_unsignedbv || t.
id() == ID_c_bool ||
1143 t.
id() == ID_c_enum ||
1144 (t.
id() == ID_c_bit_field &&
1217 return expr.
id() == ID_max;
1222 return expr.
id() == ID_min;
1287 is_signed(expr),
"We don't support anything other than integers yet");
1325 "Best we can do now is a==b?, but this is covered by the above, so "
1389 "These cases should have all been handled before this point");
1399 "We have excluded all of these cases in the code above");
1423 return !
equal(a, b);
1437 std::stringstream out;
1451 out << integer2string(*numeric_cast<mp_integer>(i.
get_lower()));
1481 out << integer2string(*numeric_cast<mp_integer>(i.
get_upper()));
1549 return lhs.
minus(rhs);
1643 if(e.id() == ID_min || e.id() == ID_max)
1838 if(it->has_operands())
API to expression classes for bitvectors.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
A constant literal expression.
Represents an interval of values.
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
static bool is_bottom(const constant_interval_exprt &a)
constant_interval_exprt bottom() const
constant_interval_exprt minus(const constant_interval_exprt &other) const
tvt greater_than_or_equal(const constant_interval_exprt &o) const
tvt greater_than(const constant_interval_exprt &o) const
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
constant_interval_exprt decrement() const
tvt less_than_or_equal(const constant_interval_exprt &o) const
tvt is_definitely_false() const
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
tvt not_equal(const constant_interval_exprt &o) const
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
bool has_no_upper_bound() const
static bool is_top(const constant_interval_exprt &a)
constant_interval_exprt typecast(const typet &type) const
constant_interval_exprt multiply(const constant_interval_exprt &o) const
static constant_interval_exprt tvt_to_interval(const tvt &val)
constant_interval_exprt unary_plus() const
constant_interval_exprt plus(const constant_interval_exprt &o) const
static exprt get_extreme(std::vector< exprt > values, bool min=true)
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 ...
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
bool is_single_value_interval() const
constant_interval_exprt increment() const
bool is_bitvector() const
std::string to_string() const
bool contains(const constant_interval_exprt &interval) const
static bool is_extreme(const exprt &expr)
tvt logical_or(const constant_interval_exprt &o) const
static exprt simplified_expr(exprt expr)
bool contains_zero() const
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
constant_interval_exprt modulo(const constant_interval_exprt &o) const
static exprt get_max(const exprt &a, const exprt &b)
bool has_no_lower_bound() const
static exprt get_min(const exprt &a, const exprt &b)
static bool is_max(const constant_interval_exprt &a)
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
constant_interval_exprt eval(const irep_idt &unary_operator) const
tvt is_definitely_true() const
static bool is_min(const constant_interval_exprt &a)
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
tvt logical_xor(const constant_interval_exprt &o) const
const exprt & get_lower() const
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 right_shift(const constant_interval_exprt &o) const
tvt logical_and(const constant_interval_exprt &o) const
static void append_multiply_expression_max(const exprt &expr, std::vector< exprt > &collection)
Appends interval bounds that could arise from MAX * expr.
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
constant_interval_exprt top() const
static bool contains_extreme(const exprt expr)
constant_interval_exprt unary_minus() const
constant_exprt zero() const
tvt less_than(const constant_interval_exprt &o) const
static exprt abs(const exprt &expr)
constant_interval_exprt bitwise_not() const
constant_interval_exprt divide(const constant_interval_exprt &o) const
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
const exprt & get_upper() const
tvt equal(const constant_interval_exprt &o) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_one() const
Return whether the expression is a constant representing 1.
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_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
+∞ upper bound for intervals
-∞ upper bound for intervals
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
A base class for shift and rotate operators.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
The unary minus expression.
#define forall_operands(it, expr)
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)
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)
bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
std::ostream & operator<<(std::ostream &out, const constant_interval_exprt &i)
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)
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)
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)
bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION(CONDITION)
API to expression classes.