Loading...

Searching...

No Matches

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

interval_evaluator Class Reference

+ Collaboration diagram for interval_evaluator:

Public Member Functions

interval_evaluator (const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)

abstract_object_pointert operator() () const

Private Types

using interval_abstract_value_pointert = sharing_ptrt< const interval_abstract_valuet >

Private Member Functions

abstract_object_pointert transform () const

std::vector< constant_interval_exprt > operands_as_intervals () const

abstract_object_pointert evaluate_conditional (const std::vector< constant_interval_exprt > &interval_operands) const

abstract_object_pointert evaluate_unary_expr (const std::vector< constant_interval_exprt > &interval_operands) const

interval_abstract_value_pointert make_interval (const exprt &expr) const

Private Attributes

const exprt & expression

const std::vector< abstract_object_pointert > & operands

const abstract_environmentt & environment

const namespacet & ns

Detailed Description

Definition at line 387 of file abstract_value_object.cpp.

Member Typedef Documentation

◆ interval_abstract_value_pointert

using interval_evaluator::interval_abstract_value_pointert = sharing_ptrt<const interval_abstract_valuet>

private

Definition at line 406 of file abstract_value_object.cpp.

Constructor & Destructor Documentation

◆ interval_evaluator()

interval_evaluator::interval_evaluator ( const exprt & e,

const std::vector< abstract_object_pointert > & ops,

const abstract_environmentt & env,

const namespacet & n

)

inline

Definition at line 390 of file abstract_value_object.cpp.

Member Function Documentation

◆ evaluate_conditional()

abstract_object_pointert interval_evaluator::evaluate_conditional ( const std::vector< constant_interval_exprt > & interval_operands ) const

inlineprivate

Definition at line 476 of file abstract_value_object.cpp.

◆ evaluate_unary_expr()

abstract_object_pointert interval_evaluator::evaluate_unary_expr ( const std::vector< constant_interval_exprt > & interval_operands ) const

inlineprivate

Definition at line 500 of file abstract_value_object.cpp.

◆ make_interval()

interval_abstract_value_pointert interval_evaluator::make_interval ( const exprt & expr ) const

inlineprivate

Definition at line 527 of file abstract_value_object.cpp.

◆ operands_as_intervals()

std::vector< constant_interval_exprt > interval_evaluator::operands_as_intervals ( ) const

inlineprivate

Definition at line 446 of file abstract_value_object.cpp.

◆ operator()()

abstract_object_pointert interval_evaluator::operator() ( ) const

inline

Definition at line 400 of file abstract_value_object.cpp.

◆ transform()

abstract_object_pointert interval_evaluator::transform ( ) const

inlineprivate

Definition at line 409 of file abstract_value_object.cpp.

Member Data Documentation

◆ environment

const abstract_environmentt& interval_evaluator::environment

private

Definition at line 534 of file abstract_value_object.cpp.

◆ expression

const exprt& interval_evaluator::expression

private

Definition at line 532 of file abstract_value_object.cpp.

◆ ns

const namespacet& interval_evaluator::ns

private

Definition at line 535 of file abstract_value_object.cpp.

◆ operands

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

private

Definition at line 533 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