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