Main Content

Precision level (-O0 | -O1 | -O2 | -O3)

Specify a precision level for the verification

Description

This option affects a Code Prover analysis only.

Specify the precision level that the verification must use.

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 -O#, for instance, -O0 or -O1. See Command-Line Information.

Why Use This Option

Higher precision leads to greater number of proven results but also requires more verification time. Each precision level corresponds to a different algorithm used for verification.

In most cases, you see the optimal balance between precision and verification time at level 2.

Settings

Default: 2

0

This option corresponds to a static interval verification.

1

This option corresponds to a more complex static interval verification.

2

This option corresponds to a complex polyhedron model of domain values with additional precision for interprocedural analysis depending on the option Improve precision of interprocedural analysis (-path-sensitivity-delta).

3

This option is only suitable for code having less than 1000 lines. Using this option, the percentage of proven results can be very high.

Tips

  • For best results in reasonable time, use the default level 2. If the verification takes a long time, reduce precision. However, the number of unproven checks can increase. Likewise, to reduce orange checks, you can improve your precision. But the verification can take significantly longer time.

  • The precision levels 2 and below begin to take effect only from verification levels higher than Software Safety Analysis level 0. See also Verification level (-to).

    For instance, to reduce analysis time, you might have reduced the verification level to Software Safety Analysis level 0. Do not try to reduce the precision level below 2 to lower the analysis time further.

    Note that algorithms used in precision level 3 can also apply to the verification level Software Safety Analysis level 0.

Command-Line Information

Parameter: -O0 | -O1 | -O2 | -O3
Default: -O2
Example (Code Prover): polyspace-code-prover -sources file_name -O1
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -O1

See Also

|

Topics