В этом примере показано, как настроить многозадачное строение проекта 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()
{}

Чтобы настроить свои многозадачные строения и проанализировать код:

Bug Finder обнаруживает гонку данных на переменной 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() вызовы.

Code Prover обнаруживает, что 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() вызовы.