Configure multitasking manually

Consider that code is intended for multitasking

Description

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

Specify whether your code is a multitasking application. This option allows you to manually configure the multitasking structure for Polyspace^®.

Set Option

User interface (desktop products only): In your project configuration, the option is available on the Multitasking node.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Multitasking node.

Command line and options file: See Command-Line Information.

Why Use This Option

By default, Bug Finder determines your multitasking model from your use of multithreading functions. In Code Prover, you have to enable automatic concurrency detection with the option Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection). However, in some cases, using automatic concurrency detection can slow down the Code Prover analysis.

In cases where automatic concurrency detection is not supported, you can explicitly specify your multitasking model by using this option. Once you select this option, you can explicitly specify your entry point functions, cyclic tasks, interrupts and protection mechanisms for shared variables, such as critical section details.

A Code Prover verification uses your specifications to determine:

Whether a global variable is shared.
See Global Variables (Polyspace Code Prover).
Whether a run-time error can occur.
For instance, if the operation var++ occurs in the body of a cyclic task and you do not impose a limit on var, the operation can overflow. The analysis detects the possible overflow.

A Bug Finder analysis uses your specifications to look for concurrency defects. For more information, see Concurrency Defects.

Settings

On

The code is intended for a multitasking application.

You have to explicitly specify your multitasking configuration using other Polyspace options. See Configuring Polyspace Multitasking Analysis Manually.

Off (default)

The code is not intended for a multitasking application.

Disabling the option has this additional effect in Code Prover:

If a main exists, Code Prover verifies only those functions that are called by the main.
If a main does not exist, Polyspace verifies the functions that you specify. To verify the functions, Polyspace generates a main function and calls functions from the generated main in a sequence that you specify. For more information, see Verify module or library (-main-generator).

Tips

If you run a file by file verification in Code Prover, your multitasking options are ignored. See Verify files independently (-unit-by-unit).

Command-Line Information

There is no single command-line option to turn on multitasking analysis. By using any of the options Tasks (-entry-points), Cyclic tasks (-cyclic-tasks) or Interrupts (-interrupts), you turn on multitasking analysis.