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.

#include <stdio.h>
#include <stdlib.h>
#define SIZE_ARRAY 3

typedef unsigned int uint32;

// Defining three functions of which 
// only one accesses a global variable
uint32 var;

void Write_to_var(void) {
    var+=1;
}

void No_write_read_1(void) {
}

void No_write_read_2(void) {
   
}

// Defining a 3-element array of function pointers 
// that point to the three functions
typedef void (*FuncPtr)(void);
typedef struct {
    FuncPtr pFuncPtr;
}FuncPtrStruct;

const FuncPtrStruct FuncPtrArray[SIZE_ARRAY] =
{
    { &Write_to_var    },
    { &No_write_read_1 },
    { &No_write_read_2 }
};

void main() {}

// Defining a function that calls one of the three functions 
// via the function pointer
void function(int uiSignalType) {
    FuncPtrArray[uiSignalType].pFuncPtr();
}

// Entry-point functions in void(void) format for Polyspace analysis
// Analyze this example with
// -D POLYSPACE -entry-points task_10ms,task_20ms,task_50ms

#ifdef POLYSPACE
void task_10ms(void) {
    int signalType;
    signalType = 0;
    function(signalType);
}

void task_20ms(void) {
    int signalType;
    signalType = 1;
    function(signalType);
}

void task_50ms(void) {
    int signalType;
    signalType = 2;
    function(signalType);
}

#endif

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

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

task_10ms

task_20ms

task_50ms

Preprocessor definitions (-D)POLYSPACE

Однако сообщение на переменной показывает, что может быть потенциально записано или считано одной из задач task_10ms, task_20ms, или task_50ms.

Message on variable var shows that it can be accessed by all three tasks.

var не совместно используемая переменная вообще, поскольку к ней получают доступ только в задаче, task_10ms. Однако анализ сообщает обо всех трех задачах как о доступе к переменной из-за приближения на линии:

FuncPtrArray[uiSignalType].pFuncPtr();
FuncPtrArray массив указателей функции. Указатель в индексе 0 указывает на функциональный Write_to_var, который обновляет переменную var. Указатели в индексах 1 и 2 указывают на функции No_write_read_1 и No_write_read_2, которые не получают доступ к var вообще. Однако анализ не хранит информацию, на который вызовы доступа к массиву, которые функционируют. Вместо этого анализ делает звуковое приближение, что безотносительно индекса, каждый доступ к массиву потенциально вызывает одну из трех функций.

В результате этого приближения анализ полагает что задачи task_10ms, task_20ms и task_50ms может потенциально вызвать каждую из функций Write_to_var, No_write_read_1 и No_write_read_2. Различный аналитический маршрут решает правильно, что переменная не совместно используется.

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

Язык: C | C++

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

| | | | | | |

Темы

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

Поддержка