|
CBMC
|
Collaboration diagram for float_bvt::rounding_mode_bitst:Public Member Functions | |
| void | get (const exprt &rm) |
| rounding_mode_bitst (const exprt &rm) | |
Public Attributes | |
| exprt | round_to_even |
| exprt | round_to_zero |
| exprt | round_to_plus_inf |
| exprt | round_to_minus_inf |
| exprt | round_to_away |
Definition at line 114 of file float_bv.h.
Definition at line 124 of file float_bv.h.
Definition at line 288 of file float_bv.cpp.
| exprt float_bvt::rounding_mode_bitst::round_to_away |
Definition at line 121 of file float_bv.h.
| exprt float_bvt::rounding_mode_bitst::round_to_even |
Definition at line 117 of file float_bv.h.
| exprt float_bvt::rounding_mode_bitst::round_to_minus_inf |
Definition at line 120 of file float_bv.h.
| exprt float_bvt::rounding_mode_bitst::round_to_plus_inf |
Definition at line 119 of file float_bv.h.
| exprt float_bvt::rounding_mode_bitst::round_to_zero |
Definition at line 118 of file float_bv.h.