Loading...

Searching...

No Matches

Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | List of all members

value_set_evaluator Class Reference

+ Collaboration diagram for value_set_evaluator:

[フレーム]

[legend]

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.

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

Detailed Description

Definition at line 550 of file abstract_value_object.cpp.

Constructor & Destructor Documentation

◆ value_set_evaluator()

value_set_evaluator::value_set_evaluator ( const exprt & e,

const std::vector< abstract_object_pointert > & ops,

const abstract_environmentt & env,

const namespacet & n

)

inline

Definition at line 553 of file abstract_value_object.cpp.

Member Function Documentation

◆ evaluate_combination()

void value_set_evaluator::evaluate_combination ( abstract_object_sett & results,

const std::vector< value_ranget > & value_ranges,

std::vector< abstract_object_pointert > & combination

) const

inlineprivate

Definition at line 593 of file abstract_value_object.cpp.

◆ evaluate_conditional()

static abstract_object_pointert value_set_evaluator::evaluate_conditional ( const std::vector< value_ranget > & ops )

inlinestaticprivate

Definition at line 655 of file abstract_value_object.cpp.

◆ evaluate_each_combination()

abstract_object_sett value_set_evaluator::evaluate_each_combination ( const std::vector< value_ranget > & value_ranges ) const

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 585 of file abstract_value_object.cpp.

◆ is_constant_value()

static bool value_set_evaluator::is_constant_value ( const abstract_object_pointert & v )

inlinestaticprivate

Definition at line 633 of file abstract_value_object.cpp.

◆ operands_as_ranges()

std::vector< value_ranget > value_set_evaluator::operands_as_ranges ( ) const

inlineprivate

Definition at line 639 of file abstract_value_object.cpp.

◆ operator()()

abstract_object_pointert value_set_evaluator::operator() ( ) const

inline

Definition at line 563 of file abstract_value_object.cpp.

◆ rewrite_expression()

exprt value_set_evaluator::rewrite_expression ( const std::vector< abstract_object_pointert > & ops ) const

inlineprivate

Definition at line 617 of file abstract_value_object.cpp.

◆ transform()

abstract_object_pointert value_set_evaluator::transform ( ) const

inlineprivate

Definition at line 569 of file abstract_value_object.cpp.

Member Data Documentation

◆ environment

const abstract_environmentt& value_set_evaluator::environment

private

Definition at line 682 of file abstract_value_object.cpp.

◆ expression

const exprt& value_set_evaluator::expression

private

Definition at line 680 of file abstract_value_object.cpp.

◆ ns

const namespacet& value_set_evaluator::ns

private

Definition at line 683 of file abstract_value_object.cpp.

◆ operands

const std::vector<abstract_object_pointert>& value_set_evaluator::operands

private

Definition at line 681 of file abstract_value_object.cpp.

The documentation for this class was generated from the following file:

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_value_object.cpp