Этот пример показывает, как задать ограничения (также известный как спецификации области значений данных или DRS) на переменных в вашем коде. Polyspace® использует код, который вы предоставляете, чтобы сделать предположения об элементах, таких как переменные диапазоны и позволенный buffer size для указателей. Иногда предположения более широки, чем, что вы ожидаете потому что:
Вы не предоставили полный код. Например, вы не предоставляли некоторые функциональные определения.
Часть информации о переменных доступна только во время выполнения. Например, некоторые переменные в вашем коде получают значения от пользователя во время выполнения.
Из-за этих широких предположений:
Программа автоматического доказательства кода может рассмотреть больше путей к выполнению, чем те пути, которые происходят во время выполнения. Если операция перестала работать вдоль одного из путей к выполнению, Polyspace помещает оранжевую проверку в операцию. Если тот путь к выполнению прибывает из предположения, которое слишком широко, оранжевая проверка может указать на положительную ложь.
Средство поиска ошибки может иногда производить ложные положительные стороны.
Чтобы сократить количество таких ложных положительных сторон, можно задать дополнительные ограничения на глобальные переменные, входные параметры функции, и возвращаемые значения и модифицируемые аргументы заблокированных функций. Вы сохраняете ограничения как XML-файл, чтобы использовать их для последующих исследований. Если ваш исходный код изменяется, можно обновить предыдущие ограничения. Вы не должны создавать новый ограничительный шаблон.
В Средстве поиска Ошибки можно только ограничить глобальные переменные. Вы не можете ограничить входные параметры функции или возвращаемые значения заблокированных функций.
Откройте настройку проекта. На панели Configuration выберите Inputs & Stubbing.
Справа от Constraint setup нажмите кнопку Edit, чтобы открыть окно Constraint Specification.
В диалоговом окне Constraint Specification создайте пустой ограничительный шаблон. Шаблон содержит список всех переменных, на которые можно обеспечить ограничения. Чтобы создать новый шаблон, щелкнуть
. Программное обеспечение компилирует ваш проект и создает шаблон. Новый шаблон хранится в файле Module_number_Project_name_drs_template.xml
Задайте свои ограничения и сохраните шаблон как XML-файл. Для получения дополнительной информации смотрите Внешние Ограничения для Анализа Polyspace.
Нажмите OK.
Вы видите полный путь к XML-файлу шаблона в поле Constraint setup. Если при запуске анализ, Polyspace использует этот шаблон для извлечения переменных ограничений.
Используйте опцию Constraint setup (-data-range-specifications), чтобы задать ограничительный XML-файл.
Задавать ограничения в XML-файле:
Во-первых, создайте пустой шаблон XML. Шаблон перечисляет все глобальные переменные, входные параметры функции и модифицируемые аргументы и возвращаемые значения заблокированных функций, не задавая ограничений на них.
Чтобы создать пустой шаблон, запустите анализ только до фазы компиляции. В Средстве поиска Ошибки отключите проверку дефектов. Используйте опцию Find defects (-checkers). В Программе автоматического доказательства Кода проверяйте на исходное соответствие только. Используйте аргумент compile для опции Verification level (-to). После анализа пустой шаблон XML drs-template.xml создается в папке результатов.
Для проектов C++, чтобы создать пустой ограничительный шаблон, необходимо использовать аргумент cpp-normalize для опции Verification level (-to).
Отредактируйте XML-файл, чтобы задать ваши ограничения.
Для примеров см.:
Ограничьте область значений глобальной переменной (Polyspace Code Prover)
Ограничьте входные параметры функции (Polyspace Code Prover)
Можно ограничить переменные диапазоны на основе их ожидаемой области значений в реальных приложениях. Например, если переменная представляет скорость автомобиля, можно установить максимальное возможное значение. Можно также ограничить переменные диапазоны, только если они вызывают слишком много оранжевых проверок от сверхприближения.
Анализ Программы автоматического доказательства Кода показывает все глобальные переменные, входные параметры функции и заблокированные функции, которые приводят к оранжевым проверкам от возможного сверхприближения. Можно ограничить только эти переменные для более точного анализа.
Программа автоматического доказательства Открытого кода приводит к пользовательскому интерфейсу Polyspace или Polyspace доступ к веб-интерфейсу.
Откройте панель Orange Sources. Выполнить одно из следующих действий:
Выберите оранжевую проверку. Если программное обеспечение может проследить оранжевую проверку до первопричины,
значок появляется на панели Result Details. Кликните по этому значку, чтобы открыть панель Orange Sources.
В пользовательском интерфейсе Polyspace выберите Window> Show/Hide View> Orange Sources. В Polyspace доступ к веб-интерфейсу выберите Layout> Show/Hide View> Orange Sources.
Вы видите полный список переменных (входные параметры функции или возвращаемые значения заблокированных функций), который может вызвать оранжевые проверки. Ограничьте области значений этих переменных.
С новыми представлениями кода вам придется задать дополнительные ограничения. Можно обновить существующий шаблон, чтобы добавить глобальные переменные, входные параметры функции и заблокированные функции, которые прибывают из новых представлений кода.
Кроме того, если вы удаляете некоторые переменные или функции из вашего кода, ограничения на них больше не применимы. Вместо того, чтобы регенерировать ограничительный шаблон и повторно задать ограничения, можно обновить существующий шаблон и удалить переменные, которые не присутствуют в коде.
На панели Configuration выберите Inputs & Stubbing.
Откройте существующий шаблон одним из следующих способов:
В поле Constraint setup введите путь к XML-файлу шаблона. Нажмите Edit.
Нажмите Edit. В диалоговом окне Constraint Specification кликните
по значку, чтобы перейти к вашему файлу шаблона.
Нажмите Update.
Переменные, которые больше не присутствуют в вашем исходном коде, появляются под узлом Non Applicable. Чтобы удалить запись под узлом Non Applicable или самим узлом, щелкните правой кнопкой и выберите Remove This Node.
Задайте свои новые ограничения для любой из других переменных.
В непрерывном рабочем процессе интегрирования можно использовать ограничительный XML-файл от предыдущего выполнения. Если новые представления кода требуют дополнительных ограничений:
Задайте ограничения на переменные из новых представлений кода в ограничительном XML-файле. Смотрите Создают Ограничительный Шаблон: Командная строка.
Объедините ограничительный XML-файл с новыми ограничениями и ограничительный XML-файл от предыдущего выполнения.
Определение ограничений вне вашего кода допускает более точный анализ. Однако необходимо использовать код в рамках заданных ограничений, потому что ограничения вне кода. В противном случае результаты не могут применяться. Например, если вы используете входные параметры функции вне своей заданной области значений, ошибка времени выполнения может произойти на операции даже при том, что начинает работу, операция являются зелеными.
Чтобы задать ограничения в вашем коде, можно использовать:
Соответствующая обработка ошибок тестирует в вашем коде.
Проверки Polyspace, чтобы определить, могут ли ошибки на самом деле произойти. Если они не происходят, тестовые блоки появляются как Unreachable code.
Макрос assert. Например, чтобы ограничить переменную var в области значений [0,10], можно использовать assert(var >= 0 && var <=10);.
Polyspace проверяет ваши операторы assert, чтобы видеть, может ли условие быть ложным. После оператора assert Polyspace полагает, что условие assert верно. Используя операторы assert, можно ограничить переменные для остающегося кода в том же осциллографе. Для примеров смотрите Assertion.
Constraint setup (-data-range-specifications)
