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

Однако, если ваш код использует расширенную точность, например, с помощью флага GNU C -mfpmath=387, ваши результаты анализа Polyspace не могут согласиться с вашим поведением во время выполнения в некоторых угловых случаях. Смотрите некоторые примеры этих угловых случаев в codeprover_limitations.pdf в polyspaceroot\polyspace\verifier\code_prover_desktop. Здесь, 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, чтобы определить, как переполнение может произойти, рассмотрите все режимы округления.