1/*******************************************************************\
3Module: API to expression classes for floating-point arithmetic
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
16 // The 32 bits are an arbitrary choice;
17 // e.g., float_utilst consumes other widths as well.
18 // The type is signed to match the signature of fesetround.
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A constant literal expression.
Fixed-width bit-vector with two's complement interpretation.
constant_exprt floatbv_rounding_mode(unsigned rm)
returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendati...
API to expression classes for floating-point arithmetic.