OIL files selection (-osek-multitasking)

Set up multitasking configuration from OIL file definition

Description

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

Specify the OIL files that Polyspace^® parses to set up the multitasking configuration of your OSEK project.

Set Option

User interface: In the Configuration pane, 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 -osek-multitasking. See Command-Line Information.

Why Use This Option

If your project includes OIL files, Polyspace can parse these files to set up tasks, interrupts, cyclical tasks, and critical sections. You do not have to set them up manually.

Settings

On

Polyspace looks for and parses OIL files to set up your multitasking configuration.

auto

Look for OIL files in your project source and include folders, but not in their subfolders.

custom

Look for OIL files on the specified path and the path subfolders. You can specify a path to the OIL files or to the folder containing the files.

When you select this option, in your source code, Polyspace supports these OSEK multitasking keywords:

• TASK

• DeclareTask

• ActivateTask

• DeclareResource

• GetResource

• ReleaseResource

• ISR

• DeclareEvent

• DeclareAlarm

Polyspace parses the OIL files that you provide for TASK, ISR, RESOURCE, and ALARM definitions. The analysis uses these definitions and the supported multitasking keywords to configure tasks, interrupts, cyclical tasks, and critical sections.

 Example: Analyze Your OSEK Multitasking Project

This example shows how to set up the multitasking configuration of an OSEK project and run an analysis on this project. To try the steps in this example, use the demo files in the folder polyspaceroot/help/toolbox/bugfinder/examples/External_multitasking/OSEK or polyspaceroot/help/toolbox/codeprover/examples/External_multitasking/OSEK. polyspaceroot is the Polyspace installation folder. The analysis results apply to this example code.

#include <assert.h> #include "include/example_osek_multi.h" int var1; int var2; int var3; DeclareAlarm(Cyclic_task_activate); DeclareResource(res1); DeclareTask(init); TASK(afterinit1); TASK(init) // task { var2++; ActivateTask(afterinit1); var3++; GetResource(res1); // critical section begins var1++; ReleaseResource(res1); // critical section ends } TASK(afterinit1) // task { var3++; var2++; GetResource(res1); // critical section begins var1++; ReleaseResource(res1); // critical section ends } void main() {}

To set up your multitasking configuration and analyze the code:

1. Copy the contents of polyspaceroot/help/toolbox/bugfinder/examples/External_multitasking/OSEK or polyspaceroot/help/toolbox/codeprover/examples/External_multitasking/OSEK to your machine, for instance in C:\Polyspace_worskpace\OSEK.

2. Run an analysis on your OSEK project by using the command:

   • Bug Finder:

     polyspace-bug-finder -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^ 
     -osek-multitasking auto

   • Code Prover:

     polyspace-code-prover -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^
     -osek-multitasking auto

   • Bug Finder Server:

     polyspace-bug-finder-server -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^ 
     -osek-multitasking auto

   • Code Prover Server:

     polyspace-code-prover-server -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^
     -osek-multitasking auto

Bug Finder detects a data race on variable var3 because of multiple read and write operation from tasks init and afterinit1. See Data race.

#include <assert.h> #include "include/example_osek_multi.h" int var1; int var2; int var3;

There is no defect on var2 since afterinit1 goes to an active state (ActivateTask()) after init increments var2. Similarly, there is no defect on var1 because it is protected by the GetResource() and ReleaseResource() calls.

Code Prover detects that var3 is a potentially unprotected global variable because it is used in tasks init and afterinit1 with no protection from interruption during the read and write operations. The analysis also shows that the cyclic task operation on var4 can potentially cause an overflow. See Potentially unprotected variable (Polyspace Code Prover) and Overflow (Polyspace Code Prover).

#include <assert.h> #include "include/example_osek_multi.h" int var1; int var2; int var3; ... void func() { var4++; }

Variable var2 is not shared because afterinit1 goes to an active state (ActivateTask()) after init increments var2. Variable var1 is a protected variable (Polyspace Code Prover) through the critical sections from the GetResource() and ReleaseResource() calls.

To see how Polyspace models the TASK, ISR, and RESOURCE definitions from your OIL files, open the Concurrency window from the Dashboard pane.

Off (default)

Polyspace does not set up a multitasking configuration for your OSEK project.

Additional Considerations

• Make sure that you declare all tasks by using the DeclareTask or TASK keywords before you pass those tasks as parameters to functions or macros that expect a task. For example , if you pass task foo to ActivateTask without using DeclareTask(foo); first, Polyspace considers task foo undefined which results in a compilation error.

• The analysis ignores TerminateTask() declarations in your source code and considers that subsequent code is executed.

• Polyspace ignores syntax elements of your OIL files that do not follow the syntax defined here.

Dependencies

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

Command-Line Information

Parameter: -osek-multitasking

Value: auto | custom='file1 [,file2, dir1,...]'

Default: Off

Example (Bug Finder): polyspace-bug-finder -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

Example (Code Prover): polyspace-code-prover -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

Example (Bug Finder Server): polyspace-bug-finder-server -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

Example (Code Prover Server): polyspace-code-prover-server -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'