cprover
Loading...
Searching...
No Matches
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
14
constant_exprt
floatbv_rounding_mode
(
unsigned
rm)
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.
19
return ::from_integer(rm,
signedbv_typet
(32));
20
}
arith_tools.h
bitvector_types.h
Pre-defined bitvector types.
constant_exprt
A constant literal expression.
Definition
std_expr.h:3122
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition
bitvector_types.h:222
floatbv_rounding_mode
constant_exprt floatbv_rounding_mode(unsigned rm)
returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendati...
Definition
floatbv_expr.cpp:14
floatbv_expr.h
API to expression classes for floating-point arithmetic.
util
floatbv_expr.cpp
Generated by
1.14.0