-init-only-mode)Проверяйте один только код инициализации на ошибки времени выполнения и другие проблемы
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что 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 используется в последующем коде.
OnPolyspace проверяет код с начала main и продолжает до прагмы polyspace_end_of_init.
От (значения по умолчанию)Polyspace проверяет законченное приложение, начинающееся с main функция.
Можно использовать эту опцию и определять раздел кода как код инициализации только если:
Ваша программа содержит main функционируйте и вы используете опцию Verify whole application (Polyspace Code Prover) (неявно набор по умолчанию в командной строке).
Вы устанавливаете Source code language (-lang) toc.
Обратите внимание на то, что прагма должна появиться только однажды в main функция. Прагма может появиться прежде или после объявлений переменной, но должна появиться после определений типа (typedefS.
Вы не можете использовать эту опцию со следующими опциями:
Используйте эту опцию наряду с опцией Check that global variables are initialized after warm reboot (-check-globals-init) полностью проверять код инициализации прежде, чем проверять остающуюся программу. Если вы используете обе опции, верификация проверяет на следующее:
Определенные или возможные ошибки времени выполнения в коде инициализации.
Ли весь non-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).Чтобы определить инициализацию структуры, регулярный анализ Программы автоматического доказательства Кода только рассматривает поля, которые используются.
Если вы проверяете код инициализации только с помощью этой опции, анализ покрывает только фрагмент кода и не может определить, используется ли переменная вне этого фрагмента. Поэтому проверки на инициализацию рассматривают все поля структуры, или используемый или нет.
Параметр:
-init-only-mode |
| Значение по умолчанию: Off |
Пример (Программа автоматического доказательства Кода):
Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Check that global variables are initialized after warm reboot (-check-globals-init) | Global variable not assigned a value in initialization code (Polyspace Code Prover Access)