Глобальные переменные являются переменными, которые видны в программе (если не затенены локальными переменными). Анализ Code Prover делает конкретные предположения об инициализации глобальных переменных.
main Функция существуетЕсли ваш код содержит main function, a Кода Prover верификации считает, что глобальные переменные инициализируются согласно ANSI® Стандарты C. Значениями по умолчанию являются:
0 для int
0 для char
0,0 для float
и так далее.
Иногда можно хотеть проверить, явным ли образом инициализированы глобальные переменные в коде. Для образца:
При теплой перезагрузке, чтобы сэкономить время, сегмент bss программы, который может удерживать значения переменных от предыдущего состояния, не загружается. Вместо этого программа должна явным образом инициализировать все неконстовые переменные без значений по умолчанию перед выполнением. Можно разделить этот код инициализации и проверить, что все неконстатные глобальные переменные действительно инициализированы при теплой перезагрузке.
Чтобы разделить раздел кода как код инициализации, введите прагму polyspace_end_of_init в main функция. Код инициализации начинается с main функция и продолжается до этой прагмы. Используйте эти опции, чтобы проверить только код инициализации и определить, инициализированы ли все глобальные переменные в этом разделе кода:
Анализ Code Prover сообщает о неинициализированных переменных с использованием красных или оранжевых результатов в коде инициализации для проверок:
Чтобы проверить, явным образом ли инициализированы глобальные переменные в точке использования, используйте опцию Ignore default initialization of global variables (-no-def-init-glob).
Анализ Code Prover сообщает о неинициализированных переменных, используя красные или оранжевые результаты для проверки Non-initialized variable.
main Функция не существуетЕсли ваш код не имеет main function, Code Prover начинает верификацию каждой неотключенной функции с предположением, что глобальные переменные имеют полное значение области значений, ограниченное только их типом данных. Смотрите также Допущения о переменных Областях значений.
Например, рассмотрим этот пример:
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() для инициализации глобальных переменных. The _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, и т.д.) | Переменная записывается хотя бы один раз. |
| Типы данных массива | Каждый элемент массива записывается хотя бы один раз. |
| Структурированные типы данных | Каждое используемое поле структуры записывается хотя бы один раз. Если вы проверяете код инициализации только с помощью опции В особых случаях, когда ни одно из полей не используется, проверки инициализации являются оранжевыми, а не зелеными, если все поля не инициализированы. |
| Указатели | Указатель записывается хотя бы один раз. Однако Code Prover не проверяет на инициализацию заостренного буфера (пока вы не высмеиваете указатель). |
| Перечисления | The enum переменная записывается по крайней мере один раз. Однако Code Prover не проверяет, есть ли у переменной один из 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)