Определенная точность (-modules-precision)

Задайте исходные файлы, которые вы хотите проверить в более высокой точности, чем остающаяся верификация

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Задайте исходные файлы, которые вы хотите проверить на уровне точности выше, чем это для целой верификации.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Precision. Смотрите Зависимость для других опций, которые необходимо также включить.

Командная строка: Используйте опцию -modules-precision. Смотрите информацию о Командной строке.

Почему использование эта опция

Если определенный файл проверяется, неточно ведя ко многим оранжевым регистрациям файла и в другое место, можно улучшить точность для того файла.

Обратите внимание на то, что увеличение точности также увеличивает время верификации.

Настройки

Значение по умолчанию: Все файлы проверяются с точностью, вы задали использование Precision> Precision level.

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

Зависимость

Эта опция доступна, только если вы устанавливаете Source code language (-lang) на C или C-CPP.

Информация о командной строке

Параметр: -modules-precision
Значение: file:O0 | file:O1 | file:O2 | file:O3
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -O1 -modules-precision My_File:02
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -O1 -modules-precision My_File:02