Exponenta Banner

Используемая неразделяемая переменная

Глобальные переменные используются в одной задаче

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

Описание

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

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

  • Polyspace® обнаруживает по крайней мере одну операцию чтения или операцию записи на переменной.

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

В ваших результатах верификации эти переменные окрашены в черный на панелях Variable Access и Results List.

Примеры

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

int var1;
int var2;
int var3;
int var4;

int input(void);

void main() {
    int loc_var = input(), flag=0;

    var1 = loc_var;
    if(0) {
        var3 = loc_var;
    }
    if(flag!=0) {
        var4 =loc_var;
    }


}

Если вы проверяете вышеупомянутый код в проекте C, программное обеспечение перечисляет var2, var3 и var4 как неразделяемые неиспользуемые переменные и var1 как неразделяемая используемая переменная.

var3 и var4 используются в недостижимом коде и поэтому отмечены как неиспользованные.

Примечание

В проекте C++ программное обеспечение не перечисляет неиспользуемую переменную var2.

unsigned int var_1;
unsigned int var_2;
volatile int randomVal;

void task1(void) {
    while(randomVal)
    	operation(1);
}

void task2(void) {
    while(randomVal)
	    operation(2);
}

void operation(int i) {
    if(i==1) {
        var_1++;
    }
    else    {
        var_2++;
    }
}

int main(void) {
    return 0;
}

В этом примере, даже когда вы задаете task1 и task2 для опции Tasks (-entry-points), программное обеспечение решает, что var_1 и var_2 неразделяемы.

Даже при том, что и task1 и task2 вызывают функциональный operation из-за оператора if в operation, task1 может работать только с var_1 и task2 только на var_2.

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

Язык: C | C++

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

| |

Документация Polyspace Code Prover
Поддержка