Set depth of verification inside structures

Specify that depth of verification inside structures must be specified

Since R2023b

Description

The option with this name is available only in the Polyspace Platform (Polyspace Test) user interface. For the equivalent option in the standard Polyspace^® user interface, see Depth of verification inside structures (-k-limiting).

Specify whether you want to set the option Depth of verification inside structures (-k-limiting).

Set Option

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Scaling node.

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

Why Use This Option

If your code is structured with many levels, then a Polyspace Code Prover™ verification might be slower than you expect. In such a case, use this option to enable the option Depth of verification inside structures (-k-limiting) so that you can limit the depth of verification.

Settings

On: Polyspace enables the option Depth of verification inside structures (-k-limiting).
Off (default): Polyspace keeps the field Depth of verification inside structures (-k-limiting) disabled.

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

Version History

Introduced in R2023b