Infinities (-check-infinite)

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

Description

This option affects a Code Prover analysis only.

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

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.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Run Time Errors > Check Behavior node. See Dependencies for other options you must also enable.

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

Why Use This Option

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

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 Overflow check.

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

warn-first

The verification produces a check on the operation. The check determines if the result of the operation is infinite when the operands themselves are not infinite. The verification does not terminate the execution thread that produces infinity.

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

For instance, in the following code, there is a nonblocking Overflow check for infinity.

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

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

forbid

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

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 infinity.

For instance, in the following code, there is a blocking Overflow check for infinity.

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

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

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-infinite

Value: allow | warn-first | forbid

Default: allow

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

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

Version History

Introduced in R2016a