CBMC
floatbv_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for floating-point arithmetic
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "floatbv_expr.h"
10 
11 #include "arith_tools.h"
12 #include "bitvector_types.h"
13 
15 {
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.
20 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Pre-defined bitvector types.
A constant literal expression.
Definition: std_expr.h:2987
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.