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