CBMC
|
API to expression classes for floating-point arithmetic. More...
#include "std_expr.h"
Go to the source code of this file.
Classes | |
class | floatbv_typecast_exprt |
Semantic type conversion from/to floating-point formats. More... | |
class | floatbv_round_to_integral_exprt |
Round a floating-point number to an integral value considering the given rounding mode. More... | |
class | isnan_exprt |
Evaluates to true if the operand is NaN. More... | |
class | isinf_exprt |
Evaluates to true if the operand is infinite. More... | |
class | isfinite_exprt |
Evaluates to true if the operand is finite. More... | |
class | isnormal_exprt |
Evaluates to true if the operand is a normal number. More... | |
class | ieee_float_equal_exprt |
IEEE-floating-point equality. More... | |
class | ieee_float_notequal_exprt |
IEEE floating-point disequality. More... | |
class | ieee_float_op_exprt |
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2). More... | |
class | floatbv_mod_exprt |
IEEE floating-point mod. More... | |
class | floatbv_rem_exprt |
IEEE floating-point rem. More... | |
API to expression classes for floating-point arithmetic.
Definition in file floatbv_expr.h.
|
inline |
Definition at line 122 of file floatbv_expr.h.
|
inline |
Definition at line 52 of file floatbv_expr.h.
|
inline |
Definition at line 340 of file floatbv_expr.h.
|
inline |
Definition at line 388 of file floatbv_expr.h.
|
inline |
Definition at line 471 of file floatbv_expr.h.
|
inline |
Definition at line 249 of file floatbv_expr.h.
|
inline |
Definition at line 205 of file floatbv_expr.h.
|
inline |
Definition at line 161 of file floatbv_expr.h.
|
inline |
Definition at line 293 of file floatbv_expr.h.
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.
|
inline |
Cast an exprt to a floatbv_mod_exprt.
expr must be known to be floatbv_mod_exprt.
expr | Source expression |
Definition at line 523 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_mod_exprt.
expr must be known to be floatbv_mod_exprt.
expr | Source expression |
Definition at line 531 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_rem_exprt.
expr must be known to be floatbv_rem_exprt.
expr | Source expression |
Definition at line 556 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_rem_exprt.
expr must be known to be floatbv_rem_exprt.
expr | Source expression |
Definition at line 564 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_round_to_integral_exprt.
expr must be known to be floatbv_round_to_integral_exprt.
expr | Source expression |
Definition at line 134 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_round_to_integral_exprt.
expr must be known to be floatbv_round_to_integral_exprt.
expr | Source expression |
Definition at line 143 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_typecast_exprt.
expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 68 of file floatbv_expr.h.
|
inline |
Cast an exprt to a floatbv_typecast_exprt.
expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 78 of file floatbv_expr.h.
|
inline |
Cast an exprt to an ieee_float_equal_exprt.
expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 356 of file floatbv_expr.h.
|
inline |
Cast an exprt to an ieee_float_equal_exprt.
expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 366 of file floatbv_expr.h.
|
inline |
Cast an exprt to an ieee_float_notequal_exprt.
expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 405 of file floatbv_expr.h.
|
inline |
Cast an exprt to an ieee_float_notequal_exprt.
expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 415 of file floatbv_expr.h.
|
inline |
Cast an exprt to an ieee_float_op_exprt.
expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 489 of file floatbv_expr.h.
|
inline |
Cast an exprt to an ieee_float_op_exprt.
expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 498 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isfinite_exprt.
expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 265 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isfinite_exprt.
expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 274 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isinf_exprt.
expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 221 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isinf_exprt.
expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 230 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isnan_exprt.
expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 177 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isnan_exprt.
expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 186 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isnormal_exprt.
expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 309 of file floatbv_expr.h.
|
inline |
Cast an exprt to a isnormal_exprt.
expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 318 of file floatbv_expr.h.
|
inline |
Definition at line 57 of file floatbv_expr.h.
|
inline |
Definition at line 345 of file floatbv_expr.h.
|
inline |
Definition at line 393 of file floatbv_expr.h.
|
inline |
Definition at line 477 of file floatbv_expr.h.
|
inline |
Definition at line 254 of file floatbv_expr.h.
|
inline |
Definition at line 210 of file floatbv_expr.h.
|
inline |
Definition at line 166 of file floatbv_expr.h.
|
inline |
Definition at line 298 of file floatbv_expr.h.