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

Set the option using one of these methods:

Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Run Time Errors > Precision node and then select a value for this option.
Command line and options file: Use the option -O#, for instance, -O0 or -O1. See Command-Line Information.
Python^® API: Set the PrecisionLevel property in the static analysis configuration. See polyspace.project.StaticAnalysisConfiguration (Polyspace Test).
TOML configuration file (.toml.pscfg) — Use the key PrecisionLevel in the [CodeProverVerification.Precision] table. For example:
```
[CodeProverVerification.Precision]
PrecisionLevel = "2"
```

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

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