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

Можно просмотреть результаты проверки 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 на панели Variable Access. Если вы проверяете только код инициализации, проверяется только код жирным шрифтом, и вы должны просматривать только образцы в коде инициализации.

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

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

Попробуйте поместить прагму непосредственно в 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
    }
}

Чтобы определить инициализацию структуры, регулярный анализ Code Prover рассматривает только используемые поля.

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