В этом примере показано, как настроить многозадачную настройку проекта OSEK и запустить анализ этого проекта. Чтобы попробовать шаги в этом примере, используйте демонстрационные файлы в папке polyspaceroot/help/toolbox/bugfinder/examples/External_multitasking/OSEK или polyspaceroot/help/toolbox/codeprover/examples/External_multitasking/OSEK. polyspaceroot папка установки Polyspace. Результаты анализа применяются к этому примеру кода.

#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()
{}

Настраивать вашу многозадачную настройку и анализировать код:

Средство поиска ошибки обнаруживает гонку данных на переменной var3 из-за нескольких операция чтения и операция записи от задач init и afterinit1. Смотрите Data race.

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3;

На var2 нет никакого дефекта начиная с afterinit1 переходит к активному состоянию (ActivateTask()) после init шаг var2. Точно так же на var1 нет никакого дефекта потому что это защищено GetResource() и ReleaseResource() вызовы.

Программа автоматического доказательства кода обнаруживает тот var3 потенциально незащищенная глобальная переменная, потому что она используется в задачах init и afterinit1 без защиты от прерывания во время операций чтения и операций записи. Анализ также показывает что циклическая операция задачи на var4 может потенциально вызвать переполнение. Смотрите Potentially unprotected variable и Overflow.

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3;

...
void func()
{
  var4++;
}  

Переменный var2 не совместно используется потому что afterinit1 переходит к активному состоянию (ActivateTask()) после init шаг var2. Переменный var1 защищенная переменная через критические разделы от GetResource() и ReleaseResource() вызовы.