Задайте критические разделы с функциями тот, берут аргументы

При проверке многозадачного кода Polyspace^® полагает, что критический раздел находится между вызовами блокировки, и разблокируйте функцию.

lock();
/* Critical section code */
unlock();

Группа операций в критическом разделе является атомарной относительно другой группы операций, которые находятся в том же критическом разделе (то есть, имея ту же блокировку, и разблокируйте функцию). См. также Задают Атомарные Операции в Многозадачном Коде.

Предположение Polyspace на функциях, задающих критические разделы

Polyspace игнорирует аргументы к функциям, которые начинают и заканчивают критические разделы.

Например, Polyspace обрабатывает эти две секции кода ниже как тот же критический раздел, если вы задаете my_task_1 и my_task_2 как точки входа, my_lock как функция блокировки и my_unlock как разблокировать функция.

int shared_var;

void my_lock(int);
void my_unlock(int);

void my_task_1() {
   my_lock(1);
   /* Critical section code */
   shared_var=0;
   my_unlock(1);
}

void my_task_2() {
   my_lock(2);
   /* Critical section code */
   shared_var++;
   my_unlock(2);
}

В результате анализ полагает, что эти два раздела защищены от прерывания друг друга даже при том, что они не могут быть защищены. Например, Bug Finder не обнаруживает гонку данных на shared_var.

Часто, аргументы функции могут быть определены только во время выполнения. Начиная с моделей Polyspace критические разделы до статического анализа и фазы проверки ошибки времени выполнения, анализ не может определить, отличаются ли аргументы функции, и игнорирует аргументы.

Адаптируйте анализ Polyspace, чтобы заблокировать и разблокировать функции с аргументами

Когда аргументы к функциям, задающим критические разделы, являются константами времени компиляции, можно адаптировать анализ, чтобы работать вокруг предположения Polyspace.

Например, можно использовать опции анализа Polyspace так, чтобы код в предыдущем примере появился к Polyspace как показано здесь.

int shared_var;

void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);

void my_task_1() {
   my_lock_1();
   /* Critical section code */
   shared_var=0;
   my_unlock_1();
}

void my_task_2() {
   my_lock_2();
   /* Critical section code */
   shared_var++;
   my_unlock_2();
}

Если вы затем задаете my_lock_1 и my_lock_2 когда блокировка функционирует и my_unlock_1 и my_unlock_2 как разблокировать функции, анализ распознает два раздела кода как часть различных критических разделов. Например, Bug Finder обнаруживает гонку данных на shared_var.

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

В заголовочном файле common_polyspace_include.h, преобразуйте аргументы функции в расширения имени функции с #defineS. Кроме того, обеспечьте объявление для новых функций.
Например, для предыдущего примера, используйте их #define- s и объявления:
```
#define my_lock(X) my_lock_##X()
#define my_unlock(X) my_unlock_##X()

void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);
```
Задайте имя файла common_polyspace_include.h в качестве аргумента для опции Include (-include).
Анализ рассматривает этот заголовочный файл как #include- d во всех исходных файлах, которые анализируются.
Задайте новые имена функций как начало функций и окончание критических разделов. Используйте опции Critical section details (-critical-section-begin -critical-section-end).

Документация