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

Можно рассмотреть результаты средства проверки Global variable not assigned a value in initialization code (Polyspace Code Prover Access) относительно легко.

Рассмотрите этот пример. На 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
    }
}

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

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