-data-range-specifications)Ограничивайте глобальные переменные, входные параметры функции и возвращаемые значения упрямых функций
Эта опция применяется, в основном, к анализу Code Prover. В Bug Finder можно задать только внешние ограничения на глобальные переменные.
Задайте ограничения (также известные как спецификации области значений или DRS) для глобальных переменных, входных параметров функции и возвращаемых значений упрямых функций с помощью файла шаблона Constraint Specification. Файл шаблона является XML файл, который можно сгенерировать в Polyspace® пользовательский интерфейс.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Inputs & Stubbing.
Командная строка и файл опций: Используйте опцию -data-range-specifications. См. «Информация о командной строке».
Используйте эту опцию для определения ограничений вне вашего кода.
Polyspace использует код, который вы предоставляете, чтобы делать предположения о элементах, таких как переменные области значений и разрешённый buffer size для указателей. Иногда предположения шире, чем вы ожидаете, потому что:
Вы не предоставили полный код. Для примера вы не предоставили некоторые определения функций.
Часть информации о переменных доступна только во время выполнения. Для примера некоторые переменные в вашем коде получают значения от пользователя во время исполнения.
Из-за этих широких предположений:
Code Prover может учитывать больше путей выполнения, чем те пути, которые происходят во время выполнения. Если операция прекращается вдоль одного из выполнения путей, Polyspace помещает оранжевую проверку на операцию. Если этот путь выполнения не происходит во время исполнения, оранжевая проверка указывает на ложное срабатывание.
Bug Finder иногда может выдать ложные срабатывания.
Чтобы уменьшить количество таких ложных срабатываний, можно задать дополнительные ограничения на глобальные переменные, входные параметры функции и возвращаемые значения упрямых функций.
После того, как вы задаете свои ограничения, можно сохранить их как XML- файл, чтобы использовать их для последующих анализов. Если ваш исходный код изменится, можно обновить предыдущие ограничения. Вы не должны создавать новый шаблон ограничений.
По умолчанию нет
Введите полный путь к файлу шаблона. Также щелкните
, чтобы открыть мастер Constraint Specification. Этот мастер позволяет вам сгенерировать файл шаблона или перейти к существующему файлу шаблона.
Для получения дополнительной информации см. раздел «Задание внешних ограничений».
Параметр: -data-range-specifications |
Значение: file |
| По умолчанию нет |
Пример (Bug Finder):
Polyspace Bug Finder -sources file_name |
Пример (Code Prover):
Polyspace Code Prover -sources file_name |
Пример (Bug Finder Server): polyspace-bug-finder-server -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |