Depth of verification inside structures (-k-limiting)

Limit the depth of analysis for nested structures

Description

This option affects a Code Prover analysis only.

Specify a limit to the depth of analysis for nested structures.

Set Option

Set the option using one of these methods:

• Polyspace^® user interface (desktop products only): In your project configuration, select the Scaling node and then select a value for the option.

• Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Run Time Errors > Scaling node and enter a value for this option. See Dependencies for other options must enable first.

• Command line and options file: Use the option -k-limiting. See Command-Line Information.

Why Use This Option

Use this option if the analysis is slow because your code has a structure that is many levels deep.

Typically, you see a warning message when a structure with a deep hierarchy is slowing down the verification.

Dependencies

To use this option in the Polyspace Platform user interface, you must set the option Set depth of verification inside structures to On ().

Settings

Default: Full depth of nested structures is analyzed.

Enter a number to specify the depth of analysis for nested structures. For instance, if you specify 0, the analysis does not verify a structure inside a structure.

If you specify a number less than 2, the verification could be less precise.

Command-Line Information

Parameter: -k-limiting

Value: positive integer

Example (Code Prover): polyspace-code-prover -sources file_name -k-limiting 3

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -k-limiting 3