Инициализация глобальных переменных

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

Инициализация глобальной переменной, когда main Функция существует

Если ваш код содержит main функция, верификация Программы автоматического доказательства Кода полагает, что глобальные переменные инициализируются согласно стандартам ANSI® C. Значения по умолчанию:

  • 0 для int

  • 0 для char

  • 0.0 для float

и так далее.

Иногда, вы можете хотеть проверять, инициализируются ли глобальные переменные явным образом в коде. Например:

  • В горячей перезагрузке, чтобы сэкономить время, не загружается bss сегмент программы, которая может содержать значения переменных от предыдущего состояния. Вместо этого программа, как предполагается, явным образом инициализирует все переменные неconst без значений по умолчанию перед выполнением. Можно разграничить этот код инициализации и проверить, что все глобальные переменные неconst действительно инициализируются в горячей перезагрузке.

    Чтобы разграничить раздел кода как код инициализации, введите прагму polyspace_end_of_init в main функция. Код инициализации начинается с main функционируйте и продолжается до этой прагмы. Используйте эти опции, чтобы проверять код инициализации только и определить, инициализируются ли все глобальные переменные в этом разделе кода:

    Анализ Программы автоматического доказательства Кода сообщает о неинициализированных переменных с помощью красных или оранжевых результатов в коде инициализации для проверок:

  • Чтобы только проверять, инициализируются ли глобальные переменные явным образом при использовании, используйте опцию Ignore default initialization of global variables (-no-def-init-glob).

    Анализ Программы автоматического доказательства Кода сообщает о неинициализированных переменных с помощью красных или оранжевых результатов для проверки Non-initialized variable.

Инициализация глобальной переменной, когда main Функция не существует

Если ваш код не имеет main функция, Программа автоматического доказательства Кода начинает проверять каждую невостребованную функцию учитывая, что глобальные переменные имеют полнофункциональное значение, ограниченное только их типом данных. См. также Переменные диапазоны.

Например, рассмотрите этот пример:

int glob;
void func1_callee();

void func1() {
    int loc =  glob;
    if(!glob)
       func1_callee();
}

void func1_callee() {
    int loc = glob;
}

void func2() {
    int loc = glob;
}
В обоих func1 и func2, глобальная переменная glob и следовательно локальная переменная loc имеет полный спектр int значения.

Однако только невостребованные функции начинаются с полнофункциональных значений глобальных переменных. Функциональный func1_callee называется в func1 после значения glob ограничивается обнулить. В func1_callee, глобальная переменная glob и следовательно локальная переменная loc имеет ограниченный нуль значения.

Как программа автоматического доказательства кода реализует предположение об инициализации глобальной переменной

Программное обеспечение использует фиктивный функциональный _init_globals() инициализировать глобальные переменные. _init_globals() функция является первой функцией, неявно вызванной в main функция (или сгенерированный main функционируйте, если нет никакого main).

Считайте следующий код в приложении gv_example.c.

extern int func(int);

int garray[3] = {1, 2, 3};  
int gvar = 12;

int main(void) {
    int i, lvar = 0;
    for (i = 0; i < 3; i++) 
       lvar += func(garray[i] + gvar);
    return lvar;
}

После верификации:

  • На панели Results List, если вы выбираете File из списка под узлом gv_example.c, вы видите _init_globals.

  • На панели Variable Access, gv_example._init_globals представляет инициализацию глобальной переменной. Столбец Values показывает значение глобальной переменной сразу после инициализации.

Какие средние значения инициализации для сложных типов данных

В следующей таблице перечислены то, что проверяется на каждый тип данных, чтобы определить инициализацию. Проверка происходит во время операций чтения для проверки Non-initialized variable и в конце раздела инициализации для проверки Global variable not assigned a value in initialization code.

Тип данныхКакая зеленая проверка на средние значения инициализации
Фундаментальные типы (int'double', и т.д.)Переменная записана, по крайней мере, однажды.
Типы данных массиваКаждый элемент массива записан, по крайней мере, однажды.
Структурированные типы данных

Каждое поле структуры, которое используется, записано, по крайней мере, однажды.

Если вы проверяете код инициализации только с помощью опции Verify initialization section of code only (-init-only-mode), анализ проверяет на инициализацию всех полей структуры, или используемый или нет.

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

УказателиУказатель записан, по крайней мере, однажды. Однако Программа автоматического доказательства Кода не проверяет на инициализацию резкого буфера (пока вы не разыменовываете указатель).
Перечисленияenum переменная записана, по крайней мере, однажды. Однако Программа автоматического доказательства Кода не проверяет, имеет ли переменная один из enum значения.

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

| | |