Float rounding mode (-float-rounding-mode)

Specify rounding modes to consider when determining the results of floating point arithmetic

Description

This option affects a Code Prover analysis only.

Specify the rounding modes to consider when determining the results of floating-point arithmetic.

Set Option

User interface (desktop products only): In your project configuration, the option is available on the Verification Assumptions node.

Command line and options file: Use the option -float-rounding-mode. See Command-Line Information.

Why Use This Option

The default verification uses the round-to-nearest mode.

Use the rounding mode all if your code contains routines such as fesetround to specify a rounding mode other than round-to-nearest. Although the verification ignores the fesetround specification, it considers all rounding modes including the rounding mode that you specified. Alternatively, for targets that can use extended precision (for instance, using the flag -mfpmath=387), use the rounding mode all. However, for your Polyspace^® analysis results to agree with run-time behavior, you must prevent use of extended precision through a flag such as -ffloat-store.

Otherwise, continue to use the default rounding mode to-nearest. Because all rounding modes are considered when you specify all, you can have many orange Overflow checks resulting from overapproximation.

Settings

Default: to-nearest

to-nearest

The verification assumes the round-to-nearest mode.

all

The verification assumes all rounding modes for each operation involving floating-point variables. The following rounding modes are considered: round-to-nearest, round-towards-zero, round-towards-positive-infinity, and round-towards-negative-infinity.

Tips

• The Polyspace analysis uses floating-point arithmetic that conforms to the IEEE^® 754 standard. For instance, the arithmetic uses floating point instructions present in the SSE instruction set. The GNU^® C flag -mfpmath=sse enforces use of this instruction set. If you use the GNU C compiler with this flag to compile your code, your Polyspace analysis results agree with your run-time behavior.

  However, if your code uses extended precision, for instance using the GNU C flag -mfpmath=387, your Polyspace analysis results might not agree with your run-time behavior in some corner cases. See some examples of these corner cases in codeprover_limitations.pdf in polyspaceroot\polyspace\verifier\code_prover_desktop. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2019a.

  To prevent use of extended precision, on targets without SSE support, you can use a flag such as -ffloat-store. For your Polyspace analysis, use all for rounding mode to account for double rounding.

• The Overflow check uses the rounding modes that you specify. For instance, the following table shows the difference in the result of the check when you change your rounding modes.

  Rounding mode: to-nearest

  Rounding mode: all

  If results of floating-point operations are rounded to nearest values: In the first addition operation, eps1 is just large enough that the value nearest to FLT_MAX + eps1 is greater than FLT_MAX. The Overflow check is red. In the second addition operation, eps2 is just small enough that the value nearest to FLT_MAX + eps2 is FLT_MAX. The Overflow check is green. #include <float.h> #define eps1 0x1p103 #define eps2 0x0.FFFFFFp103 float func(int ch) { float left_op = FLT_MAX; float right_op_1 = eps1, right_op_2 = eps2; switch(ch) { case 1: return (left_op + right_op_1); case 2: return (left_op + right_op_2); default: return 0; } }

  Besides to-nearest mode, the Overflow check also considers other rounding modes. In the first addition operation, in to-nearest mode, the value nearest to FLT_MAX + eps1 is greater than FLT_MAX, so the addition overflows. But if rounded towards negative infinity, the result is FLT_MAX, so the addition does not overflow. Combining these two rounding modes, the Overflow check is orange. In the second addition operation, in to-nearest mode, the value nearest to FLT_MAX + eps2 is FLT_MAX, so the addition does not overflow. But if rounded towards positive infinity, the result is greater than FLT_MAX, so the addition overflows. Combining these two rounding modes, the Overflow check is orange. #include <float.h> #define eps1 0x1p103 #define eps2 0x0.FFFFFFp103 float func(int ch) { float left_op = FLT_MAX; float right_op_1 = eps1, right_op_2 = eps2; switch(ch) { case 1: return (left_op + right_op_1); case 2: return (left_op + right_op_2); default: return 0; } }

  If you set the rounding mode to all and obtain an orange Overflow check, to determine how the overflow can occur, consider all rounding modes.

Command-Line Information

Parameter: -float-rounding-mode

Value: to-nearest | all

Default: to-nearest

Example (Code Prover): polyspace-code-prover -sources file_name -float-rounding-mode all

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -float-rounding-mode all