Specific precision (-modules-precision)

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

Описание

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

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

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

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

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

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

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

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

Настройки

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

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

Зависимость

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

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

Параметр: -modules-precision
Значение: file:O0 | file:O1 | file:O2 | file:O3
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - O1 - точность модулей My_File:02
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - O1 - точность модулей My_File:02