Interrupts (-interrupts)

Specify functions that represent nonpreemptable interrupts

Description

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

Specify functions that represent nonpreemptable interrupts. The analysis assumes that operations in the function body:

• Can execute any number of times.

• Cannot be interrupted by noncyclic tasks, cyclic tasks or other interrupts. Noncyclic tasks are specified with the option Tasks (-entry-points) and cyclic tasks are specified with the option Cyclic tasks (-cyclic-tasks).

  To model an interrupt that can be interrupted by other interrupts, specify the interrupt as preemptable. See -preemptable-interrupts. For examples, see Define Preemptable Interrupts and Nonpreemptable Tasks.

Set Option

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

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

Why Use This Option

Use this option to specify interrupts in your multitasking code. The functions that you specify must have the prototype:

void function_name(void);

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=INT_MAX; occurs in an interrupt and var++ occurs in the body of a task, an overflow can occur if the interrupt excepts before the operation in the task. The analysis detects the possible overflow.

A Bug Finder analysis uses your specifications to look for concurrency defects. For the Data race defect, the analysis establishes the following relations between interrupts and other tasks:

• Data race between two interrupts:

  Two operations in different interrupts cannot interfere with each other (unless one of the interrupts is preemptable). Even if the operations use the same shared variable without protection, a data race cannot occur.

• Data race between an interrupt and another task:

  • An operation in an interrupt cannot interfere with an atomic operation in any other task. Even if the operations use the same shared variable without protection, a data race cannot occur.

  • An operation in an interrupt can interfere with a nonatomic operation in any other task unless the other task is also a nonpreemptable interrupt. Therefore, if the operations use the same shared variable without protection, a data race can occur.

See Concurrency Defects.

Settings

No Default

Enter function names or choose from a list.

• Click to add a field and enter the function name.

• Click to list functions in your code. Choose functions from the list.

Dependencies

To enable this option in the user interface of the desktop products, first select the option Configure multitasking manually.

Tips

• In Code Prover, the functions representing interrupts must have the form

  void functionName (void)

• If a function func takes arguments or returns a value, you cannot use it directly as an interrupt. To use func as an interrupt, call func from a wrapper void-void function and specify the wrapper as an interrupt. See Configuring Polyspace Multitasking Analysis Manually.

• If you specify a function as an interrupt, you must provide its definition. Otherwise, a Code Prover verification stops with the error message:

  task func_name must be a userdef function without parameters

  A Bug Finder analysis continues but does not consider the function as an interrupt.

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

• The Polyspace^® multitasking analysis assumes that an interrupt cannot interrupt itself.

Command-Line Information

Parameter: -interrupts

No Default

Value: function1[,function2[,...]]

Example (Bug Finder): polyspace-bug-finder -sources file_name -interrupts func_1,func_2

Example (Code Prover): polyspace-code-prover -sources file_name -interrupts func_1,func_2

Example (Bug Finder Server): polyspace-bug-finder-server -sources file_name -interrupts func_1,func_2

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -interrupts func_1,func_2