CBMC
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 407 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: