cprover
|
#include <ostream>
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/simplify_expr.h>
#include "abstract_environment.h"
#include "abstract_object_statistics.h"
#include "interval_abstract_value.h"
#include "widened_range.h"
Go to the source code of this file.
Classes | |
class | interval_index_ranget |
|
inlinestatic |
Definition at line 79 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 93 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 118 of file interval_abstract_value.cpp.
|
inlinestatic |
Builds an interval representing all values satisfying the input expression.
The expression is expected to be a comparison between an integer constant and a variable (symbol)
e | the relation expression that should be satisfied |
Definition at line 194 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 113 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 138 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 107 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 127 of file interval_abstract_value.cpp.
Definition at line 173 of file interval_abstract_value.cpp.
|
inlinestatic |
Definition at line 154 of file interval_abstract_value.cpp.
|
static |
Definition at line 71 of file interval_abstract_value.cpp.
bool new_interval_is_top | ( | const constant_interval_exprt & | e | ) |
Definition at line 240 of file interval_abstract_value.cpp.
Definition at line 148 of file interval_abstract_value.cpp.
abstract_object_pointert widening_merge | ( | const constant_interval_exprt & | lhs, |
const constant_interval_exprt & | rhs | ||
) |
Definition at line 364 of file interval_abstract_value.cpp.