Main Content

Verify files independently (-unit-by-unit)

Option to verify each source file independently of other source files

Description

This option affects a Code Prover analysis only.

This option is not available for code generated from MATLAB® code or Simulink® models.

The Verify files independently option determines whether each source file must be verified independently of other source files. When you enable this option, Code Prover verifies each file independent of other files in the module. You can view verification results for the entire project or for individual files.

After you open the verification result for one file, in the user interface of the Polyspace® desktop products, you can see a summary of results for all files on the Dashboard pane. You can open the results for each file directly from this summary table.

Each result file (with name ps_results.pscp) is saved in a subfolder of the results folder. The subfolder has the same name as the source file being analyzed.

Code Prover requires a main function as the starting point of verification. In file-by-file mode, because most files do not have a main function, Code Prover generates a main function when required. By default, the generated main function calls uncalled functions (uncalled nonprivate methods and out-of-class functions in C++). For more information, see:

Set Option

User interface (desktop products only): In your project configuration, the option is on the Code Prover Verification node. See Dependencies for other options that you must also enable.

User interface (Polyspace Platform, desktop products only): In your project configuration, in the Static Analysis tab, click Run Time Errors and then select Verify files independently.

Command line and options file: Use the option -unit-by-unit. See Command-Line Information.

Why Use This Option

There are many reasons to verify each source file independently of other files. For example, if verification of a project takes a long time, you can perform a file-by-file verification to identify which file is slowing the verification.

Settings

On

Polyspace creates a separate verification job for each source file.

Off (default)

Polyspace creates a single verification job for all source files in a module.

Dependencies

This option is enabled only if you select Verify module or library (-main-generator).

Tips

  • If you perform a file-by-file verification, you cannot specify multitasking options.

  • If your verification for the entire project takes a long time, perform a file by file verification. After the verification is complete for a file, you can view the results while other files are still being verified.

  • You can generate a report of the verification results for each file or for all the files together. To generate a single report for all files, perform the report generation after verification (and not along with verification using analysis options).

    To generate a single report for all the files in the Polyspace user interface (desktop product only):

    1. Open the results for one file.

    2. Select Reporting > Run Report. Before generating the report, select the option Generate a single report including all unit results.

    To generate a single report for all the files in the Polyspace Platform user interface (desktop product only):

    1. Open the results for one file.

    2. Select Report > Run Report. Before generating the report, select the option Report for all files.

    If you use the product Polyspace Code Prover™ Server™ to run a verification, to generate a single report for all files:

    • Upload the results for all files to the Polyspace Access server.

    • Use the polyspace-report-generator command with option -all-units to generate a single report for all the files.

  • When you perform a file-by-file verification, you can see many instances of unused variables. Some of these variables might be used in other files but show as unused in a file-by-file verification.

    If you want to ignore these results, use a review scope (named set of filters) that filters out unused variables. See Filter and Group Results in Polyspace Desktop User Interface (Polyspace Code Prover).

Command-Line Information

Parameter: -unit-by-unit
Default: Off
Example (Code Prover): polyspace-code-prover -sources file1,file2,... -unit-by-unit
Example (Code Prover Server): polyspace-code-prover-server -sources file1,file2,... -unit-by-unit