-init-only-mode)Проверьте код инициализации только на ошибки времени выполнения и другие проблемы
Эта опция влияет только на анализ Code Prover.
Задайте, что Polyspace® необходимо проверить только раздел кода, отмеченный как код инициализации, на ошибки времени выполнения и других проблем.
Чтобы указать конец кода инициализации, вы вводите линию
#pragma polyspace_end_of_init
main функция (только один раз). Код инициализации начинается с начала main и продолжается до этой прагмы.Поскольку компиляторы игнорируют непризнанные прагмы, наличие этой прагмы не влияет на выполнение программы.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Code Prover Verification.
Командная строка и файл опций: Используйте опцию -init-only-mode. См. «Информация о командной строке».
Часто проблемы в коде инициализации могут сделать недействительным анализ оставшегося кода. Можно использовать эту опцию, чтобы проверить код инициализации в одиночку и исправить проблемы, а затем отключить эту опцию, чтобы проверить оставшуюся программу.
Например, в этом примере:
#include <limits.h>
int aVar;
const int aConst = INT_MAX;
int anotherVar;
int main() {
aVar = aConst + 1;
#pragma polyspace_end_of_init
anotherVar = aVar - 1;
return 0;
}
aVar = aConst+1 перед значением aVar используется в последующем коде.
НаPolyspace проверяет код с начала main и продолжается до прагмы polyspace_end_of_init.
Off (по умолчанию)Polyspace проверяет полное приложение начиная с main функция.
Использовать эту опцию и обозначить раздел кода как код инициализации можно только в том случае, если:
Ваша программа содержит main и вы используете эту опцию Verify whole application (неявно установленный по умолчанию в командной строке).
Вы задаете Source code language (-lang) на C.
Обратите внимание, что прагма должна появиться только один раз в main функция. Прагма может появиться до или после объявлений переменных, но должна появиться после определений типов (typedef-с).
Вы не можете использовать эту опцию со следующими опциями:
Используйте эту опцию вместе с опцией Check that global variables are initialized after warm reboot (-check-globals-init) тщательно проверить код инициализации перед проверкой оставшейся программы. Если вы используете обе опции, верификация проверяет следующее:
Определенные или возможные ошибки времени выполнения в коде инициализации.
Все ли не - const глобальные переменные инициализируются по всем путям выполнения через код инициализации.
Опции многозадачности отключены, если вы проверяете код инициализации только потому, что инициализация глобальных переменных ожидается до начала задач (потоков). В результате тела задач не проверяются.
Смотрите также Многозадачность.
Если вы проверяете только код инициализации, анализ обрезает пути выполнения, содержащие прагму в местоположении прагмы, но продолжает проверять другие пути выполнения.
Например, в этом примере pragma появляется в if блок. В линии появляется красная неинициализированная проверка переменной int a = var потому что путь, содержащий инициализацию, останавливается в местоположении прагмы. На единственном другом оставшемся пути, который обходит if блок, переменная var не инициализирован.
int var;
int func();
int main() {
int err = func();
if(err) {
var = 0;
#pragma polyspace_end_of_init
}
int a = var;
return 0;
}
Check that global variables are initialized after warm reboot (-check-globals-init).Чтобы определить инициализацию структуры, регулярный анализ Code Prover рассматривает только используемые поля.
Если вы проверяете код инициализации только с помощью этой опции, анализ охватывает только фрагмент кода и не может определить, используется ли переменная за пределами этого фрагмента. Поэтому при проверке на инициализацию учитываются все используемые или нет структурные поля.
Параметр:
-init-only-mode |
| По умолчанию: Off |
Пример (Code Prover):
Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources |
Check that global variables are initialized after warm reboot (-check-globals-init) | Global variable not assigned a value in initialization code