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

При проверке многозадачного кода 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);
}

В результате анализ полагает, что эти два раздела защищены от прерывания друг друга даже при том, что они не могут быть защищены. Например, Средство поиска Ошибки не обнаруживает гонку данных на 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 как разблокировать функции, анализ распознает два раздела кода как часть различных критических разделов. Например, Средство поиска Ошибки обнаруживает гонку данных на shared_var.

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

В заголовочном файле common_polyspace_include.h преобразуйте аргументы функции в расширения имени функции с #define-s. Кроме того, обеспечьте объявление для новых функций.
Например, для предыдущего примера, используйте их #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).

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