cprover
|
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 109 of file float_bv.h.
|
inlineexplicit |
Definition at line 118 of file float_bv.h.
void float_bvt::rounding_mode_bitst::get | ( | const exprt & | rm | ) |
Definition at line 193 of file float_bv.cpp.
References from_integer(), round_to_even, ieee_floatt::ROUND_TO_EVEN, round_to_minus_inf, ieee_floatt::ROUND_TO_MINUS_INF, round_to_plus_inf, ieee_floatt::ROUND_TO_PLUS_INF, round_to_zero, ieee_floatt::ROUND_TO_ZERO, and exprt::type().
exprt float_bvt::rounding_mode_bitst::round_to_even |
Definition at line 112 of file float_bv.h.
Referenced by float_bvt::fraction_rounding_decision(), get(), and float_bvt::round_exponent().
exprt float_bvt::rounding_mode_bitst::round_to_minus_inf |
Definition at line 115 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::fraction_rounding_decision(), get(), and float_bvt::round_exponent().
exprt float_bvt::rounding_mode_bitst::round_to_plus_inf |
Definition at line 114 of file float_bv.h.
Referenced by float_bvt::fraction_rounding_decision(), get(), and float_bvt::round_exponent().
exprt float_bvt::rounding_mode_bitst::round_to_zero |
Definition at line 113 of file float_bv.h.
Referenced by float_bvt::fraction_rounding_decision(), and get().