Ошибки времени выполнения в коде инициализации могут сделать анализ оставшегося кода недействительным. Перед проверкой оставшейся программы можно выполнить сравнительно быструю проверку кода инициализации.

Вы можете просмотреть результаты проверки Global variable not assigned a value in initialization code относительно легко.

Рассмотрим этот пример. Есть оранжевый чек на var потому что var может оставаться неинициализированным, когда if и else if операторы пропускаются.

int var;
 
int checkSomething(void);
int checkSomethingElse(void);
 
int main() {
    int local_var;
    if(checkSomething())
    {
        var=0;
    }
    else if(checkSomethingElse()) {
        var=1;
    }
    #pragma polyspace_end_of_init
    var=2;
    local_var = var;
    return 0;
}
 

Чтобы просмотреть эту проверку и понять, когда x может быть не инициализирован, необходимо просмотреть все экземпляры x на панели «Доступ к переменной». При проверке только кода инициализации проверяется только код, выделенный полужирным шрифтом, и необходимо просматривать только экземпляры кода инициализации.

Размещайте прагматику только после завершения кода инициализации.

В противном случае переменная может выглядеть ложно неинициализированной.

Попробуйте поместить прагматику прямо в main функция, то есть вне блока. При размещении прагматики в блоке проверка учитывает только те пути, которые заканчиваются в блоке.

Все пути, которые заканчиваются в блоке, могут иметь инициализированную переменную, но пути, которые пропускают блок, могут оставить переменную неинициализированной. Если прагматика помещена в блок, убедитесь, что переменная остается неинициализированной вне блока.

Например, в этом примере переменная var инициализируется на всех путях, которые заканчиваются в расположении прагматики. Чек зеленый, несмотря на то, что if блок может быть пропущен, в результате чего переменная не будет инициализирована.

int var;

int func();

int main() {
    int err = func();
    if(err) {
        var = 0;
 #pragma polyspace_end_of_init
    }
    int a = var;   
    return 0;
}

Проблема обнаруживается средством проверки при размещении прагматики после if концы блоков.

Не помещайте прагматику в петлю.

Если поместить прагматику в цикл, можно увидеть результаты, которые трудно интерпретировать. Например, в этом примере оба aVar и anotherVar инициализируются в одной итерации цикла. Однако прагматика рассматривает первую итерацию цикла только тогда, когда она показывает зеленую проверку для инициализации. Если переменная инициализирована на более поздней итерации, проверка будет оранжевой.

int aVar;
int anotherVar;

void main() {
    for(int i=0; i<=1; i++) {
        if(i == 0)
            aVar = 0;
        else
            anotherVar = 0;
        #pragma polyspace_end_of_init
    }
}

Для определения инициализации структуры при регулярном анализе средства проверки кода учитываются только используемые поля.

При проверке кода инициализации только с помощью опции Verify initialization section of code only (-init-only-mode)анализ охватывает только часть кода и не может определить, используется ли переменная за пределами этой части. Поэтому при проверке инициализации учитываются все поля структуры, независимо от того, используются они или нет.