cprover
|
Public Member Functions | |
unpacked_floatt () | |
Public Attributes | |
exprt | sign |
exprt | infinity |
exprt | zero |
exprt | NaN |
exprt | fraction |
exprt | exponent |
Definition at line 133 of file float_bv.h.
|
inline |
Definition at line 138 of file float_bv.h.
exprt float_bvt::unpacked_floatt::exponent |
Definition at line 136 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::bias(), float_bvt::conversion(), float_bvt::div(), float_bvt::from_signed_integer(), float_bvt::from_unsigned_integer(), float_bvt::mul(), float_bvt::pack(), float_bvt::round_exponent(), float_bvt::round_fraction(), float_bvt::rounder(), float_bvt::subtract_exponents(), float_bvt::to_integer(), and float_bvt::unpack().
exprt float_bvt::unpacked_floatt::fraction |
Definition at line 136 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::bias(), float_bvt::conversion(), float_bvt::div(), float_bvt::from_signed_integer(), float_bvt::from_unsigned_integer(), float_bvt::mul(), float_bvt::pack(), float_bvt::round_exponent(), float_bvt::round_fraction(), float_bvt::rounder(), float_bvt::to_integer(), and float_bvt::unpack().
exprt float_bvt::unpacked_floatt::infinity |
Definition at line 135 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::bias(), float_bvt::conversion(), float_bvt::div(), float_bvt::mul(), float_bvt::pack(), float_bvt::round_exponent(), float_bvt::rounder(), and float_bvt::unpack().
exprt float_bvt::unpacked_floatt::NaN |
Definition at line 135 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::bias(), float_bvt::conversion(), float_bvt::div(), float_bvt::mul(), float_bvt::pack(), float_bvt::rounder(), and float_bvt::unpack().
exprt float_bvt::unpacked_floatt::sign |
Definition at line 135 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::bias(), float_bvt::conversion(), float_bvt::div(), float_bvt::from_signed_integer(), float_bvt::from_unsigned_integer(), float_bvt::mul(), float_bvt::pack(), float_bvt::round_exponent(), float_bvt::round_fraction(), float_bvt::rounder(), float_bvt::to_integer(), and float_bvt::unpack().
exprt float_bvt::unpacked_floatt::zero |
Definition at line 135 of file float_bv.h.
Referenced by float_bvt::add_sub(), float_bvt::div(), float_bvt::mul(), and float_bvt::unpack().