Main Content

Consider non finite floats (-allow-non-finite-floats)

Enable an analysis mode that incorporates infinities and NaNs

Description

Enable an analysis mode that incorporates infinities and NaNs for floating point operations.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node.

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.

Command line and options file: Use the option -allow-non-finite-floats. See Command-Line Information.

Why Use This Option

Code Prover

By default, the analysis does not incorporate infinities and NaNs. For instance, the analysis terminates the execution thread where a division by zero occurs and does not consider that the result could be infinite.

If you use functions such as isinf or isnan and account for infinities and NaNs in your code, set this option. When you set this option and a division by zero occurs for instance, the execution thread continues with infinity as the result of the division.

Set this option alone if you are sure that you have accounted for infinities and NaNs in your code. Using the option alone effectively disables many numerical checks on floating point operations. If you have generally accounted for infinities and NaNs, but you are not sure that you have considered all situations, set these additional options:

Bug Finder

If the analysis flags comparisons using isinf or isnan as dead code, use this option. By default, a Bug Finder analysis does not incorporate infinities and NaNs.

Settings

On

The analysis allows infinities and NaNs. For instance, in this mode:

  • The analysis assumes that floating-point operations can produce results such as infinities and NaNs.

    By using options Infinities (-check-infinite) and NaNs (-check-nan), you can choose to highlight operations that produce nonfinite results and stop the execution threads where the nonfinite results occur. These options are not available for a Bug Finder analysis.

  • The analysis assumes that floating-point variables with unknown values can have any value allowed by their type, including infinite or NaN. Floating-point variables with unknown values include volatile variables and return values of stubbed functions.

Off (default)

The analysis does not allow infinities and NaNs. For instance, in this mode:

  • The Code Prover analysis produces a red check on a floating-point operation that produces an infinity or a NaN as the only possible result on all execution paths. The verification produces an orange check on a floating-point operation that can potentially produce an infinity or NaN.

  • The Code Prover analysis assumes that floating-point variables with unknown values are full-range but finite.

  • The Bug Finder analysis shows comparisons with infinity using isinf as dead code.

Tips

  • The IEEE® 754 Standard allows special quantities such as infinities and NaN so that you can handle certain numerical exceptions without aborting the code. Some implementations of the C standard support infinities and NaN.

    • If your compiler supports infinities and NaNs and you account for them explicitly in your code, use this option so that the verification also allows them.

      For instance, if a division results in infinity, in your code, you specify an alternative action. Therefore, you do not want the verification to highlight division operations that result in infinity.

    • If your compiler supports infinities and NaNs but you are not sure if you account for them explicitly in your code, use this option so that the verification incorporates infinities and NaNs. Use the options -check-nan and -check-infinite with argument warn so that the verification highlights operations that result in infinities and NaNs, but does not stop the execution thread. These options are not available for a Bug Finder analysis.

  • If you run a Code Prover analysis and use this option, checkers for overflow, division by zero and other numerical run-time errors are disabled. See Numerical Checks (Polyspace Code Prover).

    If you run a Bug Finder analysis and use this option:

  • If you select this option, the number and type of Code Prover checks in your code can change.

    For instance, in the following example, when you select the option, the results have one less red check and three more green checks.

    Infinities and NaNs Not AllowedInfinities and NaNs Allowed

    Code Prover produces a Division by zero error and stops verification.

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

    If you select this option, Code Prover does not check for a Division by zero error. 

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

    The analysis assumes that dividing by zero results in:

    • Value of x equal to Inf

    • Value of y equal to 0.0

    • Value of z equal to NaN

    In your analysis results in the Polyspace® user interface, if you place your cursor on y and z, you can see the nonfinite values Inf and NaN respectively in the tooltip.

Command-Line Information

Parameter: -allow-non-finite-floats
Default: Off
Example (Bug Finder): polyspace-bug-finder -sources file_name -allow-non-finite-floats
Example (Code Prover): polyspace-code-prover -sources file_name -allow-non-finite-floats
Example (Bug Finder Server): polyspace-bug-finder-server -sources file_name -allow-non-finite-floats
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -allow-non-finite-floats

Version History

Introduced in R2016a

See Also

| | | (Polyspace Code Prover)

Topics