Exponenta Banner

Potentially unprotected variable

Глобальные переменные, совместно использованные несколькими задачами, но не защищенный от параллельного доступа задачами

расширьте все на странице

Описание

Разделяемая незащищенная глобальная переменная имеет следующие свойства:

  • Переменная используется больше чем в одной задаче.

  • Polyspace® определяет при наименьшем количестве одной операции на переменной, не защищен от прерывания операциями в других задачах.

В коде, который не предназначается для многозадачности, все глобальные переменные неразделяемы.

В ваших результатах верификации эти переменные окрашены в оранжевый на Source, Results List и панелях Variable Access. На панели Source окраска применяется к переменной только во время объявления.

Примеры

развернуть все

#include <limits.h>
int shared_var;

void inc() {
    shared_var+=2;
}

void reset() {
    shared_var = 0;
}

void task() {
    volatile int randomValue = 0;
    while(randomValue) {
        reset();
        inc();
        inc();
    }
}

void interrupt() {
    shared_var = INT_MAX;
}

void interrupt_handler() {
    volatile int randomValue = 0;
    while(randomValue) {
        interrupt();
    }
}

void main() {
}

В этом примере, shared_var незащищенная совместно используемая переменная, если вы задаете следующие многозадачные опции:

ОпцияЗначение
Сконфигурируйте многозадачность вручную
Задачи

task

interrupt_handler

Вы не задаете механизмы защиты, такие как критические разделы.

Операция shared_var = INT_MAX может прервать другие операции на shared_var и вызовите непредсказуемое поведение.

Если вы кликаете (график) по значку на панели Result Details, вы видите две параллельных задачи (потоки).

Первый график показывает, как задачи получают доступ к переменной. Например, задача interrupt_handler вызывает функциональный interrupt это пишет в совместно используемую переменную shared_var.

Второй график показывает, как задачи создаются. В этом примере обе задачи создаются после main завершается. В других случаях задачи могут быть созданы в функциях, вызванных от main.

Проверяйте информацию

Язык: C | C++

Смотрите также

| | | | | | |

Темы

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

Поддержка