cprover
|
Public Member Functions | |
value_set_evaluator (const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n) | |
abstract_object_pointert | operator() () const |
Private Member Functions | |
abstract_object_pointert | transform () const |
abstract_object_sett | evaluate_each_combination (const std::vector< value_ranget > &value_ranges) const |
Evaluate expression for every combination of values in value_ranges . More... | |
void | evaluate_combination (abstract_object_sett &results, const std::vector< value_ranget > &value_ranges, std::vector< abstract_object_pointert > &combination) const |
exprt | rewrite_expression (const std::vector< abstract_object_pointert > &ops) const |
std::vector< value_ranget > | operands_as_ranges () const |
Static Private Member Functions | |
static bool | is_constant_value (const abstract_object_pointert &v) |
static abstract_object_sett | unwrap_and_extract_values (const abstract_object_sett &values) |
static abstract_object_pointert | maybe_extract_single_value (const abstract_object_pointert &maybe_singleton) |
static abstract_object_pointert | resolve_values (const abstract_object_sett &new_values) |
static abstract_object_pointert | make_interval (const abstract_object_sett &values) |
static abstract_object_pointert | make_value_set (const abstract_object_sett &values) |
static abstract_object_pointert | evaluate_conditional (const std::vector< value_ranget > &ops) |
Private Attributes | |
const exprt & | expression |
const std::vector< abstract_object_pointert > & | operands |
const abstract_environmentt & | environment |
const namespacet & | ns |
Definition at line 492 of file abstract_value_object.cpp.
|
inline |
Definition at line 495 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 535 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 655 of file abstract_value_object.cpp.
|
inlineprivate |
Evaluate expression for every combination of values in value_ranges
.
<{1,2},{1},{1,2,3}> -> eval(1,1,1), eval(1,1,2), eval(1,1,3), eval(2,1,1), eval(2,1,2), eval(2,1,3).
Definition at line 527 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 575 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 640 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 646 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 610 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 581 of file abstract_value_object.cpp.
|
inline |
Definition at line 505 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 627 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 559 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 511 of file abstract_value_object.cpp.
|
inlinestaticprivate |
Definition at line 597 of file abstract_value_object.cpp.
|
private |
Definition at line 682 of file abstract_value_object.cpp.
|
private |
Definition at line 680 of file abstract_value_object.cpp.
|
private |
Definition at line 683 of file abstract_value_object.cpp.
|
private |
Definition at line 681 of file abstract_value_object.cpp.