-preemptable-interrupts

Specify functions that represent preemptable interrupts

Syntax

-preemptable-interrupts function1[,function2[,...]]

Description

-preemptable-interrupts function1[,function2[,...]] specifies functions that represent preemptable interrupts.

The function acts as an interrupt in every way except that it can be interrupted by other interrupts, preemptable or nonpreemptable. Interrupts are specified with the option Interrupts (-interrupts). For examples, see Define Task Priorities for Data Race Detection in Polyspace.

To specify a function as a preemptable interrupt, you must first specify the function as an interrupt. The functions that you specify must have the prototype:

void function_name(void);

If you are running an analysis from the user interface (Polyspace^® desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other.

Examples

Consider the following program. Suppose that functions task1 and task2 represent interrupts.

int x;
void task1() {
    x++;
}
void task2() {
    x = 0;
}
void main() {
}

To specify that task1 and task2 are cyclic tasks, enter the following:

polyspace-bug-finder -sources filename -interrupts task1,task2

You do not see a Data race defect because the operations in task1 and task2 cannot interrupt each other. Functions specified as interrupts are nonpreemptable by default.

Specify task1 as preemptable.

polyspace-bug-finder -sources multi.c -interrupts task1,task2 -preemptable-interrupts task1

A Data race now appears because the operation x++ in task1 can be interrupted by operations in task2.

Tips

This option is not useful in a Polyspace as You Code analysis.
Code Prover interprets this option with some limitations. The reason is that Code Prover considers all operations as potentially non-atomic and interruptible. This overapproximation leads to situations where the option might appear to be ignored. For an example, see Effect of Task Priorities in Code Prover (Polyspace Code Prover).

Version History

Introduced in R2016b