abstract_environment.cpp File Reference

#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"

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

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 555 of file abstract_environment.cpp.

assume_and()

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

static

Definition at line 627 of file abstract_environment.cpp.

assume_eq()

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

static

Definition at line 730 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 708 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 855 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 809 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 778 of file abstract_environment.cpp.

assume_not()

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

static

Definition at line 612 of file abstract_environment.cpp.

assume_noteq()

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

static

Definition at line 755 of file abstract_environment.cpp.

assume_or()

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

static

Definition at line 646 of file abstract_environment.cpp.

count_globals()

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

static

Definition at line 513 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 541 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 690 of file abstract_environment.cpp.

invert_expr()

static exprt invert_expr ( const exprt &  expr )

static

Definition at line 584 of file abstract_environment.cpp.

invert_result()

static exprt invert_result ( const exprt &  result )

static

Definition at line 574 of file abstract_environment.cpp.

is_access_expr()

static bool is_access_expr ( const irep_idt &  id )

static

Definition at line 80 of file abstract_environment.cpp.

is_dynamic_allocation()

static bool is_dynamic_allocation ( const exprt &  expr )

static

Definition at line 91 of file abstract_environment.cpp.

is_object_creation()

static bool is_object_creation ( const irep_idt &  id )

static

Definition at line 85 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 561 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 598 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},
                                      {ID_ge, assume_greater_than},
                                      {ID_gt, assume_greater_than}}

Definition at line 283 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 566 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 852 of file abstract_environment.cpp.