Go to the documentation of this file.
74 return util_make_unique<interval_index_ranget>(interval, n);
79 while(e.
id() == ID_typecast)
90 if(type.
id() == ID_signedbv)
104 if(type.
id() == ID_signedbv)
130 INVARIANT(maybe_integer_value.has_value(),
"Input has to have a value");
131 return maybe_integer_value.value();
159 return (e.
id() == ID_constant_interval || e.
id() == ID_constant);
165 if(e.
id() == ID_constant_interval)
169 else if(e.
id() == ID_constant)
183 relation == ID_le || relation == ID_lt || relation == ID_ge ||
184 relation == ID_gt || relation == ID_equal);
185 if(relation == ID_le)
187 if(relation == ID_ge)
189 if(relation == ID_lt)
191 if(relation == ID_gt)
204 const auto &relation = e.
id();
206 const auto &lhs = binary_e.lhs();
207 const auto &rhs = binary_e.rhs();
209 relation == ID_le || relation == ID_lt || relation == ID_ge ||
210 relation == ID_gt || relation == ID_equal);
211 PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
212 PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
215 const auto the_constant_part_of_the_relation =
216 (rhs.id() == ID_symbol ? lhs : rhs);
217 const auto maybe_inverted_relation =
220 if(maybe_inverted_relation == ID_le)
222 if(maybe_inverted_relation == ID_lt)
224 if(maybe_inverted_relation == ID_ge)
226 if(maybe_inverted_relation == ID_gt)
229 maybe_inverted_relation == ID_equal,
"We excluded other cases above");
231 the_constant_part_of_the_relation, the_constant_part_of_the_relation);
323 std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
324 return cast_other &&
interval == cast_other->interval;
334 std::string lower_string;
335 std::string upper_string;
339 lower_string =
"-INF";
345 "We only support constant limits");
352 upper_string =
"+INF";
358 "We only support constant limits");
363 out <<
"[" << lower_string <<
", " << upper_string <<
"]";
379 widened.widened_lower_bound, widened.widened_upper_bound);
387 if(other->is_bottom())
388 return shared_from_this();
390 auto other_interval = other->to_interval();
396 return shared_from_this();
412 auto other_interval = other->to_interval();
414 if(other_interval.contains(
interval))
415 return shared_from_this();
451 const exprt &upper)
const
474 return and_exprt(lower_bound, upper_bound);
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
mp_integer smallest() const
Return the smallest value that can be represented using this type.
The type of an expression, extends irept.
bool advance_to_next() override
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
static exprt get_max(const exprt &a, const exprt &b)
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
static bool is_bottom(const constant_interval_exprt &a)
+∞ upper bound for intervals
bool contains(const constant_interval_exprt &interval) const
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
Meet another interval abstract object with this one.
The plus expression Associativity is not specified.
Base class for all expressions.
-∞ upper bound for intervals
bool is_true() const
Return whether the expression is a constant representing true.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
exprt to_constant() const override
Converts to a constant expression if possible.
static index_range_implementation_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
void set_top_internal() override
const constant_interval_exprt & interval
Represents an interval of values.
tvt greater_than(const constant_interval_exprt &o) const
bool is_false() const
Return whether the expression is a constant representing false.
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
size_t internal_hash() const override
index_range_implementation_ptrt make_empty_index_range()
typet & type()
Return the type of the expression.
static mp_integer force_value_from_expr(const exprt &value)
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
const std::string & id2string(const irep_idt &d)
bool is_single_value_interval() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
Pre-defined bitvector types.
static exprt look_through_casts(exprt e)
static exprt next_element(const exprt &cur, const namespacet &ns)
An abstract version of a program environment.
constant_interval_exprt bottom() const
virtual exprt to_constant() const
Converts to a constant expression if possible.
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
exprt simplify_expr(exprt src, const namespacet &ns)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
const irep_idt & id() const
static constant_interval_exprt make_interval_expr(exprt e)
std::set< abstract_object_pointert > abstract_object_visitedt
bool new_interval_is_top(const constant_interval_exprt &e)
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
nonstd::optional< T > optionalt
index_range_implementation_ptrt reset() const override
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
Merge another interval abstract object with this one.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
bool is_zero() const
Return whether the expression is a constant representing 0.
static bool represents_interval(exprt e)
static bool is_top(const constant_interval_exprt &a)
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
bool internal_equality(const abstract_object_pointert &other) const override
Statistics gathering for the variable senstivity domain.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
An interval to represent a set of possible values.
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
A base class for relations, i.e., binary predicates whose two operands have the same type.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
This is the basic interface of the abstract interpreter with default implementations of the core func...
interval_abstract_valuet(const typet &t)
std::size_t number_of_single_value_intervals
tvt less_than_or_equal(const constant_interval_exprt &o) const
const exprt & get_lower() const
mp_integer largest() const
Return the largest value that can be represented using this type.
bool is_one() const
Return whether the expression is a constant representing 1.
const exprt & current() const override
const exprt & get_upper() const
static exprt get_min(const exprt &a, const exprt &b)
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
constant_interval_exprt interval
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
value_range_implementation_ptrt value_range_implementation() const override
abstract_object_pointert widening_merge(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
const irep_idt & get_value() const
static memory_sizet from_bytes(std::size_t bytes)
interval_index_ranget(const constant_interval_exprt &interval_, const namespacet &n)
virtual internal_abstract_object_pointert mutable_clone() const
static irep_idt invert_relation(const irep_idt &relation)
std::size_t number_of_interval_abstract_objects
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.