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

R2026b

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

Set the option using one of these methods:

  • Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Run Time Errors > Check Behavior node and then select this option.

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

  • Python® API: Set the AllowNonFiniteFloats property in the static analysis configuration. See polyspace.project.StaticAnalysisConfiguration (Polyspace Test).

  • TOML configuration file (.toml.pscfg) — Use the key AllowNonFiniteFloats in the [CodeProverVerification.CheckBehavior] table. For example:

    [CodeProverVerification.CheckBehavior]
AllowNonFiniteFloats = true

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 your code supports infinities and NaNs, 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. Using the option alone effectively disables many numerical checks on floating point operations. If you want a warning when an infinity or NaN appears in your code, 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 code 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 code 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.

    • Do not set the option -allow-non-finite-floats along with the value forbid for -check-nan and -check-infinite to indicate that your code does not support nonfinites. The default analysis without the option -allow-non-finite-floats already works this way.

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

    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 Test)

Topics