Этот пример показывает, как настроить многозадачную настройку проекта 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

}

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

TASK(Cyclic_task) // cyclic task
{
  func();
}

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, потому что он защищен вызовами ReleaseResource() и GetResource().

Программа автоматического доказательства кода обнаруживает, что 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 является защищенной переменной через критические разделы от вызовов ReleaseResource() и GetResource().