NaNs (-check-nan)

Specify how to handle floating-point operations that result in NaN

Description

This option affects a Code Prover analysis only.

Specify how the analysis must handle floating-point operations that result in NaN.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node. See Dependencies for other options you must also enable.

Command line and options file: Use the option -check-nan. See Command-Line Information.

Why Use This Option

Use this option to enable detection of floating-point operations that result in NaN-s.

If you specify that the analysis must consider nonfinite floats, by default, the analysis does not flag these operations. Use this option to detect these operations while still incorporating nonfinite floats.

Settings

Default: allow

allow

The verification does not produce a check on the operation.

For instance, in the following code, there is no Invalid operation on floats check.

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

warn-first

The verification produces a check on the operation. The check determines if the result of the operation is NaN when the operands themselves are not NaN. For instance, the check flags the operation val1 + val2 only if the result can be NaN when both val1 and val2 are not NaN. The verification does not terminate the execution thread that produces NaN.

If the verification detects an operation that produces NaN as the only possible result on all execution paths and the operands themselves are never NaN, the check is red. If the operation can potentially result in NaN, the check is orange.

For instance, in the following code, there is a nonblocking Invalid operation on floats check for NaN.

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

Even though the Invalid operation on floats check on the - operation is red, the verification continues. For instance, a green Non-initialized local variable check appears on y in the return statement.

forbid

The verification produces a check on the operation and terminates the execution thread that produces NaN.

If the check is red, the verification does not continue for the remaining code in the same scope as the check. If the check is orange, the verification continues but removes from consideration the variable values that produced a NaN.

For instance, in the following code, there is a blocking Invalid operation on floats check for NaN.

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

The verification stops because the Invalid operation on floats check on the - operation is red. For instance, a Non-initialized local variable check does not appear on y in the return statement.

The Invalid operation on floats check for NaN also appears on the / operation and is green.

Dependencies

To use this option, you must enable the verification mode that incorporates infinities and NaNs. See Consider non finite floats (-allow-non-finite-floats).

Command-Line Information

Parameter: -check-nan

Value: allow | warn-first | forbid

Default: allow

Example (Code Prover): polyspace-code-prover -sources file_name -check-nan forbid

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -check-nan forbid