cprover
|
#include <float_bv.h>
Public Member Functions | |
void | get (const exprt &rm) |
rounding_mode_bitst (const exprt &rm) | |
Public Attributes | |
exprt | round_to_even |
exprt | round_to_zero |
exprt | round_to_plus_inf |
exprt | round_to_minus_inf |
Definition at line 117 of file float_bv.h.
|
inlineexplicit |
Definition at line 127 of file float_bv.h.
References float_bvt::add_bias(), float_bvt::denormalization_shift(), float_bvt::limit_distance(), float_bvt::normalization_shift(), and float_bvt::sub_bias().
void float_bvt::rounding_mode_bitst::get | ( | const exprt & | rm | ) |
Definition at line 195 of file float_bv.cpp.
References from_integer(), ieee_floatt::ROUND_TO_EVEN, ieee_floatt::ROUND_TO_MINUS_INF, ieee_floatt::ROUND_TO_PLUS_INF, ieee_floatt::ROUND_TO_ZERO, and exprt::type().
exprt float_bvt::rounding_mode_bitst::round_to_even |
Definition at line 121 of file float_bv.h.
Referenced by float_bvt::fraction_rounding_decision(), and float_bvt::round_exponent().
exprt float_bvt::rounding_mode_bitst::round_to_minus_inf |
Definition at line 124 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::fraction_rounding_decision(), and float_bvt::round_exponent().
exprt float_bvt::rounding_mode_bitst::round_to_plus_inf |
Definition at line 123 of file float_bv.h.
Referenced by float_bvt::fraction_rounding_decision(), and float_bvt::round_exponent().
exprt float_bvt::rounding_mode_bitst::round_to_zero |
Definition at line 122 of file float_bv.h.
Referenced by float_bvt::fraction_rounding_decision().