Main Content

Subnormal detection mode (-check-subnormal)

Detect operations that result in subnormal floating-point values

Description

This option affects a Code Prover analysis only.

Specify that the verification must check floating-point operations for subnormal results.

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 -check-subnormal. See Command-Line Information.

Why Use This Option

Use this option to detect floating-point operations that result in subnormal values.

Subnormal numbers have magnitudes less than the smallest floating-point number that can be represented without leading zeros in the significand. The presence of subnormal numbers indicates loss of significant digits. This loss can accumulate over subsequent operations and eventually result in unexpected values. Subnormal numbers can also slow down the execution on targets without hardware support.

Settings

Default: allow

allow

The verification does not check operations for subnormal results.

forbid

The verification checks for subnormal results.

The verification stops the execution path with the subnormal result and prevents subnormal values from propagating further. Therefore, in practice, you see only the first occurrence of the subnormal value.

warn-all

The verification checks for subnormal results and highlights all occurrences of subnormal values. Even if a subnormal result comes from previous subnormal values, the result is highlighted.

The verification continues even if the check is red.

warn-first

The verification checks for subnormal results but only highlights first occurrences of subnormal values. If a subnormal value propagates to further subnormal results, those subsequent results are not highlighted.

The verification continues even if the check is red.

For details of the result colors in each mode, see Subnormal float.

Tips

  • If you want to see only those operations where a subnormal value originates from non-subnormal operands, use the warn-first mode.

    For instance, in the following code, arg1 and arg2 are unknown. The verification assumes that they can take all values allowed for the type double. This assumption can lead to subnormal results from certain operations. If you use the warn-first mode, the first operation causing the subnormal result is highlighted.

    warn-allwarn-first

    void func (double arg1, double arg2) 
{
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}

    In this example, all four operations can have subnormal results. The four checks for subnormal results are orange.

    void func (double arg1, double arg2) 
{
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}

    In this example, difference1 and difference2 can be subnormal if arg1 and arg2 are sufficiently close. The first two checks for subnormal results are orange. val1 and val2 cannot be subnormal unless difference1 and difference2 are subnormal. The last two checks for subnormal results are green.

    Through red/orange checks, you see only the first instance where a subnormal value appears. You do not see red/orange checks from those subnormal values propagating to subsequent operations.

  • If you want to see where a subnormal value originates and do not want to see subnormal results arising from the same cause more than once, use the forbid mode.

    For instance, in the following code, arg1 and arg2 are unknown. The verification assumes that they can take all values allowed for the type double. This assumption can lead to subnormal results for arg1-arg2. If you use the forbid mode and perform the operation arg1-arg2 twice in succession, only the first operation is highlighted. The second operation is not highlighted because the subnormal result for the second operation arises from the same cause as the first operation.

    warn-allforbid

    void func (double arg1, double arg2) 
{
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}

    In this example, all four operations can have subnormal results. The four checks for subnormal results are orange.

    void func (double arg1, double arg2) 
{
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}

    In this example, difference1 can be subnormal if arg1 and arg2 are sufficiently close. The first check for subnormal results is orange. Following this check, the verification excludes from consideration:

    • The close values of arg1 and arg2 that led to the subnormal value of difference1.

      In the subsequent operation arg1 - arg2, the check is green and difference2 is not subnormal. The result of the check on difference2 * 2 is green for the same reason.

    • The subnormal value of difference1.

      In the subsequent operation difference1 * 2, the check is green.

Command-Line Information

Parameter: -check-subnormal
Value: allow | warn-first | warn-all | forbid
Default: allow
Example (Code Prover): polyspace-code-prover -sources file_name -check-subnormal forbid
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -check-subnormal forbid

Version History

Introduced in R2016b

See Also

Polyspace Results

Topics