cprover
interval_abstract_value.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity intervals
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include <ostream>
10 
11 #include <util/arith_tools.h>
12 #include <util/bitvector_types.h>
13 #include <util/invariant.h>
14 #include <util/make_unique.h>
15 #include <util/simplify_expr.h>
16 
17 #include "abstract_environment.h"
20 #include "widened_range.h"
21 
23  const constant_interval_exprt &interval,
24  const namespacet &n);
25 
27 {
28 public:
30  const constant_interval_exprt &interval_,
31  const namespacet &n)
32  : interval(interval_),
33  index(nil_exprt()),
34  next(interval.get_lower()),
35  upper(interval.get_upper()),
36  ns(n)
37  {
38  }
39 
40  const exprt &current() const override
41  {
42  return index;
43  }
44  bool advance_to_next() override
45  {
46  index = next;
49  .is_true();
50  }
51 
53  {
55  }
56 
57 private:
58  static exprt next_element(const exprt &cur, const namespacet &ns)
59  {
60  return simplify_expr(plus_exprt(cur, from_integer(1, cur.type())), ns);
61  }
62 
67  const namespacet &ns;
68 };
69 
71  const constant_interval_exprt &interval,
72  const namespacet &n)
73 {
74  return util_make_unique<interval_index_ranget>(interval, n);
75 }
76 
77 static inline exprt look_through_casts(exprt e)
78 {
79  while(e.id() == ID_typecast)
80  {
81  e = to_typecast_expr(e).op();
82  }
83  return e;
84 }
85 
86 static inline bool
87 bvint_value_is_max(const typet &type, const mp_integer &value)
88 {
89  PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
90  if(type.id() == ID_signedbv)
91  {
92  return to_signedbv_type(type).largest() == value;
93  }
94  else
95  {
96  return to_unsignedbv_type(type).largest() == value;
97  }
98 }
99 
100 static inline bool
101 bvint_value_is_min(const typet &type, const mp_integer &value)
102 {
103  PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
104  if(type.id() == ID_signedbv)
105  {
106  return to_signedbv_type(type).smallest() == value;
107  }
108  else
109  {
110  return to_unsignedbv_type(type).smallest() == value;
111  }
112 }
113 
114 static inline constant_interval_exprt
116 {
117  return constant_interval_exprt(min_exprt(value.type()), value);
118 }
119 
120 static inline constant_interval_exprt
122 {
123  return constant_interval_exprt(value, max_exprt(value.type()));
124 }
125 
126 static inline mp_integer force_value_from_expr(const exprt &value)
127 {
129  optionalt<mp_integer> maybe_integer_value = numeric_cast<mp_integer>(value);
130  INVARIANT(maybe_integer_value.has_value(), "Input has to have a value");
131  return maybe_integer_value.value();
132 }
133 
134 static inline constant_interval_exprt
136 {
137  mp_integer integer_value = force_value_from_expr(value);
138  if(!bvint_value_is_min(value.type(), integer_value))
140  min_exprt(value.type()), from_integer(integer_value - 1, value.type()));
141  else
142  return constant_interval_exprt::bottom(value.type());
143 }
144 
145 static inline constant_interval_exprt
147 {
148  mp_integer integer_value = force_value_from_expr(value);
149  if(!bvint_value_is_max(value.type(), integer_value))
151  from_integer(integer_value + 1, value.type()), max_exprt(value.type()));
152  else
153  return constant_interval_exprt::bottom(value.type());
154 }
155 
156 static inline bool represents_interval(exprt e)
157 {
158  e = look_through_casts(e);
159  return (e.id() == ID_constant_interval || e.id() == ID_constant);
160 }
161 
163 {
164  e = look_through_casts(e);
165  if(e.id() == ID_constant_interval)
166  {
167  return to_constant_interval_expr(e);
168  }
169  else if(e.id() == ID_constant)
170  {
171  return constant_interval_exprt(e, e);
172  }
173  else
174  {
175  // not directly representable, so just return TOP
176  return constant_interval_exprt(e.type());
177  }
178 }
179 
180 static inline irep_idt invert_relation(const irep_idt &relation)
181 {
182  PRECONDITION(
183  relation == ID_le || relation == ID_lt || relation == ID_ge ||
184  relation == ID_gt || relation == ID_equal);
185  if(relation == ID_le)
186  return ID_ge;
187  if(relation == ID_ge)
188  return ID_le;
189  if(relation == ID_lt)
190  return ID_gt;
191  if(relation == ID_gt)
192  return ID_lt;
193  return relation;
194 }
195 
202 {
203  PRECONDITION(e.operands().size() == 2);
204  const auto &relation = e.id();
205  const auto &binary_e = to_binary_expr(e);
206  const auto &lhs = binary_e.lhs();
207  const auto &rhs = binary_e.rhs();
208  PRECONDITION(
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);
213  PRECONDITION(lhs.id() != rhs.id());
214 
215  const auto the_constant_part_of_the_relation =
216  (rhs.id() == ID_symbol ? lhs : rhs);
217  const auto maybe_inverted_relation =
218  (rhs.id() == ID_symbol ? invert_relation(relation) : relation);
219 
220  if(maybe_inverted_relation == ID_le)
221  return interval_from_x_le_value(the_constant_part_of_the_relation);
222  if(maybe_inverted_relation == ID_lt)
223  return interval_from_x_lt_value(the_constant_part_of_the_relation);
224  if(maybe_inverted_relation == ID_ge)
225  return interval_from_x_ge_value(the_constant_part_of_the_relation);
226  if(maybe_inverted_relation == ID_gt)
227  return interval_from_x_gt_value(the_constant_part_of_the_relation);
228  INVARIANT(
229  maybe_inverted_relation == ID_equal, "We excluded other cases above");
231  the_constant_part_of_the_relation, the_constant_part_of_the_relation);
232 }
233 
235  : abstract_value_objectt(t), interval(t)
236 {
237 }
238 
240  const typet &t,
241  bool tp,
242  bool bttm)
243  : abstract_value_objectt(t, tp, bttm), interval(t)
244 {
245 }
246 
248 {
249  if(e.is_top())
250  return true;
251 
252  if(e.get_lower().is_false() && e.get_upper().is_true())
253  return true;
254  if(
255  e.type().id() == ID_c_bool && e.get_lower().is_zero() &&
256  e.get_upper().is_one())
257  return true;
258 
259  return false;
260 }
261 
263  const constant_interval_exprt &e)
264  : abstract_value_objectt(e.type(), new_interval_is_top(e), e.is_bottom()),
265  interval(e)
266 {
267 }
268 
270  const exprt &lower,
271  const exprt &upper)
273 {
274 }
275 
277  const exprt &e,
278  const abstract_environmentt &environment,
279  const namespacet &ns)
282  ? make_interval_expr(e)
283  : (e.operands().size() == 2 ? interval_from_relation(e)
284  : constant_interval_exprt(e.type())))
285 {
286 }
287 
289 {
290  // Attempt to reduce this interval to a constant expression
292  {
293  // Interval is the equivalent of a constant, so reduce it to a constant
295  }
297 #if 0
298  if(!is_top() && !is_bottom())
299  {
300  return this->interval;
301  }
302  else
303  {
305  }
306 #endif
307 }
308 
310 {
312 }
313 
315 {
316  return std::hash<std::string>{}(interval.pretty());
317 }
318 
320  const abstract_object_pointert &other) const
321 {
322  auto cast_other =
323  std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
324  return cast_other && interval == cast_other->interval;
325 }
326 
328  std::ostream &out,
329  const ai_baset &ai,
330  const namespacet &ns) const
331 {
332  if(!is_top() && !is_bottom())
333  {
334  std::string lower_string;
335  std::string upper_string;
336 
337  if(interval.get_lower().id() == ID_min)
338  {
339  lower_string = "-INF";
340  }
341  else
342  {
343  INVARIANT(
344  interval.get_lower().id() == ID_constant,
345  "We only support constant limits");
346  lower_string =
348  }
349 
350  if(interval.get_upper().id() == ID_max)
351  {
352  upper_string = "+INF";
353  }
354  else
355  {
356  INVARIANT(
357  interval.get_upper().id() == ID_constant,
358  "We only support constant limits");
359  upper_string =
361  }
362 
363  out << "[" << lower_string << ", " << upper_string << "]";
364  }
365  else
366  {
367  abstract_objectt::output(out, ai, ns);
368  }
369 }
370 
372  const constant_interval_exprt &lhs,
373  const constant_interval_exprt &rhs)
374 {
375  auto widened = widened_ranget(lhs, rhs);
376 
377  // new interval ...
378  auto new_interval = constant_interval_exprt(
379  widened.widened_lower_bound, widened.widened_upper_bound);
380  return interval_abstract_valuet::make_interval(new_interval);
381 }
382 
384  const abstract_value_pointert &other,
385  const widen_modet &widen_mode) const
386 {
387  if(other->is_bottom())
388  return shared_from_this();
389 
390  auto other_interval = other->to_interval();
391 
392  if(is_bottom())
393  return make_interval(other_interval);
394 
395  if(interval.contains(other_interval))
396  return shared_from_this();
397 
398  if(widen_mode == widen_modet::could_widen)
399  return widening_merge(interval, other_interval);
400 
401  auto lower_bound = constant_interval_exprt::get_min(
402  interval.get_lower(), other_interval.get_lower());
403  auto upper_bound = constant_interval_exprt::get_max(
404  interval.get_upper(), other_interval.get_upper());
405 
406  return make_interval(lower_bound, upper_bound);
407 }
408 
410  const abstract_value_pointert &other) const
411 {
412  auto other_interval = other->to_interval();
413 
414  if(other_interval.contains(interval))
415  return shared_from_this();
416 
417  if(interval.contains(other_interval))
418  return make_interval(other_interval);
419 
420  auto lower_bound = constant_interval_exprt::get_max(
421  interval.get_lower(), other_interval.get_lower());
422  auto upper_bound = constant_interval_exprt::get_min(
423  interval.get_upper(), other_interval.get_upper());
424 
425  // if the interval is valid, we have a meet!
426  if(constant_interval_exprt::less_than_or_equal(lower_bound, upper_bound))
427  return make_interval(constant_interval_exprt(lower_bound, upper_bound));
428 
429  return make_interval(interval.type(), false, true);
430 }
431 
434 {
435  if(is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
436  return make_empty_index_range();
437  if(interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
438  return make_empty_index_range();
439 
441 }
442 
445 {
446  return make_single_value_range(shared_from_this());
447 }
448 
450  const exprt &lower,
451  const exprt &upper) const
452 {
453  auto lower_bound =
455  auto upper_bound =
457 
458  if(constant_interval_exprt::greater_than(lower_bound, upper_bound))
459  return as_value(mutable_clone());
460 
461  auto constrained_interval = constant_interval_exprt(lower_bound, upper_bound);
462  return as_value(
463  make_interval(constant_interval_exprt(lower_bound, upper_bound)));
464 }
465 
467 {
469  return equal_exprt(name, interval.get_lower());
470 
471  auto lower_bound = binary_relation_exprt(interval.get_lower(), ID_le, name);
472  auto upper_bound = binary_relation_exprt(name, ID_le, interval.get_upper());
473 
474  return and_exprt(lower_bound, upper_bound);
475 }
476 
478  abstract_object_statisticst &statistics,
479  abstract_object_visitedt &visited,
480  const abstract_environmentt &env,
481  const namespacet &ns) const
482 {
483  abstract_objectt::get_statistics(statistics, visited, env, ns);
486  {
488  }
489  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
490 }
widen_modet
widen_modet
Definition: abstract_environment.h:33
interval_abstract_valuet::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: interval_abstract_value.cpp:433
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
interval_index_ranget::index
exprt index
Definition: interval_abstract_value.cpp:64
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:69
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:155
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
index_range_implementationt
Definition: abstract_value_object.h:29
abstract_objectt::output
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
Definition: abstract_object.cpp:190
interval_abstract_valuet::output
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
Definition: interval_abstract_value.cpp:327
arith_tools.h
integer_bitvector_typet::smallest
mp_integer smallest() const
Return the smallest value that can be represented using this type.
Definition: bitvector_types.cpp:33
widen_modet::no
@ no
typet
The type of an expression, extends irept.
Definition: type.h:28
interval_index_ranget::advance_to_next
bool advance_to_next() override
Definition: interval_abstract_value.cpp:44
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
constant_interval_exprt::get_max
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:47
constant_interval_exprt::is_bottom
static bool is_bottom(const constant_interval_exprt &a)
Definition: interval.cpp:1811
max_exprt
+∞ upper bound for intervals
Definition: interval.h:18
constant_interval_exprt::contains
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1423
interval_abstract_valuet::meet_with_value
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
Meet another interval abstract object with this one.
Definition: interval_abstract_value.cpp:409
invariant.h
widened_ranget
Definition: widened_range.h:18
and_exprt
Boolean AND.
Definition: std_expr.h:1920
interval_abstract_valuet
Definition: interval_abstract_value.h:22
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
abstract_environmentt
Definition: abstract_environment.h:41
exprt
Base class for all expressions.
Definition: expr.h:54
widened_range.h
min_exprt
-∞ upper bound for intervals
Definition: interval.h:31
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:310
bvint_value_is_max
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
Definition: interval_abstract_value.cpp:87
interval_abstract_valuet::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: interval_abstract_value.cpp:288
make_interval_index_range
static index_range_implementation_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
Definition: interval_abstract_value.cpp:70
equal_exprt
Equality.
Definition: std_expr.h:1225
interval_from_relation
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
Definition: interval_abstract_value.cpp:201
interval_abstract_valuet::set_top_internal
void set_top_internal() override
Definition: interval_abstract_value.cpp:309
interval_index_ranget::interval
const constant_interval_exprt & interval
Definition: interval_abstract_value.cpp:63
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:48
constant_interval_exprt::greater_than
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:398
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
constant_interval_exprt::is_int
bool is_int() const
Definition: interval.cpp:1064
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:131
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
interval_from_x_le_value
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
Definition: interval_abstract_value.cpp:115
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
interval_abstract_valuet::internal_hash
size_t internal_hash() const override
Definition: interval_abstract_value.cpp:314
make_empty_index_range
index_range_implementation_ptrt make_empty_index_range()
Definition: abstract_value_object.cpp:76
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
make_unique.h
force_value_from_expr
static mp_integer force_value_from_expr(const exprt &value)
Definition: interval_abstract_value.cpp:126
interval_from_x_gt_value
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
Definition: interval_abstract_value.cpp:146
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
abstract_value_objectt
Definition: abstract_value_object.h:241
interval_index_ranget::ns
const namespacet & ns
Definition: interval_abstract_value.cpp:67
constant_interval_exprt::is_single_value_interval
bool is_single_value_interval() const
Definition: interval.cpp:1861
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
bitvector_types.h
Pre-defined bitvector types.
look_through_casts
static exprt look_through_casts(exprt e)
Definition: interval_abstract_value.cpp:77
interval_index_ranget::next
exprt next
Definition: interval_abstract_value.cpp:65
interval_index_ranget::next_element
static exprt next_element(const exprt &cur, const namespacet &ns)
Definition: interval_abstract_value.cpp:58
abstract_environment.h
An abstract version of a program environment.
constant_interval_exprt::bottom
constant_interval_exprt bottom() const
Definition: interval.cpp:1057
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:170
abstract_value_objectt::as_value
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
Definition: abstract_value_object.cpp:697
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2659
interval_abstract_valuet::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: interval_abstract_value.cpp:477
irept::id
const irep_idt & id() const
Definition: irep.h:407
make_interval_expr
static constant_interval_exprt make_interval_expr(exprt e)
Definition: interval_abstract_value.cpp:162
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:70
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
new_interval_is_top
bool new_interval_is_top(const constant_interval_exprt &e)
Definition: interval_abstract_value.cpp:247
interval_abstract_valuet::constrain
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
Definition: interval_abstract_value.cpp:449
interval_index_ranget
Definition: interval_abstract_value.cpp:27
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
interval_index_ranget::reset
index_range_implementation_ptrt reset() const override
Definition: interval_abstract_value.cpp:52
interval_abstract_valuet::merge_with_value
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.
Definition: interval_abstract_value.cpp:383
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
simplify_expr.h
interval_from_x_ge_value
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
Definition: interval_abstract_value.cpp:121
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
represents_interval
static bool represents_interval(exprt e)
Definition: interval_abstract_value.cpp:156
constant_interval_exprt::is_top
static bool is_top(const constant_interval_exprt &a)
Definition: interval.cpp:1806
interval_abstract_valuet::make_interval
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
Definition: interval_abstract_value.h:37
make_single_value_range
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
Definition: abstract_value_object.cpp:115
interval_index_ranget::upper
exprt upper
Definition: interval_abstract_value.cpp:66
interval_abstract_valuet::internal_equality
bool internal_equality(const abstract_object_pointert &other) const override
Definition: interval_abstract_value.cpp:319
abstract_object_statistics.h
Statistics gathering for the variable senstivity domain.
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
bvint_value_is_min
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
Definition: interval_abstract_value.cpp:101
interval_abstract_value.h
An interval to represent a set of possible values.
interval_abstract_valuet::to_predicate_internal
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
Definition: interval_abstract_value.cpp:466
to_constant_interval_expr
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
Definition: interval.h:458
interval_from_x_lt_value
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
Definition: interval_abstract_value.cpp:135
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
abstract_object_statisticst::objects_memory_usage
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
Definition: abstract_object_statistics.h:28
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
interval_abstract_valuet::interval_abstract_valuet
interval_abstract_valuet(const typet &t)
Definition: interval_abstract_value.cpp:234
abstract_object_statisticst::number_of_single_value_intervals
std::size_t number_of_single_value_intervals
Definition: abstract_object_statistics.h:21
constant_interval_exprt::less_than_or_equal
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:404
constant_interval_exprt::get_lower
const exprt & get_lower() const
Definition: interval.cpp:29
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: bitvector_types.cpp:38
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
interval_index_ranget::current
const exprt & current() const override
Definition: interval_abstract_value.cpp:40
constant_interval_exprt::get_upper
const exprt & get_upper() const
Definition: interval.cpp:34
constant_interval_exprt::get_min
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
exprt::operands
operandst & operands()
Definition: expr.h:92
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:26
abstract_value_objectt::abstract_value_pointert
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
Definition: abstract_value_object.h:302
interval_abstract_valuet::interval
constant_interval_exprt interval
Definition: interval_abstract_value.h:100
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:160
interval_abstract_valuet::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: interval_abstract_value.cpp:444
widening_merge
abstract_object_pointert widening_merge(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval_abstract_value.cpp:371
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
memory_sizet::from_bytes
static memory_sizet from_bytes(std::size_t bytes)
Definition: memory_units.cpp:38
interval_index_ranget::interval_index_ranget
interval_index_ranget(const constant_interval_exprt &interval_, const namespacet &n)
Definition: interval_abstract_value.cpp:29
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:428
invert_relation
static irep_idt invert_relation(const irep_idt &relation)
Definition: interval_abstract_value.cpp:180
abstract_object_statisticst::number_of_interval_abstract_objects
std::size_t number_of_interval_abstract_objects
Definition: abstract_object_statistics.h:20
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786