Проблема происходит, когда счетчик цикла имеет тип с плавающей точкой.

Если for индекс является переменным символом, Polyspace^® проверяет, что это не плавание.

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

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

int main(void){
    unsigned int counter = 0u;
    int result = 0;
    float foo;

    // Float loop counters
    for(float foo = 0.0f; foo < 1.0f; foo +=0.001f){ 
        /* Non-compliant - counter = 1000 at the end of the loop */
        ++counter;
    }

    float fff = 0.0f; 
    for(fff = 0.0f; fff <12.0f; fff += 1.0f){    /* Non-compliant*/
        result++;
    }

    // Integer loop count
    for(unsigned int count = 0u; count < 1000u; ++count){ /* Compliant */
        foo = (float) count * 0.001f;
    }
}

В этом примере, трех for циклы показывают три различных счетчика цикла. Первый и второй for плавающие переменные использования циклов как счетчики цикла, и поэтому несовместимы. Третий цикл использует целочисленный count как счетчик цикла. Даже при том, что count используется в качестве плавания в цикле, переменная остается целое число при действии как индекс цикла. Поэтому этот for цикл совместим.

int main(void){
    unsigned int u32a;
    float foo;

    foo = 0.0f;
    while (foo < 1.0f){
        foo += 0.001f;  /* Non-compliant - foo used as a loop counter */
    }

    foo = read_float32();
    do{
        u32a = read_u32();
    }while( ((float)u32a - foo) > 10.0f );   
                        /* Compliant - foo doesn't change in the loop */
                        /*  so cannot be a counter */
    return 1; 
}

Этот пример показывает два while циклы, оба из которых используют foo в while- условия цикла.

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

Второй while цикл не использует foo в цикле, но действительно использует foo в while- условие. Так foo не счетчик цикла. Целочисленный u32a счетчик цикла, потому что он изменяется в цикле и является частью в то время как условие. Поскольку u32a целое число, проблемой погрешности округления не является беспокойство, делая этот while совместимый цикл.