cprover
|
#include <float_bv.h>
Classes | |
struct | biased_floatt |
struct | rounding_mode_bitst |
struct | unbiased_floatt |
struct | unpacked_floatt |
Public Types | |
enum | relt { relt::LT, relt::LE, relt::EQ, relt::GT, relt::GE } |
Public Member Functions | |
exprt | operator() (const exprt &src) const |
exprt | convert (const exprt &) const |
exprt | add_sub (bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const |
exprt | mul (const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const |
exprt | div (const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const |
exprt | from_unsigned_integer (const exprt &, const exprt &rm, const ieee_float_spect &) const |
exprt | from_signed_integer (const exprt &, const exprt &rm, const ieee_float_spect &) const |
exprt | conversion (const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const |
Static Public Member Functions | |
static exprt | negation (const exprt &, const ieee_float_spect &) |
static exprt | abs (const exprt &, const ieee_float_spect &) |
static exprt | is_equal (const exprt &, const exprt &, const ieee_float_spect &) |
static exprt | is_zero (const exprt &) |
static exprt | isnan (const exprt &, const ieee_float_spect &) |
static exprt | isinf (const exprt &, const ieee_float_spect &) |
static exprt | isnormal (const exprt &, const ieee_float_spect &) |
static exprt | isfinite (const exprt &, const ieee_float_spect &) |
static exprt | to_signed_integer (const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &) |
static exprt | to_unsigned_integer (const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &) |
static exprt | to_integer (const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &) |
static exprt | relation (const exprt &, relt rel, const exprt &, const ieee_float_spect &) |
Private Member Functions | |
exprt | rounder (const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const |
Static Private Member Functions | |
static ieee_float_spect | get_spec (const exprt &) |
static exprt | get_exponent (const exprt &, const ieee_float_spect &) |
Gets the unbiased exponent in a floating-point bit-vector. More... | |
static exprt | get_fraction (const exprt &, const ieee_float_spect &) |
Gets the fraction without hidden bit in a floating-point bit-vector src. More... | |
static exprt | sign_bit (const exprt &) |
static exprt | exponent_all_ones (const exprt &, const ieee_float_spect &) |
static exprt | exponent_all_zeros (const exprt &, const ieee_float_spect &) |
static exprt | fraction_all_zeros (const exprt &, const ieee_float_spect &) |
static void | normalization_shift (exprt &fraction, exprt &exponent) |
normalize fraction/exponent pair returns 'zero' if fraction is zero More... | |
static void | denormalization_shift (exprt &fraction, exprt &exponent, const ieee_float_spect &) |
make sure exponent is not too small; the exponent is unbiased More... | |
static exprt | add_bias (const exprt &exponent, const ieee_float_spect &) |
static exprt | sub_bias (const exprt &exponent, const ieee_float_spect &) |
static exprt | limit_distance (const exprt &dist, mp_integer limit) |
Limits the shift distance. More... | |
static biased_floatt | bias (const unbiased_floatt &, const ieee_float_spect &) |
takes an unbiased float, and applies the bias More... | |
static exprt | pack (const biased_floatt &, const ieee_float_spect &) |
static unbiased_floatt | unpack (const exprt &, const ieee_float_spect &) |
static void | round_fraction (unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &) |
static void | round_exponent (unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &) |
static exprt | fraction_rounding_decision (const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &) |
rounding decision for fraction using sticky bit More... | |
static exprt | subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2) |
Subtracts the exponents. More... | |
static exprt | sticky_right_shift (const exprt &op, const exprt &dist, exprt &sticky) |
Definition at line 18 of file float_bv.h.
|
strong |
Enumerator | |
---|---|
LT | |
LE | |
EQ | |
GT | |
GE |
Definition at line 85 of file float_bv.h.
|
static |
Definition at line 172 of file float_bv.cpp.
|
staticprivate |
Definition at line 1364 of file float_bv.cpp.
exprt float_bvt::add_sub | ( | bool | subtract, |
const exprt & | op0, | ||
const exprt & | op1, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) | const |
Definition at line 488 of file float_bv.cpp.
|
staticprivate |
takes an unbiased float, and applies the bias
Definition at line 1330 of file float_bv.cpp.
exprt float_bvt::conversion | ( | const exprt & | src, |
const exprt & | rm, | ||
const ieee_float_spect & | src_spec, | ||
const ieee_float_spect & | dest_spec | ||
) | const |
Definition at line 392 of file float_bv.cpp.
Definition at line 16 of file float_bv.cpp.
|
staticprivate |
make sure exponent is not too small; the exponent is unbiased
Definition at line 978 of file float_bv.cpp.
exprt float_bvt::div | ( | const exprt & | src1, |
const exprt & | src2, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) | const |
Definition at line 707 of file float_bv.cpp.
|
staticprivate |
Definition at line 230 of file float_bv.cpp.
|
staticprivate |
Definition at line 239 of file float_bv.cpp.
|
staticprivate |
Definition at line 248 of file float_bv.cpp.
|
staticprivate |
rounding decision for fraction using sticky bit
Definition at line 1099 of file float_bv.cpp.
exprt float_bvt::from_signed_integer | ( | const exprt & | src, |
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) | const |
Definition at line 280 of file float_bv.cpp.
exprt float_bvt::from_unsigned_integer | ( | const exprt & | src, |
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) | const |
Definition at line 304 of file float_bv.cpp.
|
staticprivate |
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 896 of file float_bv.cpp.
|
staticprivate |
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 906 of file float_bv.cpp.
|
staticprivate |
Definition at line 166 of file float_bv.cpp.
|
static |
Definition at line 192 of file float_bv.cpp.
Definition at line 214 of file float_bv.cpp.
|
static |
Definition at line 888 of file float_bv.cpp.
|
static |
Definition at line 879 of file float_bv.cpp.
|
static |
Definition at line 915 of file float_bv.cpp.
|
static |
Definition at line 459 of file float_bv.cpp.
|
staticprivate |
Limits the shift distance.
Definition at line 634 of file float_bv.cpp.
exprt float_bvt::mul | ( | const exprt & | src1, |
const exprt & | src2, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) | const |
Definition at line 658 of file float_bv.cpp.
|
static |
Definition at line 182 of file float_bv.cpp.
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition at line 924 of file float_bv.cpp.
Definition at line 21 of file float_bv.h.
|
staticprivate |
Definition at line 1417 of file float_bv.cpp.
|
static |
Definition at line 796 of file float_bv.cpp.
|
staticprivate |
Definition at line 1264 of file float_bv.cpp.
|
staticprivate |
Definition at line 1157 of file float_bv.cpp.
|
private |
Definition at line 1056 of file float_bv.cpp.
Definition at line 273 of file float_bv.cpp.
|
staticprivate |
Definition at line 1448 of file float_bv.cpp.
|
staticprivate |
Definition at line 1374 of file float_bv.cpp.
|
staticprivate |
Subtracts the exponents.
Definition at line 469 of file float_bv.cpp.
|
static |
Definition at line 344 of file float_bv.cpp.
|
static |
Definition at line 326 of file float_bv.cpp.
|
static |
Definition at line 335 of file float_bv.cpp.
|
staticprivate |
Definition at line 1384 of file float_bv.cpp.