Go to the source code of this file.
|
static exprt | assume_not (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static exprt | assume_or (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static exprt | assume_and (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static exprt | assume_eq (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static exprt | assume_noteq (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static exprt | assume_less_than (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static exprt | assume_greater_than (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
static abstract_value_pointert | as_value (const abstract_object_pointert &obj) |
|
static bool | is_value (const abstract_object_pointert &obj) |
|
std::vector< abstract_object_pointert > | eval_operands (const exprt &expr, const abstract_environmentt &env, const namespacet &ns) |
|
bool | is_ptr_diff (const exprt &expr) |
|
bool | is_ptr_comparison (const exprt &expr) |
|
static bool | is_access_expr (const irep_idt &id) |
|
static bool | is_object_creation (const irep_idt &id) |
|
static bool | is_dynamic_allocation (const exprt &expr) |
|
static std::size_t | count_globals (const namespacet &ns) |
|
static exprt | invert_result (const exprt &result) |
|
static exprt | invert_expr (const exprt &expr) |
|
void | prune_assign (abstract_environmentt &env, const abstract_object_pointert &previous, const exprt &destination, abstract_object_pointert obj, const namespacet &ns) |
|
left_and_right_valuest | eval_operands_as_values (abstract_environmentt &env, const exprt &expr, const namespacet &ns) |
|
exprt | assume_eq_unbounded (abstract_environmentt &env, const left_and_right_valuest &operands, const namespacet &ns) |
|
exprt | assume_less_than_unbounded (abstract_environmentt &env, const left_and_right_valuest &operands, const namespacet &ns) |
|
◆ assume_function
◆ as_value()
◆ assume_and()
◆ assume_eq()
◆ assume_eq_unbounded()
◆ assume_greater_than()
◆ assume_less_than()
◆ assume_less_than_unbounded()
◆ assume_not()
◆ assume_noteq()
◆ assume_or()
◆ count_globals()
◆ eval_operands()
◆ eval_operands_as_values()
◆ invert_expr()
◆ invert_result()
◆ is_access_expr()
◆ is_dynamic_allocation()
◆ is_object_creation()
◆ is_ptr_comparison()
◆ is_ptr_diff()
◆ is_value()
◆ prune_assign()
◆ assume_functions
Initial value:=
static exprt assume_not(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_eq(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_noteq(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_or(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_less_than(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_and(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_greater_than(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition at line 284 of file abstract_environment.cpp.
◆ inverse_operations
◆ symmetric_operations
auto symmetric_operations |
|
static |