cprover
Loading...
Searching...
No Matches
widened_range.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: helper for extending intervals during widening merges
4
5 Author: Jez Higgins
6
7\*******************************************************************/
8
9#include "widened_range.h"
10#include <util/simplify_expr.h>
11
12static bool has_underflowed(const exprt &value)
13{
15 value, from_integer(0, value.type()));
16}
17static bool has_overflowed(const exprt &value, const exprt &initial_value)
18{
19 return constant_interval_exprt::less_than(value, initial_value);
20}
21
36
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
tvt greater_than(const constant_interval_exprt &o) const
Definition interval.cpp:398
static bool contains_extreme(const exprt expr)
tvt less_than(const constant_interval_exprt &o) const
Definition interval.cpp:377
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
+∞ upper bound for intervals
Definition interval.h:18
-∞ upper bound for intervals
Definition interval.h:31
Binary minus.
Definition std_expr.h:973
The plus expression Associativity is not specified.
Definition std_expr.h:914
const exprt upper_bound
exprt widen_lower_bound() const
const bool is_upper_widened
namespacet ns_
const exprt lower_bound
exprt widen_upper_bound() const
const bool is_lower_widened
exprt simplify_expr(exprt src, const namespacet &ns)
static bool has_overflowed(const exprt &value, const exprt &initial_value)
static bool has_underflowed(const exprt &value)