Modularize Polyspace Analysis at Command Line Based on an Initial Interdependency Analysis

Analyzing the entire code base for a single application might take a long time, depending on the size of the application.

For a large application, Polyspace^® allows you to:

Partition the application into modules that individually require less time to verify.
Specify the number of modules in a tradeoff between verification speed and precision.

You can carry out faster analysis with a larger number of small modules. During partitioning, the software automatically minimizes cross-module references. However, with more modules, greater cross-module referencing is required during verification, which results in a loss of precision.

Basic Options

You can partition an application into modules using the following batch command:

polyspace-modularize [target_folder] {option1,option2,...}

This table describes the basic options that you can use.

Option	Description
`target_folder`	Folder that contains the results of the initial run that processes source files. Default is the folder from which you run `polyspace-modularize`.
`-o=output_folder`	Output folder for partitioned application. Default is the folder from which you run `polyspace-modularize`.
`-gui=max_n`	The Polyspace verification environment displays the Modularizing choices window with a predefined limit for the maximum number of modules that you can select. Use this option to specify a new limit `max_n`.
`-matlab=max_n`	If data cache for Modularizing choices window does not exist, create cache `project_name_max_n.m`. Cache enables faster display of Modularizing choices window. `project_name` is the value used by `-prog` option. `max_n` is the limit for the maximum number of modules that you can select. No action if cache already exists.
`-modules=n`	Partition application into `n` modules. Identical to clicking the gray region associated with `n` in the Modularizing choices window.
`-max-complexity=max_c`	Partitions application into modules with reference to specified maximum complexity `max_c`. The complexity of a function is a number that is related to the size of the function. The complexity of a module is the sum of the complexities of the functions in the module. When partitioning your application, the software minimizes the use of cross-module references to functions and variables, subject to the constraint that the complexity of a module does not exceed `max_c`. If you make `max_c` sufficiently large, the software generates only one module, which is identical to the original, unpartitioned application.

Constrain Module Complexity During Partitioning

To force all functions to have a complexity of 1, run the following command:

polyspace-modularize -uniform-complexities

Result Folder Names

By default, modularization results folders are named projectName_kk_module:

kk is either the max complexity argument you give to -max-complexity, or the number of modules.

You can control the naming of result folders in the i^th module using the -stem option:

polyspace-modularize -stem=stem_format

stem_format is a string. The # and @ characters in the string are processed as follows:

# — Replaced by the number of modules in the partitioning.
@ — Replaced by the argument of -max-complexity.

For example, if you want a specific name, MyName, which overrides the project name and does not incorporate the module number, then run:

polyspace-modularize -stem=MyName

Forbid Cycles in Module Dependence Graph

By default, the software allows the module dependence graph to have cycles. However, in some cases, you might get better results with acyclic graphs. Use the following command:

polyspace-modularize -forbid-cycles