cprover
Loading...
Searching...
No Matches
abstract_environment.cpp File Reference
Include dependency graph for abstract_environment.cpp:

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 &)

Functions

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_pointerteval_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 exprt &expr)
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)

Variables

static auto assume_functions
static auto inverse_operations
static auto symmetric_operations

Typedef Documentation

◆ assume_function

typedef exprt( * assume_function) (abstract_environmentt &, const exprt &, const namespacet &)

Definition at line 31 of file abstract_environment.cpp.

Function Documentation

◆ as_value()

abstract_value_pointert as_value ( const abstract_object_pointert & obj)
static

Definition at line 561 of file abstract_environment.cpp.

◆ assume_and()

exprt assume_and ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 633 of file abstract_environment.cpp.

◆ assume_eq()

exprt assume_eq ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 736 of file abstract_environment.cpp.

◆ assume_eq_unbounded()

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.

◆ assume_greater_than()

exprt assume_greater_than ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 861 of file abstract_environment.cpp.

◆ assume_less_than()

exprt assume_less_than ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 815 of file abstract_environment.cpp.

◆ assume_less_than_unbounded()

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.

◆ assume_not()

exprt assume_not ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 618 of file abstract_environment.cpp.

◆ assume_noteq()

exprt assume_noteq ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 761 of file abstract_environment.cpp.

◆ assume_or()

exprt assume_or ( abstract_environmentt & env,
const exprt & expr,
const namespacet & ns )
static

Definition at line 652 of file abstract_environment.cpp.

◆ count_globals()

std::size_t count_globals ( const namespacet & ns)
static

Definition at line 519 of file abstract_environment.cpp.

◆ eval_operands()

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.

◆ eval_operands_as_values()

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.

◆ invert_expr()

exprt invert_expr ( const exprt & expr)
static

Definition at line 590 of file abstract_environment.cpp.

◆ invert_result()

exprt invert_result ( const exprt & result)
static

Definition at line 580 of file abstract_environment.cpp.

◆ is_access_expr()

bool is_access_expr ( const exprt & expr)
static

Definition at line 80 of file abstract_environment.cpp.

◆ is_dynamic_allocation()

bool is_dynamic_allocation ( const exprt & expr)
static

Definition at line 95 of file abstract_environment.cpp.

◆ is_object_creation()

bool is_object_creation ( const irep_idt & id)
static

Definition at line 89 of file abstract_environment.cpp.

◆ is_ptr_comparison()

bool is_ptr_comparison ( const exprt & expr)

Definition at line 70 of file abstract_environment.cpp.

◆ is_ptr_diff()

bool is_ptr_diff ( const exprt & expr)

Definition at line 63 of file abstract_environment.cpp.

◆ is_value()

bool is_value ( const abstract_object_pointert & obj)
static

Definition at line 567 of file abstract_environment.cpp.

◆ prune_assign()

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.

Variable Documentation

◆ assume_functions

auto assume_functions
static
Initial value:
=
std::map<irep_idt, assume_function>{{ID_not, assume_not},
{ID_and, assume_and},
{ID_or, assume_or},
{ID_equal, assume_eq},
{ID_notequal, assume_noteq},
{ID_le, assume_less_than},
{ID_lt, assume_less_than},
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)

Definition at line 289 of file abstract_environment.cpp.

◆ inverse_operations

auto inverse_operations
static
Initial value:
=
std::map<irep_idt, irep_idt>{{ID_equal, ID_notequal},
{ID_notequal, ID_equal},
{ID_le, ID_gt},
{ID_lt, ID_ge},
{ID_ge, ID_lt},
{ID_gt, ID_le}}

Definition at line 572 of file abstract_environment.cpp.

◆ symmetric_operations

auto symmetric_operations
static
Initial value:
=
std::map<irep_idt, irep_idt>{{ID_ge, ID_le}, {ID_gt, ID_lt}}

Definition at line 858 of file abstract_environment.cpp.