constants_evaluator Class Reference

Collaboration diagram for constants_evaluator:

Public Member Functions
	constants_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	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
abstract_object_pointert	top (const typet &type) const
bool	rounding_mode_is_not_set () const

Static Private Member Functions
static std::vector< abstract_object_pointert >	reeval_operands (const exprt::operandst &ops, const abstract_environmentt &env, const namespacet &ns)

Private Attributes
const exprt &	expression
std::vector< abstract_object_pointert >	operands
const abstract_environmentt &	environment
const namespacet &	ns

Static Private Attributes
static const symbol_exprt	rounding_mode_symbol
static const rounding_modes	all_rounding_modes

Detailed Description

Definition at line 223 of file abstract_value_object.cpp.

Member Typedef Documentation

rounding_modes

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

private

Definition at line 362 of file abstract_value_object.cpp.

Constructor & Destructor Documentation

constants_evaluator()

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

inline

Definition at line 226 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 318 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 304 of file abstract_value_object.cpp.

operator()()

abstract_object_pointert constants_evaluator::operator() ( void  ) const

inline

Definition at line 235 of file abstract_value_object.cpp.

reeval_operands()

static std::vector<abstract_object_pointert> constants_evaluator::reeval_operands ( const exprt::operandst &  ops, const abstract_environmentt &  env, const namespacet &  ns  )

inlinestaticprivate

Definition at line 329 of file abstract_value_object.cpp.

rounding_mode_is_not_set()

bool constants_evaluator::rounding_mode_is_not_set ( ) const

inlineprivate

Definition at line 348 of file abstract_value_object.cpp.

top()

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

inlineprivate

Definition at line 343 of file abstract_value_object.cpp.

transform()

abstract_object_pointert constants_evaluator::transform ( ) const

inlineprivate

Definition at line 246 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 274 of file abstract_value_object.cpp.

Member Data Documentation

all_rounding_modes

const constants_evaluator::rounding_modes constants_evaluator::all_rounding_modes

staticprivate

Initial value:

{ieee_floatt::ROUND_TO_EVEN,
                                          ieee_floatt::ROUND_TO_ZERO,
                                          ieee_floatt::ROUND_TO_MINUS_INF,
                                          ieee_floatt::ROUND_TO_PLUS_INF}

Definition at line 363 of file abstract_value_object.cpp.

environment

const abstract_environmentt& constants_evaluator::environment

private

Definition at line 357 of file abstract_value_object.cpp.

expression

const exprt& constants_evaluator::expression

private

Definition at line 355 of file abstract_value_object.cpp.

ns

const namespacet& constants_evaluator::ns

private

Definition at line 358 of file abstract_value_object.cpp.

operands

std::vector<abstract_object_pointert> constants_evaluator::operands

mutableprivate

Definition at line 356 of file abstract_value_object.cpp.

rounding_mode_symbol

const symbol_exprt constants_evaluator::rounding_mode_symbol

staticprivate

Initial value:

=
  symbol_exprt( "__CPROVER_"  "rounding_mode", signedbv_typet(32))

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