В анализе Polyspace используется арифметика с плавающей точкой, которая соответствует IEEE^® 754 стандарт. Для образца арифметика использует команды с плавающей точкой, существующие в наборе команд SSE. GNU^® Флаг C -mfpmath=sse обеспечивает принудительное использование этого набора команд. Если вы используете компилятор GNU C с этим флагом для компиляции кода, результаты анализа Polyspace согласуются с поведением во время выполнения.

Однако, если ваш код использует расширенную точность, например, используя флаг GNU C -mfpmath=387результаты анализа Polyspace могут не согласиться с поведением во время выполнения в некоторых угловых случаях. Смотрите некоторые примеры этих угловых случаев в codeprover_limitations.pdf в polyspaceroot\ polyspace\verifier\code _ prover _ рабочий стол. Здесь, polyspaceroot является папкой установки Polyspace, например C:\Program Files\Polyspace\R2019a.

Чтобы предотвратить использование расширенной точности, на целях без поддержки SSE, можно использовать флаг, такой как -ffloat-store. Для анализа Polyspace используйте all для режима округления, учитывающего двойное округление.

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

#include <float.h>
#define eps1 0x1p103
#define eps2 0x0.FFFFFFp103

float func(int ch) {
    float left_op = FLT_MAX;
    float right_op_1 = eps1, right_op_2 = eps2;
    switch(ch) {
    case 1:
        return (left_op + right_op_1);
    case 2:
        return (left_op + right_op_2);
    default:
        return 0;
    }
}

#include <float.h>
#define eps1 0x1p103
#define eps2 0x0.FFFFFFp103

float func(int ch) {
    float left_op = FLT_MAX;
     float right_op_1 = eps1, right_op_2 = eps2;
    switch(ch) {
    case 1:
        return (left_op + right_op_1);
    case 2:
        return (left_op + right_op_2);
    default:
        return 0;
    }
}

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