Main Content

Improve precision of interprocedural analysis (-path-sensitivity-delta)

Avoid certain verification approximations for code with fewer lines

Description

This option affects a Code Prover analysis only.

For smaller code, use this option to improve the precision of cross-functional analysis.

Set Option

User interface (desktop products only): In your project configuration, the option is available on the Precision 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 > Precision node.

Command line and options file: Use the option -path-sensitivity-delta. See Command-Line Information.

Why Use This Option

Use this option to avoid certain software approximations on execution paths. Avoiding these approximations results in fewer orange checks but a much longer verification time.

For instance, for deep function call hierarchies or nested conditional statements, to complete verification in a reasonable amount of time, the software combines many execution paths and stores less information at each stage of verification. If you use this option, the software stores more information about the execution paths, resulting in a more precise verification.

Settings

Default: Off

Enter a positive integer to turn on this option.

Entering a higher value leads to a greater number of proven results, but also increases verification time exponentially. For instance, a value of 10 can result in very long verification times.

Tips

Use this option only when you have less than 1000 lines of code.

Command-Line Information

Parameter: -path-sensitivity-delta
Value: Positive integer
Example (Code Prover): polyspace-code-prover -sources file_name -path-sensitivity-delta 1
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -path-sensitivity-delta 1

See Also

Topics