Описание

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

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

Риск

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

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

Пример - счетчики цикла for

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 совместим.

Пример - счетчики цикла while

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 совместимым.