cprover
|
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 exprt & | expression |
const abstract_environmentt & | environment |
const namespacet & | ns |
Static Private Attributes | |
static const symbol_exprt | rounding_mode_symbol |
static const rounding_modes | all_rounding_modes |
Definition at line 188 of file abstract_value_object.cpp.
|
private |
Definition at line 304 of file abstract_value_object.cpp.
|
inline |
Definition at line 191 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 275 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 261 of file abstract_value_object.cpp.
Definition at line 282 of file abstract_value_object.cpp.
|
inline |
Definition at line 199 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 292 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 287 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 210 of file abstract_value_object.cpp.
|
inlineprivate |
Definition at line 240 of file abstract_value_object.cpp.
|
staticprivate |
Definition at line 305 of file abstract_value_object.cpp.
|
private |
Definition at line 299 of file abstract_value_object.cpp.
|
private |
Definition at line 298 of file abstract_value_object.cpp.
|
private |
Definition at line 300 of file abstract_value_object.cpp.
|
staticprivate |
Definition at line 302 of file abstract_value_object.cpp.