В этом примере показано, как задать ограничения (также известный как технические требования области значений данных или DRS) на переменных в вашем коде. Polyspace® использует код, который вы предоставляете, чтобы сделать предположения об элементах, таких как переменные диапазоны и позволенный buffer size для указателей. Иногда предположения более широки, чем, что вы ожидаете потому что:
Вы не предоставили полный код. Например, вы не предоставляли некоторые функциональные определения.
Часть информации о переменных доступна только во время выполнения. Например, некоторые переменные в вашем коде получают значения от пользователя во время выполнения.
Из-за этих широких предположений:
Code Prover может рассмотреть больше путей к выполнению, чем те пути, которые происходят во время выполнения. Если операция перестала работать вдоль одного из путей к выполнению, Polyspace помещает оранжевую проверку в операцию. Если тот путь к выполнению прибывает из предположения, которое слишком широко, оранжевая проверка может указать на положительную ложь.
Bug Finder может иногда производить ложные положительные стороны.
Чтобы сократить количество таких ложных положительных сторон, можно задать дополнительные ограничения на глобальные переменные, входные параметры функции, и возвращаемые значения и модифицируемые аргументы заблокированных функций. Вы сохраняете ограничения как XML-файл, чтобы использовать их для последующих исследований. Если ваш исходный код изменяется, можно обновить предыдущие ограничения. Вы не должны создавать новый ограничительный шаблон.
Примечание
В Bug Finder можно только ограничить глобальные переменные. Вы не можете ограничить входные параметры функции или возвращаемые значения заблокированных функций.
Откройте настройку проекта. На панели 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. Шаблон перечисляет все глобальные переменные, входные параметры функции и модифицируемые аргументы и возвращаемые значения заблокированных функций, не задавая ограничений на них.
Чтобы создать пустой шаблон, запустите анализ только до фазы компиляции. В Bug Finder отключите проверку дефектов. Используйте опцию Find defects (-checkers). В Code Prover проверяйте на исходную податливость только. Используйте аргумент compile для опции Verification level (-to). После анализа, пустого шаблона XML drs-template.xml создается в папке результатов.
Для проектов C++, чтобы создать пустой ограничительный шаблон, необходимо использовать аргумент cpp-normalize для опции Verification level (-to).
Отредактируйте XML-файл, чтобы задать ваши ограничения.
Для примеров см.:
Можно ограничить переменные диапазоны на основе их ожидаемой области значений в реальных приложениях. Например, если переменная представляет скорость транспортного средства, можно установить максимальное возможное значение. Можно также ограничить переменные диапазоны, только если они вызывают слишком много оранжевых проверок от сверхприближения.
Анализ Code Prover показывает все глобальные переменные, входные параметры функции и заблокированные функции, которые приводят к оранжевым проверкам от возможного сверхприближения. Можно ограничить только эти переменные для более точного анализа.
Программа автоматического доказательства Открытого кода приводит к пользовательскому интерфейсу Polyspace или Polyspace доступ к веб-интерфейсу.
Откройте панель Orange Sources. Выполнить одно из следующих действий:
Выберите оранжевую проверку. Если программное обеспечение может проследить оранжевую проверку до первопричины,
значок появляется на панели Result Details. Кликните по этому значку, чтобы открыть панель Orange Sources.
В пользовательском интерфейсе Polyspace выберите Window> Show/Hide View> Orange Sources. В Polyspace доступ к веб-интерфейсу выберите Window> Orange Sources.
Вы видите полный список переменных (входные параметры функции или возвращаемые значения заблокированных функций), который может вызвать оранжевые проверки. Ограничьте области значений этих переменных.
В деталях для отдельных оранжевых проверок вы часто видите сообщение, похожее на это:
If appropriate, applying DRS to stubbed function random_float in example.c line 44 may remove this orange.
Сообщение является индикацией, что заблокированная функция является возможным источником оранжевой проверки. Можно применить внешние ограничения на функцию, чтобы осуществить более точные предположения и возможно удалить оранжевую проверку (в случае, если это прибыло из более широких предположений).
С новыми представлениями кода вам придется задать дополнительные ограничения. Можно обновить существующий шаблон, чтобы добавить глобальные переменные, входные параметры функции и заблокированные функции, которые прибывают из новых представлений кода.
Кроме того, если вы удаляете некоторые переменные или функции из вашего кода, ограничения на них больше не применимы. Вместо того, чтобы регенерировать ограничительный шаблон и повторно задать ограничения, можно обновить существующий шаблон и удалить переменные, которые не присутствуют в коде.
На панели 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 операторы, можно ограничить переменные для остающегося кода в том же осциллографе. Для примеров смотрите User assertion.
Constraint setup (-data-range-specifications)
