В анализе Polyspace используется арифметика с плавающей запятой, соответствующая стандарту IEEE ® 754. Например, арифметика использует команды с плавающей запятой, присутствующие в наборе команд SSE. Флаг ^GNU ® C -mfpmath=sse принудительно использует этот набор команд. При использовании компилятора GNU C с этим флагом для компиляции кода результаты анализа 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 для режима округления для учета двойного округления.

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

#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 и получите оранжевую проверку переполнения, чтобы определить, как может произойти переполнение, рассмотрим все режимы округления.