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

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

User interface (Polyspace Platform, desktop products only): In your project configuration, the relevant options are on the Static Analysis tab on the Run Time Errors > Precision node. In the Polyspace Platform user interface, this option is split into two options: Set depth of verification inside structures and Depth of verification inside structures (-k-limiting).

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