cprover
constants_evaluator Class Reference
+ Collaboration diagram for constants_evaluator:

Public Member Functions

 constants_evaluator (const exprt &e, const abstract_environmentt &env, const namespacet &n)
 
abstract_object_pointert operator() () const
 

Private Types

using rounding_modes = std::vector< ieee_floatt::rounding_modet >
 

Private Member Functions

abstract_object_pointert transform () const
 
abstract_object_pointert try_transform_expr_with_all_rounding_modes () const
 
abstract_environmentt environment_with_rounding_mode (ieee_floatt::rounding_modet rm) const
 
exprt adjust_expression_for_rounding_mode () const
 
exprt eval_constant (const exprt &op) const
 
abstract_object_pointert top (const typet &type) const
 
bool rounding_mode_is_not_set () const
 

Private Attributes

const exprtexpression
 
const abstract_environmenttenvironment
 
const namespacetns
 

Static Private Attributes

static const symbol_exprt rounding_mode_symbol
 
static const rounding_modes all_rounding_modes
 

Detailed Description

Definition at line 188 of file abstract_value_object.cpp.

Member Typedef Documentation

◆ rounding_modes

Definition at line 304 of file abstract_value_object.cpp.

Constructor & Destructor Documentation

◆ constants_evaluator()

constants_evaluator::constants_evaluator ( const exprt e,
const abstract_environmentt env,
const namespacet n 
)
inline

Definition at line 191 of file abstract_value_object.cpp.

Member Function Documentation

◆ adjust_expression_for_rounding_mode()

exprt constants_evaluator::adjust_expression_for_rounding_mode ( ) const
inlineprivate

Definition at line 275 of file abstract_value_object.cpp.

◆ environment_with_rounding_mode()

abstract_environmentt constants_evaluator::environment_with_rounding_mode ( ieee_floatt::rounding_modet  rm) const
inlineprivate

Definition at line 261 of file abstract_value_object.cpp.

◆ eval_constant()

exprt constants_evaluator::eval_constant ( const exprt op) const
inlineprivate

Definition at line 282 of file abstract_value_object.cpp.

◆ operator()()

abstract_object_pointert constants_evaluator::operator() ( void  ) const
inline

Definition at line 199 of file abstract_value_object.cpp.

◆ rounding_mode_is_not_set()

bool constants_evaluator::rounding_mode_is_not_set ( ) const
inlineprivate

Definition at line 292 of file abstract_value_object.cpp.

◆ top()

abstract_object_pointert constants_evaluator::top ( const typet type) const
inlineprivate

Definition at line 287 of file abstract_value_object.cpp.

◆ transform()

abstract_object_pointert constants_evaluator::transform ( ) const
inlineprivate

Definition at line 210 of file abstract_value_object.cpp.

◆ try_transform_expr_with_all_rounding_modes()

abstract_object_pointert constants_evaluator::try_transform_expr_with_all_rounding_modes ( ) const
inlineprivate

Definition at line 240 of file abstract_value_object.cpp.

Member Data Documentation

◆ all_rounding_modes

◆ environment

const abstract_environmentt& constants_evaluator::environment
private

Definition at line 299 of file abstract_value_object.cpp.

◆ expression

const exprt& constants_evaluator::expression
private

Definition at line 298 of file abstract_value_object.cpp.

◆ ns

const namespacet& constants_evaluator::ns
private

Definition at line 300 of file abstract_value_object.cpp.

◆ rounding_mode_symbol

const symbol_exprt constants_evaluator::rounding_mode_symbol
staticprivate
Initial value:
=

Definition at line 302 of file abstract_value_object.cpp.


The documentation for this class was generated from the following file:
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:127
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128