Go to the documentation of this file.
73 return util_make_unique<interval_index_ranget>(interval, n);
78 while(e.
id() == ID_typecast)
89 if(type.
id() == ID_signedbv)
103 if(type.
id() == ID_signedbv)
129 INVARIANT(maybe_integer_value.has_value(),
"Input has to have a value");
130 return maybe_integer_value.value();
158 return (e.
id() == ID_constant_interval || e.
id() == ID_constant);
164 if(e.
id() == ID_constant_interval)
168 else if(e.
id() == ID_constant)
182 relation == ID_le || relation == ID_lt || relation == ID_ge ||
183 relation == ID_gt || relation == ID_equal);
184 if(relation == ID_le)
186 if(relation == ID_ge)
188 if(relation == ID_lt)
190 if(relation == ID_gt)
203 const auto &relation = e.
id();
205 const auto &lhs = binary_e.lhs();
206 const auto &rhs = binary_e.rhs();
208 relation == ID_le || relation == ID_lt || relation == ID_ge ||
209 relation == ID_gt || relation == ID_equal);
210 PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
211 PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
214 const auto the_constant_part_of_the_relation =
215 (rhs.id() == ID_symbol ? lhs : rhs);
216 const auto maybe_inverted_relation =
219 if(maybe_inverted_relation == ID_le)
221 if(maybe_inverted_relation == ID_lt)
223 if(maybe_inverted_relation == ID_ge)
225 if(maybe_inverted_relation == ID_gt)
228 maybe_inverted_relation == ID_equal,
"We excluded other cases above");
230 the_constant_part_of_the_relation, the_constant_part_of_the_relation);
294 std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
295 return cast_other &&
interval == cast_other->interval;
305 std::string lower_string;
306 std::string upper_string;
310 lower_string =
"-INF";
316 "We only support constant limits");
323 upper_string =
"+INF";
329 "We only support constant limits");
334 out <<
"[" << lower_string <<
", " << upper_string <<
"]";
346 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
367 if(other->is_bottom())
368 return shared_from_this();
370 auto other_interval = other->to_interval();
373 return std::make_shared<interval_abstract_valuet>(other_interval);
376 return shared_from_this();
389 std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
411 return shared_from_this();
425 return std::make_shared<interval_abstract_valuet>(
427 return std::make_shared<interval_abstract_valuet>(
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< const abstract_value_objectt > abstract_value_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
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
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
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
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)
abstract_object_pointert merge_intervals(abstract_value_pointert &other) const
Merge another interval abstract object with this one.
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.
const constant_interval_exprt & interval
Represents an interval of values.
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
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
index_range_implementation_ptrt make_empty_index_range()
typet & type()
Return the type of the expression.
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
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.
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
tvt less_than(const constant_interval_exprt &o) const
const irep_idt & id() const
static constant_interval_exprt make_interval_expr(exprt e)
std::set< abstract_object_pointert > abstract_object_visitedt
nonstd::optional< T > optionalt
index_range_implementation_ptrt reset() const override
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
static bool represents_interval(exprt e)
static bool is_top(const constant_interval_exprt &a)
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
bool internal_equality(const abstract_object_pointert &other) const override
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.
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
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)
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
std::size_t number_of_single_value_intervals
const exprt & get_lower() const
mp_integer largest() const
Return the largest value that can be represented using this type.
const exprt & current() const override
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
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
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
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)
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.