-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 используется в последующем коде.
НаPolyspace проверяет код с начала main и продолжается вплоть до прагматики polyspace_end_of_init.
Выкл. (по умолчанию)Polyspace проверяет полное приложение, начиная с main функция.
Эту опцию можно использовать и обозначить раздел кода как код инициализации только в том случае, если:
Ваша программа содержит main и вы используете опцию Verify whole application (неявно устанавливается по умолчанию в командной строке).
Вы установили Source code language (-lang) кому C.
Обратите внимание, что прагматика должна появиться только один раз в main функция. Прагматика может появляться перед объявлениями переменных или после них, но должна появляться после определений типов (typedef-s).
Этот параметр нельзя использовать со следующими параметрами:
Используйте эту опцию вместе с опцией 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).Для определения инициализации структуры при регулярном анализе средства проверки кода учитываются только используемые поля.
Если проверить код инициализации только с помощью этой опции, анализ охватывает только часть кода и не может определить, используется ли переменная за пределами этой части. Поэтому при проверке инициализации учитываются все поля структуры, независимо от того, используются они или нет.
Параметр:
-init-only-mode |
| По умолчанию: Откл. |
Пример (проверка кода):
polyspace-code-prover -sources |
Пример (сервер проверки кода):
polyspace-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