В этом примере показано, как настроить многозадачную конфигурацию проекта 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() вызовы.

Средство проверки кода обнаруживает, что 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() вызовы.