CBMC
|
#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 561 of file abstract_environment.cpp.
|
static |
Definition at line 633 of file abstract_environment.cpp.
|
static |
Definition at line 736 of file abstract_environment.cpp.
exprt assume_eq_unbounded | ( | abstract_environmentt & | env, |
const left_and_right_valuest & | operands, | ||
const namespacet & | ns | ||
) |
Definition at line 714 of file abstract_environment.cpp.
|
static |
Definition at line 861 of file abstract_environment.cpp.
|
static |
Definition at line 815 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 784 of file abstract_environment.cpp.
|
static |
Definition at line 618 of file abstract_environment.cpp.
|
static |
Definition at line 761 of file abstract_environment.cpp.
|
static |
Definition at line 652 of file abstract_environment.cpp.
|
static |
Definition at line 519 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 547 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 696 of file abstract_environment.cpp.
Definition at line 590 of file abstract_environment.cpp.
Definition at line 580 of file abstract_environment.cpp.
Definition at line 80 of file abstract_environment.cpp.
Definition at line 95 of file abstract_environment.cpp.
Definition at line 89 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 567 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 604 of file abstract_environment.cpp.
|
static |
Definition at line 289 of file abstract_environment.cpp.
|
static |
Definition at line 572 of file abstract_environment.cpp.