Verification level (-to)

Specify number of times the verification process runs on your code

expand all in page

Description

This option affects a Code Prover analysis only.

Specify the number of times the Polyspace® verification process runs on your source code. Each run can lead to greater number of proven results but also requires more verification time.

Set Option

Set the option using one of these methods:

  • Polyspace user interface (desktop products only): In your project configuration, select the Precision node and then select a value for this option.

  • 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 -to. See Command-Line Information.

Why Use This Option

There are many reasons you might want to increase or decrease the verification level. For instance, If you see many orange checks after verification, try increasing the verification level. If your analysis takes longer than expected, try decreasing the verification level.

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

Settings

Default: Software Safety Analysis level 2

Source Compliance Checking

Polyspace checks for compilation errors only.

Software Safety Analysis level 0

The verification process performs some simple analysis. The analysis is designed to reach completion despite complexities in the code.

If the verification gets stuck at a higher level, try running to this level and review the results.

Software Safety Analysis level 1

The verification process analyzes each function once with algorithms whose complexity depends on the precision level. See Precision level (-O). The analysis starts from the top of the function call hierarchy (an actual or generated main function) and propagates to the leaves of the call hierarchy.

Software Safety Analysis level 2

The verification process analyzes each function twice. In the first pass, the analysis propagates from the top of the function call hierarchy to the leaves. In the second pass, the analysis propagates from the leaves back to the top. Each pass uses information gathered from the previous pass.

Use this option for most accurate results in reasonable time.

Software Safety Analysis level 3

The verification process runs three times on each function: from the top of the function call hierarchy to the leaves, from the leaves to the top, and from the top to the leaves again. Each pass uses information gathered from the previous pass.

Software Safety Analysis level 4

The verification process runs four passes on each function: from the top of the function call hierarchy to the leaves twice. Each pass uses information gathered from the previous pass.

other

If you use this option, Polyspace verification will make 20 passes unless you stop it manually.

Tips

  • If the verification takes too long, use a lower Verification level. For best results, use the option Software Safety Analysis level 2.

  • Fix red errors and gray code before rerunning the verification with higher verification levels.

  • In some cases, if the results have reached the maximum precision at an earlier level, the verification stops and does not proceed to the level that you specify. If a higher verification level fails because the verification runs out of memory, but results are available at a lower level, Polyspace displays the results from the lower level.

  • Use the option Other sparingly since it might increase verification time by an unreasonable amount.

  • When running Polyspace analyses on a remote server, the source phase takes place on your local computer. If the Verification Level is set to Source Compliance Checking, do not use -batch to submit jobs to a remote server from a desktop. See Run Bug Finder or Code Prover analysis on a remote cluster (-batch).

  • If you want to see only global variable sharing and usage, use Show global variable sharing and usage only (-shared-variables-mode) to run a less extensive analysis.

Command-Line Information

Parameter: -to
Value: compile | pass0 | pass1 | pass2 | pass3 | pass4 | other
Default: pass2
Example (Code Prover): polyspace-code-prover -sources file_name -to pass2
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -to pass2

You can also use these additional values not available in the user interface:

  • C projects: c-to-il (C to intermediate language conversion phase)

  • C++ projects: cpp-to-il (C++ to intermediate language conversion phase), cpp-normalize (C++ compilation), cpp-link (C++ compilation)

Use these values only if you have specific reasons to do so. For instance, to generate a blank constraints (DRS) template for C++ projects, run an analysis up to the compilation by using cpp-link or cpp-normalize.

The values cpp-link and cpp-normalize will be removed in a future release. Use compile instead.

Examples

expand all

Running a Code Prover verification at a higher verification level reduces the number of orange checkers.

Run a Code Prover verification on this code while setting the precision to Software Safety Analysis level 0.

extern int tab[];

int main() {
    
    int i = tab[3];
    int j = tab[1];

    if (i > j) {
        int l = i-j;
        assert(l > 0);
     }
}

There is an orange check in the assert statement.

To resolve the orange check, run the analysis at a higher precision. For instance, run another verification on the preceding code while setting the precision to Software Safety Analysis level 1.

extern int tab[];

int main() {
    
    int i = tab[3];
    int j = tab[1];

    if (i > j) {
        int l = i-j;
        assert(l > 0);
     }
}
The assert statement now has a green check.

See Also

|

Topics