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 192 of file float_bv.cpp.
|
staticprivate |
Definition at line 1391 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 515 of file float_bv.cpp.
|
staticprivate |
takes an unbiased float, and applies the bias
Definition at line 1357 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 412 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 1005 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 734 of file float_bv.cpp.
|
staticprivate |
Definition at line 250 of file float_bv.cpp.
|
staticprivate |
Definition at line 259 of file float_bv.cpp.
|
staticprivate |
Definition at line 268 of file float_bv.cpp.
|
staticprivate |
rounding decision for fraction using sticky bit
Definition at line 1126 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 300 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 324 of file float_bv.cpp.
|
staticprivate |
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 923 of file float_bv.cpp.
|
staticprivate |
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 933 of file float_bv.cpp.
|
staticprivate |
Definition at line 186 of file float_bv.cpp.
|
static |
Definition at line 212 of file float_bv.cpp.
Definition at line 234 of file float_bv.cpp.
|
static |
Definition at line 915 of file float_bv.cpp.
|
static |
Definition at line 906 of file float_bv.cpp.
|
static |
Definition at line 942 of file float_bv.cpp.
|
static |
Definition at line 486 of file float_bv.cpp.
|
staticprivate |
Limits the shift distance.
Definition at line 661 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 685 of file float_bv.cpp.
|
static |
Definition at line 202 of file float_bv.cpp.
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition at line 951 of file float_bv.cpp.
Definition at line 19 of file float_bv.h.
|
staticprivate |
Definition at line 1444 of file float_bv.cpp.
|
static |
Definition at line 823 of file float_bv.cpp.
|
staticprivate |
Definition at line 1291 of file float_bv.cpp.
|
staticprivate |
Definition at line 1184 of file float_bv.cpp.
|
private |
Definition at line 1083 of file float_bv.cpp.
Definition at line 293 of file float_bv.cpp.
|
staticprivate |
Definition at line 1475 of file float_bv.cpp.
|
staticprivate |
Definition at line 1401 of file float_bv.cpp.
|
staticprivate |
Subtracts the exponents.
Definition at line 496 of file float_bv.cpp.
|
static |
Definition at line 364 of file float_bv.cpp.
|
static |
Definition at line 346 of file float_bv.cpp.
|
static |
Definition at line 355 of file float_bv.cpp.
|
staticprivate |
Definition at line 1411 of file float_bv.cpp.