CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_environment.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Typedefs | Functions | Variables

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

static 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()

static exprt invert_expr ( const exprt & expr )

static

Definition at line 590 of file abstract_environment.cpp.

◆ invert_result()

static exprt invert_result ( const exprt & result )

static

Definition at line 580 of file abstract_environment.cpp.

◆ is_access_expr()

static bool is_access_expr ( const exprt & expr )

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

◆ is_object_creation()

static 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},

{ID_ge, assume_greater_than},

{ID_gt, assume_greater_than}}

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

Definition abstract_environment.cpp:618

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

Definition abstract_environment.cpp:736

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

Definition abstract_environment.cpp:761

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

Definition abstract_environment.cpp:652

assume_less_than

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

Definition abstract_environment.cpp:815

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

Definition abstract_environment.cpp:633

assume_greater_than

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

Definition abstract_environment.cpp:861

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

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.