Main Content

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 Option

User interface (desktop products only): In your project configuration, the option is available on the Precision node. See Dependency for other options you must also enable.

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 -modules-precision. See Command-Line Information.

Why Use This Option

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.

Settings

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.

Dependency

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

Command-Line Information

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

See Also

Topics