cprover
|
#include <float_bv.h>
Classes | |
struct | biased_floatt |
struct | rounding_mode_bitst |
struct | unbiased_floatt |
struct | unpacked_floatt |
Public Types | |
enum class | relt { LT , LE , EQ , GT , 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 |
Definition at line 16 of file float_bv.h.
|
strong |
Enumerator | |
---|---|
LT | |
LE | |
EQ | |
GT | |
GE |
Definition at line 83 of file float_bv.h.
|
static |
Definition at line 175 of file float_bv.cpp.
|
staticprivate |
Definition at line 1367 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 491 of file float_bv.cpp.
|
staticprivate |
takes an unbiased float, and applies the bias
Definition at line 1333 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 395 of file float_bv.cpp.
Definition at line 19 of file float_bv.cpp.
|
staticprivate |
make sure exponent is not too small; the exponent is unbiased
Definition at line 981 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 710 of file float_bv.cpp.
|
staticprivate |
Definition at line 233 of file float_bv.cpp.
|
staticprivate |
Definition at line 242 of file float_bv.cpp.
|
staticprivate |
Definition at line 251 of file float_bv.cpp.
|
staticprivate |
rounding decision for fraction using sticky bit
Definition at line 1102 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 283 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 307 of file float_bv.cpp.
|
staticprivate |
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 899 of file float_bv.cpp.
|
staticprivate |
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 909 of file float_bv.cpp.
|
staticprivate |
Definition at line 169 of file float_bv.cpp.
|
static |
Definition at line 195 of file float_bv.cpp.
Definition at line 217 of file float_bv.cpp.
|
static |
Definition at line 891 of file float_bv.cpp.
|
static |
Definition at line 882 of file float_bv.cpp.
|
static |
Definition at line 918 of file float_bv.cpp.
|
static |
Definition at line 462 of file float_bv.cpp.
|
staticprivate |
Limits the shift distance.
Definition at line 637 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 661 of file float_bv.cpp.
|
static |
Definition at line 185 of file float_bv.cpp.
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition at line 927 of file float_bv.cpp.
Definition at line 19 of file float_bv.h.
|
staticprivate |
Definition at line 1420 of file float_bv.cpp.
|
static |
Definition at line 799 of file float_bv.cpp.
|
staticprivate |
Definition at line 1267 of file float_bv.cpp.
|
staticprivate |
Definition at line 1160 of file float_bv.cpp.
|
private |
Definition at line 1059 of file float_bv.cpp.
Definition at line 276 of file float_bv.cpp.
|
staticprivate |
Definition at line 1451 of file float_bv.cpp.
|
staticprivate |
Definition at line 1377 of file float_bv.cpp.
|
staticprivate |
Subtracts the exponents.
Definition at line 472 of file float_bv.cpp.
|
static |
Definition at line 347 of file float_bv.cpp.
|
static |
Definition at line 329 of file float_bv.cpp.
|
static |
Definition at line 338 of file float_bv.cpp.
|
staticprivate |
Definition at line 1387 of file float_bv.cpp.