cprover
|
#include <ieee_float.h>
Public Member Functions | |
mp_integer | bias () const |
ieee_float_spect (const floatbv_typet &type) | |
void | from_type (const floatbv_typet &type) |
ieee_float_spect () | |
ieee_float_spect (std::size_t _f, std::size_t _e) | |
std::size_t | width () const |
mp_integer | max_exponent () const |
mp_integer | max_fraction () const |
class floatbv_typet | to_type () const |
bool | operator== (const ieee_float_spect &other) const |
bool | operator!= (const ieee_float_spect &other) const |
Static Public Member Functions | |
static ieee_float_spect | half_precision () |
static ieee_float_spect | single_precision () |
static ieee_float_spect | double_precision () |
static ieee_float_spect | quadruple_precision () |
static ieee_float_spect | x86_80 () |
static ieee_float_spect | x86_96 () |
Public Attributes | |
std::size_t | f |
std::size_t | e |
bool | x86_extended |
Definition at line 25 of file ieee_float.h.
|
inlineexplicit |
Definition at line 38 of file ieee_float.h.
References from_type().
|
inline |
Definition at line 45 of file ieee_float.h.
Referenced by double_precision(), half_precision(), quadruple_precision(), and single_precision().
|
inline |
Definition at line 49 of file ieee_float.h.
mp_integer ieee_float_spect::bias | ( | ) | const |
Definition at line 21 of file ieee_float.cpp.
Referenced by float_bvt::add_bias(), float_utilst::add_bias(), ieee_floatt::align(), float_bvt::denormalization_shift(), float_utilst::denormalization_shift(), get_exponent(), ieee_floatt::pack(), float_bvt::round_exponent(), float_utilst::round_exponent(), float_bvt::sub_bias(), float_utilst::sub_bias(), float_bvt::unpack(), float_utilst::unpack(), and ieee_floatt::unpack().
|
inlinestatic |
Definition at line 80 of file ieee_float.h.
References ieee_float_spect().
Referenced by constant_float(), java_bytecode_convert_methodt::convert_const(), c_typecheck_baset::do_special_functions(), double_type(), gcc_float64_type(), gcc_float64x_type(), java_double_type(), long_double_type(), and java_bytecode_parsert::rconstant_pool().
void ieee_float_spect::from_type | ( | const floatbv_typet & | type | ) |
Definition at line 46 of file ieee_float.cpp.
References e, f, irept::get_bool(), floatbv_typet::get_f(), bitvector_typet::get_width(), width(), and x86_extended.
Referenced by ieee_float_spect().
|
inlinestatic |
Definition at line 67 of file ieee_float.h.
References ieee_float_spect().
Referenced by gcc_float16_type().
mp_integer ieee_float_spect::max_exponent | ( | ) | const |
Definition at line 36 of file ieee_float.cpp.
Referenced by ieee_floatt::align(), ieee_floatt::pack(), float_bvt::round_exponent(), float_utilst::round_exponent(), and ieee_floatt::unpack().
mp_integer ieee_float_spect::max_fraction | ( | ) | const |
Definition at line 41 of file ieee_float.cpp.
|
inline |
Definition at line 113 of file ieee_float.h.
|
inline |
Definition at line 108 of file ieee_float.h.
References e, f, and x86_extended.
|
inlinestatic |
Definition at line 86 of file ieee_float.h.
References ieee_float_spect().
Referenced by gcc_float128_type(), gcc_float128x_type(), c_typecastt::implicit_typecast_arithmetic(), and long_double_type().
|
inlinestatic |
Definition at line 74 of file ieee_float.h.
References ieee_float_spect().
Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation(), constant_float(), java_bytecode_convert_methodt::convert_const(), c_typecheck_baset::do_special_functions(), float_type(), gcc_float32_type(), gcc_float32x_type(), java_float_type(), and java_bytecode_parsert::rconstant_pool().
floatbv_typet ieee_float_spect::to_type | ( | ) | const |
Definition at line 26 of file ieee_float.cpp.
References f, irept::set(), floatbv_typet::set_f(), bitvector_typet::set_width(), width(), and x86_extended.
Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation(), convert_float_literal(), double_type(), float_type(), floatbv_of_int_expr(), gcc_float128_type(), gcc_float128x_type(), gcc_float16_type(), gcc_float32_type(), gcc_float32x_type(), gcc_float64_type(), gcc_float64x_type(), c_typecastt::implicit_typecast_arithmetic(), java_double_type(), java_float_type(), long_double_type(), float_bvt::pack(), and ieee_floatt::to_expr().
|
inline |
Definition at line 54 of file ieee_float.h.
References e, f, and x86_extended.
Referenced by float_bvt::abs(), bv_refinementt::check_SAT(), float_utilst::conversion(), smt2_convt::convert_constant(), convert_float_literal(), smt2_convt::convert_typecast(), float_utilst::fraction_all_zeros(), ieee_floatt::from_double(), ieee_floatt::from_float(), from_type(), float_bvt::negation(), float_utilst::pack(), float_bvt::relation(), ieee_floatt::to_expr(), float_utilst::to_integer(), to_type(), smt2_convt::type2id(), and float_utilst::unpack().
|
inlinestatic |
Definition at line 92 of file ieee_float.h.
References x86_extended.
|
inlinestatic |
Definition at line 100 of file ieee_float.h.
References x86_extended.
std::size_t ieee_float_spect::e |
Definition at line 30 of file ieee_float.h.
Referenced by float_bvt::add_bias(), float_utilst::add_bias(), float_bvt::add_sub(), float_utilst::add_sub(), bias(), float_utilst::build_constant(), float_bvt::conversion(), float_utilst::conversion(), float_bvt::denormalization_shift(), float_utilst::denormalization_shift(), float_bvt::div(), float_utilst::exponent_all_ones(), float_utilst::exponent_all_zeros(), ieee_floatt::from_base10(), ieee_floatt::from_double(), ieee_floatt::from_float(), from_type(), get_exponent(), float_utilst::get_exponent(), float_bvt::get_exponent(), ieee_floatt::is_double(), ieee_floatt::is_float(), ieee_floatt::make_fltmax(), max_exponent(), float_bvt::mul(), operator==(), float_bvt::pack(), float_utilst::pack(), ieee_floatt::pack(), float_bvt::round_exponent(), float_utilst::round_exponent(), float_bvt::rounder(), float_utilst::rounder(), float_bvt::sub_bias(), float_utilst::sub_bias(), float_bvt::to_integer(), float_bvt::unpack(), float_utilst::unpack(), ieee_floatt::unpack(), and width().
std::size_t ieee_float_spect::f |
Definition at line 30 of file ieee_float.h.
Referenced by float_bvt::add_sub(), float_utilst::add_sub(), ieee_floatt::align(), float_bvt::bias(), float_utilst::bias(), ieee_floatt::build(), float_utilst::build_constant(), ieee_floatt::change_spec(), float_bvt::conversion(), float_utilst::conversion(), float_bvt::denormalization_shift(), float_utilst::denormalization_shift(), float_bvt::div(), float_utilst::div(), float_utilst::exponent_all_ones(), float_utilst::exponent_all_zeros(), ieee_floatt::extract_base10(), ieee_floatt::extract_base2(), float_utilst::fraction_all_zeros(), ieee_floatt::from_base10(), ieee_floatt::from_double(), ieee_floatt::from_float(), ieee_floatt::from_integer(), from_type(), get_exponent(), float_utilst::get_exponent(), float_bvt::get_exponent(), get_fraction(), float_utilst::get_fraction(), float_bvt::get_fraction(), get_significand(), ieee_floatt::is_double(), ieee_floatt::is_float(), ieee_floatt::is_normal(), ieee_floatt::make_fltmax(), ieee_floatt::make_fltmin(), max_fraction(), float_bvt::mul(), ieee_floatt::operator*=(), ieee_floatt::operator/=(), operator==(), float_bvt::pack(), float_utilst::pack(), ieee_floatt::pack(), float_bvt::round_fraction(), float_utilst::round_fraction(), float_bvt::rounder(), float_utilst::rounder(), float_bvt::to_integer(), ieee_floatt::to_integer(), to_type(), smt2_convt::type2id(), float_bvt::unpack(), ieee_floatt::unpack(), and width().
bool ieee_float_spect::x86_extended |
Definition at line 34 of file ieee_float.h.
Referenced by from_type(), operator==(), to_type(), width(), x86_80(), and x86_96().