floatbv_expr.cpp File Reference

#include "floatbv_expr.h"
#include "arith_tools.h"
#include "bitvector_types.h"

Include dependency graph for floatbv_expr.cpp:

Go to the source code of this file.

Functions
constant_exprt	floatbv_rounding_mode (unsigned rm)
	returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendation in C11 5.2.4.2.2 More...

Function Documentation

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 recommendation in C11 5.2.4.2.2

Definition at line 14 of file floatbv_expr.cpp.