Specific precision (`-modules-precision`)

Specify source files you want to verify at higher precision than the remaining verification

Description

This option affects a Code Prover analysis only.

Specify source files that you want to verify at a precision level higher than that for the entire verification.

Set the option using one of these methods:

Polyspace^® user interface (desktop products only): In your project configuration, select the Precision node and then enter values for this option. See Dependencies for other options you must enable first.
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 enter values for this option. See Dependencies for other options you must enable first.
Command line and options file: Use the option -modules-precision. See Command-Line Information.

If a specific file is verified imprecisely leading to many orange checks in the file and elsewhere, you can improve the precision for that file.

Note that increasing precision also increases verification time.

Default: All files are verified with the precision you specified using Precision > Precision level.

Click to enter the name of a file without the extension .c and the corresponding precision level.

This option is available only if you set Source code language (-lang) to C or C-CPP.

Parameter: -modules-precision

Value: file:O0 | file:O1 | file:O2 | file:O3

Example (Code Prover):

polyspace-code-prover -sources file_name -O1
                    -modules-precision My_File:O2

Example (Code Prover Server):

polyspace-code-prover-server -sources
                        file_name -O1 -modules-precision
                    My_File:O2