Specific precision (-modules-precision)

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

Описание

Эта опция влияет только на анализ Code Prover.

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

Задать опцию

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

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

Зачем использовать эту опцию

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

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

Настройки

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

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

Зависимость

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

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

Параметр: -modules-precision
Значение: file:O0 | file:O1 | file:O2 | file:O3
Пример (Code Prover): Polyspace Code Prover -sources file_name -O1 -modules-precision My_File:02
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -O1 -modules-precision My_File:02