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