cprover
|
#include <util/expr_util.h>
#include <util/namespace.h>
#include <util/simplify_expr.h>
#include <util/simplify_utils.h>
#include <util/symbol_table.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <algorithm>
#include <map>
#include <ostream>
#include <stack>
#include "abstract_object_statistics.h"
#include "context_abstract_object.h"
#include "interval_abstract_value.h"
Go to the source code of this file.
Classes | |
struct | left_and_right_valuest |
Typedefs | |
typedef exprt(* | assume_function) (abstract_environmentt &, const exprt &, const namespacet &) |
Variables | |
static auto | assume_functions |
static auto | inverse_operations |
static auto | symmetric_operations |
typedef exprt( * assume_function) (abstract_environmentt &, const exprt &, const namespacet &) |
Definition at line 31 of file abstract_environment.cpp.
|
static |
Definition at line 558 of file abstract_environment.cpp.
|
static |
Definition at line 630 of file abstract_environment.cpp.
|
static |
Definition at line 733 of file abstract_environment.cpp.
exprt assume_eq_unbounded | ( | abstract_environmentt & | env, |
const left_and_right_valuest & | operands, | ||
const namespacet & | ns ) |
Definition at line 711 of file abstract_environment.cpp.
|
static |
Definition at line 858 of file abstract_environment.cpp.
|
static |
Definition at line 812 of file abstract_environment.cpp.
exprt assume_less_than_unbounded | ( | abstract_environmentt & | env, |
const left_and_right_valuest & | operands, | ||
const namespacet & | ns ) |
Definition at line 781 of file abstract_environment.cpp.
|
static |
Definition at line 615 of file abstract_environment.cpp.
|
static |
Definition at line 758 of file abstract_environment.cpp.
|
static |
Definition at line 649 of file abstract_environment.cpp.
|
static |
Definition at line 516 of file abstract_environment.cpp.
std::vector< abstract_object_pointert > eval_operands | ( | const exprt & | expr, |
const abstract_environmentt & | env, | ||
const namespacet & | ns ) |
Definition at line 544 of file abstract_environment.cpp.
left_and_right_valuest eval_operands_as_values | ( | abstract_environmentt & | env, |
const exprt & | expr, | ||
const namespacet & | ns ) |
Definition at line 693 of file abstract_environment.cpp.
Definition at line 587 of file abstract_environment.cpp.
Definition at line 577 of file abstract_environment.cpp.
Definition at line 80 of file abstract_environment.cpp.
Definition at line 91 of file abstract_environment.cpp.
Definition at line 85 of file abstract_environment.cpp.
Definition at line 70 of file abstract_environment.cpp.
Definition at line 63 of file abstract_environment.cpp.
|
static |
Definition at line 564 of file abstract_environment.cpp.
void prune_assign | ( | abstract_environmentt & | env, |
const abstract_object_pointert & | previous, | ||
const exprt & | destination, | ||
abstract_object_pointert | obj, | ||
const namespacet & | ns ) |
Definition at line 601 of file abstract_environment.cpp.
|
static |
Definition at line 286 of file abstract_environment.cpp.
|
static |
Definition at line 569 of file abstract_environment.cpp.