CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Classes | Public Types | Public Member Functions | Static Public Member Functions | Private Member Functions | Static Private Member Functions | List of all members
float_bvt Class Reference

#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
 

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.
 
static exprt get_fraction (const exprt &, const ieee_float_spect &)
 Gets the fraction without hidden bit in a floating-point bit-vector src.
 
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
 
static void denormalization_shift (exprt &fraction, exprt &exponent, const ieee_float_spect &)
 make sure exponent is not too small; the exponent is unbiased
 
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.
 
static biased_floatt bias (const unbiased_floatt &, const ieee_float_spect &)
 takes an unbiased float, and applies the bias
 
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
 
static exprt subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2)
 Subtracts the exponents.
 
static exprt sticky_right_shift (const exprt &op, const exprt &dist, exprt &sticky)
 

Detailed Description

Definition at line 16 of file float_bv.h.

Member Enumeration Documentation

◆ relt

enum class float_bvt::relt
strong
Enumerator
LT 
LE 
EQ 
GT 
GE 

Definition at line 83 of file float_bv.h.

Member Function Documentation

◆ abs()

exprt float_bvt::abs ( const exprt &  op,
const ieee_float_spect &  spec 
)
static

Definition at line 191 of file float_bv.cpp.

◆ add_bias()

exprt float_bvt::add_bias ( const exprt &  exponent,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 1390 of file float_bv.cpp.

◆ add_sub()

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 517 of file float_bv.cpp.

◆ bias()

float_bvt::biased_floatt float_bvt::bias ( const unbiased_floatt &  src,
const ieee_float_spect &  spec 
)
staticprivate

takes an unbiased float, and applies the bias

Definition at line 1358 of file float_bv.cpp.

◆ conversion()

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 414 of file float_bv.cpp.

◆ convert()

exprt float_bvt::convert ( const exprt &  expr) const

Definition at line 19 of file float_bv.cpp.

◆ denormalization_shift()

void float_bvt::denormalization_shift ( exprt &  fraction,
exprt &  exponent,
const ieee_float_spect &  spec 
)
staticprivate

make sure exponent is not too small; the exponent is unbiased

Definition at line 1001 of file float_bv.cpp.

◆ div()

exprt float_bvt::div ( const exprt &  src1,
const exprt &  src2,
const exprt &  rm,
const ieee_float_spect &  spec 
) const

Definition at line 737 of file float_bv.cpp.

◆ exponent_all_ones()

exprt float_bvt::exponent_all_ones ( const exprt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 249 of file float_bv.cpp.

◆ exponent_all_zeros()

exprt float_bvt::exponent_all_zeros ( const exprt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 258 of file float_bv.cpp.

◆ fraction_all_zeros()

exprt float_bvt::fraction_all_zeros ( const exprt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 267 of file float_bv.cpp.

◆ fraction_rounding_decision()

exprt float_bvt::fraction_rounding_decision ( const std::size_t  dest_bits,
const exprt  sign,
const exprt &  fraction,
const rounding_mode_bitst &  rounding_mode_bits 
)
staticprivate

rounding decision for fraction using sticky bit

Definition at line 1122 of file float_bv.cpp.

◆ from_signed_integer()

exprt float_bvt::from_signed_integer ( const exprt &  src,
const exprt &  rm,
const ieee_float_spect &  spec 
) const

Definition at line 302 of file float_bv.cpp.

◆ from_unsigned_integer()

exprt float_bvt::from_unsigned_integer ( const exprt &  src,
const exprt &  rm,
const ieee_float_spect &  spec 
) const

Definition at line 326 of file float_bv.cpp.

◆ get_exponent()

exprt float_bvt::get_exponent ( const exprt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Gets the unbiased exponent in a floating-point bit-vector.

Definition at line 926 of file float_bv.cpp.

◆ get_fraction()

exprt float_bvt::get_fraction ( const exprt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Gets the fraction without hidden bit in a floating-point bit-vector src.

Definition at line 934 of file float_bv.cpp.

◆ get_spec()

ieee_float_spect float_bvt::get_spec ( const exprt &  expr)
staticprivate

Definition at line 185 of file float_bv.cpp.

◆ is_equal()

exprt float_bvt::is_equal ( const exprt &  src0,
const exprt &  src1,
const ieee_float_spect &  spec 
)
static

Definition at line 211 of file float_bv.cpp.

◆ is_zero()

exprt float_bvt::is_zero ( const exprt &  src)
static

Definition at line 233 of file float_bv.cpp.

◆ isfinite()

exprt float_bvt::isfinite ( const exprt &  src,
const ieee_float_spect &  spec 
)
static

Definition at line 918 of file float_bv.cpp.

◆ isinf()

exprt float_bvt::isinf ( const exprt &  src,
const ieee_float_spect &  spec 
)
static

Definition at line 909 of file float_bv.cpp.

◆ isnan()

exprt float_bvt::isnan ( const exprt &  src,
const ieee_float_spect &  spec 
)
static

Definition at line 941 of file float_bv.cpp.

◆ isnormal()

exprt float_bvt::isnormal ( const exprt &  src,
const ieee_float_spect &  spec 
)
static

Definition at line 488 of file float_bv.cpp.

◆ limit_distance()

exprt float_bvt::limit_distance ( const exprt &  dist,
mp_integer  limit 
)
staticprivate

Limits the shift distance.

Definition at line 663 of file float_bv.cpp.

◆ mul()

exprt float_bvt::mul ( const exprt &  src1,
const exprt &  src2,
const exprt &  rm,
const ieee_float_spect &  spec 
) const

Definition at line 686 of file float_bv.cpp.

◆ negation()

exprt float_bvt::negation ( const exprt &  op,
const ieee_float_spect &  spec 
)
static

Definition at line 201 of file float_bv.cpp.

◆ normalization_shift()

void float_bvt::normalization_shift ( exprt &  fraction,
exprt &  exponent 
)
staticprivate

normalize fraction/exponent pair returns 'zero' if fraction is zero

Definition at line 950 of file float_bv.cpp.

◆ operator()()

exprt float_bvt::operator() ( const exprt &  src) const
inline

Definition at line 19 of file float_bv.h.

◆ pack()

exprt float_bvt::pack ( const biased_floatt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 1443 of file float_bv.cpp.

◆ relation()

exprt float_bvt::relation ( const exprt &  src1,
relt  rel,
const exprt &  src2,
const ieee_float_spect &  spec 
)
static

Definition at line 826 of file float_bv.cpp.

◆ round_exponent()

void float_bvt::round_exponent ( unbiased_floatt &  result,
const rounding_mode_bitst &  rounding_mode_bits,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 1292 of file float_bv.cpp.

◆ round_fraction()

void float_bvt::round_fraction ( unbiased_floatt &  result,
const rounding_mode_bitst &  rounding_mode_bits,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 1186 of file float_bv.cpp.

◆ rounder()

exprt float_bvt::rounder ( const unbiased_floatt &  src,
const exprt &  rm,
const ieee_float_spect &  spec 
) const
private

Definition at line 1079 of file float_bv.cpp.

◆ sign_bit()

exprt float_bvt::sign_bit ( const exprt &  op)
staticprivate

Definition at line 295 of file float_bv.cpp.

◆ sticky_right_shift()

exprt float_bvt::sticky_right_shift ( const exprt &  op,
const exprt &  dist,
exprt &  sticky 
)
staticprivate

Definition at line 1474 of file float_bv.cpp.

◆ sub_bias()

exprt float_bvt::sub_bias ( const exprt &  exponent,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 1400 of file float_bv.cpp.

◆ subtract_exponents()

exprt float_bvt::subtract_exponents ( const unbiased_floatt &  src1,
const unbiased_floatt &  src2 
)
staticprivate

Subtracts the exponents.

Definition at line 498 of file float_bv.cpp.

◆ to_integer()

exprt float_bvt::to_integer ( const exprt &  src,
std::size_t  dest_width,
bool  is_signed,
const exprt &  rm,
const ieee_float_spect &  spec 
)
static

Definition at line 366 of file float_bv.cpp.

◆ to_signed_integer()

exprt float_bvt::to_signed_integer ( const exprt &  src,
std::size_t  dest_width,
const exprt &  rm,
const ieee_float_spect &  spec 
)
static

Definition at line 348 of file float_bv.cpp.

◆ to_unsigned_integer()

exprt float_bvt::to_unsigned_integer ( const exprt &  src,
std::size_t  dest_width,
const exprt &  rm,
const ieee_float_spect &  spec 
)
static

Definition at line 357 of file float_bv.cpp.

◆ unpack()

float_bvt::unbiased_floatt float_bvt::unpack ( const exprt &  src,
const ieee_float_spect &  spec 
)
staticprivate

Definition at line 1410 of file float_bv.cpp.

The documentation for this class was generated from the following files: