Глобальные переменные являются переменными, которые отображаются в программе (если не затененный локальными переменными). Анализ Программы автоматического доказательства Кода делает определенные предположения об инициализации глобальных переменных.
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', и т.д.) | Переменная записана, по крайней мере, однажды. |
| Типы данных массива | Каждый элемент массива записан, по крайней мере, однажды. |
| Структурированные типы данных | Каждое поле структуры, которое используется, записано, по крайней мере, однажды. Если вы проверяете код инициализации только с помощью опции В особом случае, где ни одно из полей не используется, проверки на инициализацию являются оранжевыми вместо зеленого, если весь fields.are деинициализировал. |
| Указатели | Указатель записан, по крайней мере, однажды. Однако Программа автоматического доказательства Кода не проверяет на инициализацию резкого буфера (пока вы не разыменовываете указатель). |
| Перечисления | enum переменная записана, по крайней мере, однажды. Однако Программа автоматического доказательства Кода не проверяет, имеет ли переменная один из enum значения. |
Check that global variables are initialized after warm reboot (-check-globals-init) | Global variable not assigned a value in initialization code | Non-initialized variable | Verify initialization section of code only (-init-only-mode)