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