-float-rounding-mode
)Задайте округление режимов, чтобы рассмотреть при определении результатов арифметики с плавающей точкой
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте округляющиеся режимы, чтобы рассмотреть при определении результатов арифметики с плавающей точкой.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Verification Assumptions.
Командная строка: Используйте опцию -float-rounding-mode
. Смотрите информацию о командной строке.
Верификация по умолчанию использует режим раунда-к-самому-близкому.
Используйте округляющийся режим all
если ваш код содержит стандартные программы, такие как fesetround
задавать округляющийся режим кроме раунда-к-самому-близкому. Несмотря на то, что верификация игнорирует fesetround
спецификация, это рассматривает все режимы округления включая округляющийся режим, который вы задали. В качестве альтернативы для целей, которые могут использовать расширенную точность (например, с помощью флага -mfpmath=387
), используйте округляющийся режим all
. Однако для ваших результатов анализа Polyspace®, чтобы согласиться с поведением во время выполнения, необходимо предотвратить использование расширенной точности через флаг, такой как -ffloat-store
.
В противном случае продолжите использовать режим to-nearest
округления значения по умолчанию. Поскольку все режимы округления рассматриваются, когда вы задаете
all
, у вас может быть много оранжевых проверок Overflow, следующих из сверхприближения.
Значение по умолчанию: to-nearest
to-nearest
Верификация принимает режим раунда-к-самому-близкому.
all
Верификация принимает все режимы округления для каждой операции, включающей переменные с плавающей точкой. Следующие режимы округления рассматриваются: раунд-к-самому-близкому, круглый по направлению к нулю, круглый к положительной бесконечности, и вокруг к отрицательной бесконечности.
Анализ 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
папка установки Polyspace, например, polyspaceroot
C:\Program Files\Polyspace\R2019a
.
Чтобы предотвратить использование расширенной точности, на целях без поддержки SSE, можно использовать флаг, такой как -ffloat-store
. Для вашего анализа Polyspace используйте all
для округления режима с учетом двойного округления.
Проверка Overflow использует округляющиеся режимы, которые вы задаете. Например, следующая таблица показывает различие в результате проверки, когда вы изменяете свое округление режимов.
Режим Rounding: to-nearest | Режим Rounding: all | ||
---|---|---|---|
Если результаты операций с плавающей точкой округлены к самым близким значениям:
| Помимо к-самому-близкому режима, проверка Overflow также рассматривает другие режимы округления.
|
Если вы устанавливаете округляющийся режим на all
и получите оранжевую проверку Overflow, чтобы определить, как переполнение может произойти, рассмотрите все режимы округления.
Параметр: -float-rounding-mode |
Значение: to-nearest | all |
Значение по умолчанию: to-nearest |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |