В этом примере показано, как задать ограничения (также известные как спецификации диапазона данных или DRS) для переменных в коде. Polyspace ® использует предоставленный код, чтобы сделать допущения относительно таких элементов, как диапазоны переменных и допустимый размер буфера для указателей. Иногда предположения шире, чем вы ожидаете, потому что:
Вы не предоставили полный код. Например, некоторые определения функций не были предоставлены.
Некоторая информация о переменных доступна только во время выполнения. Например, некоторые переменные в коде получают значения от пользователя во время выполнения.
Из-за этих широких предположений:
Программа проверки кода может учитывать больше путей выполнения, чем те, которые происходят во время выполнения. Если операция завершается неуспешно по одному из путей выполнения, Polyspace выполняет проверку операции оранжевым цветом. Если этот путь выполнения исходит из слишком широкого предположения, оранжевая проверка может указывать на ложное положительное значение.
Иногда Bug Finder может создавать ложные положительные результаты.
Чтобы уменьшить число таких ложных срабатываний, можно задать дополнительные ограничения на глобальные переменные, входы функций и возвращаемые значения и изменяемые аргументы упорных функций. Ограничения сохраняются в виде XML-файла для последующего анализа. При изменении исходного кода можно обновить предыдущие ограничения. Создавать новый шаблон ограничения не требуется.
Примечание
В Bug Finder можно ограничить только глобальные переменные. Нельзя ограничить входы функций или возвращать значения упорных функций.
Откройте конфигурацию проекта. На панели Конфигурация (Configuration) выберите Входы и заглушки (Inputs & Stubbing).
Справа от пункта Настройка ограничения (Constraint setup) нажмите кнопку Править (Edit), чтобы открыть окно Спецификация ограничения (Constraint Specification).
В диалоговом окне Спецификация ограничения (Constraint Specification) создайте пустой шаблон ограничения. Шаблон содержит список всех переменных, для которых можно задать ограничения. Чтобы создать новый шаблон, нажмите кнопку. 
Программа компилирует проект и создает шаблон. Новый шаблон сохраняется в файле Module_number_Project_name_drs_template.xml
Укажите ограничения и сохраните шаблон в виде XML-файла. Дополнительные сведения см. в разделе Внешние зависимости для анализа в пространстве.
Нажмите кнопку ОК.
Полный путь к XML-файлу шаблона отображается в поле Настройка ограничения. При выполнении анализа 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-файл, чтобы указать ограничения.
Примеры см. в разделе:
Можно ограничить диапазоны переменных на основе их ожидаемого диапазона в реальных приложениях. Например, если переменная представляет скорость транспортного средства, можно задать максимально возможное значение. Можно также ограничить диапазоны переменных, только если они вызывают слишком много оранжевых проверок из-за чрезмерного приближения.
Анализ Prover кода показывает все глобальные переменные, входы функций и упорные функции, которые приводят к оранжевым проверкам от возможного чрезмерного приближения. Для более точного анализа можно ограничить только эти переменные.
Результаты программы Open Code Prover можно найти в интерфейсе пользователя Polyspace или веб-интерфейсе Polyspace Access.
Откройте панель «Оранжевые источники». Выполните одно из следующих действий:
Выберите оранжевый чек. Если программа может отследить оранжевую проверку по основной причине, на
панели Сведения о результате (Result Details) появится значок. Щелкните этот значок, чтобы открыть панель Оранжевые источники.
В интерфейсе пользователя Polyspace выберите «Окно» > «Показать/скрыть вид» > «Оранжевые источники». В веб-интерфейсе Polyspace Access выберите «Макет» > «Показать/скрыть вид» > «Оранжевые источники».
Появится полный список переменных (входы функций или возвращаемые значения упорных функций), которые могут вызвать проверку оранжевого цвета. Ограничение диапазонов этих переменных.
В подробных данных отдельных оранжевых чеков часто появляется сообщение, подобное следующему:
If appropriate, applying DRS to stubbed function random_float in example.c line 44 may remove this orange.
Сообщение указывает на то, что упрямая функция является возможным источником оранжевого чека. Можно применить внешние ограничения к функции, чтобы обеспечить более точные допущения и, возможно, удалить оранжевый чек (в случае, если это произошло из более широких допущений).
При новых представлениях кода может потребоваться указать дополнительные ограничения. Можно обновить существующий шаблон, чтобы добавить глобальные переменные, входы функций и упорные функции, которые получены из новых представлений кода.
Кроме того, при удалении некоторых переменных или функций из кода ограничения на них больше не применяются. Вместо регенерации шаблона ограничения и повторного определения ограничений можно обновить существующий шаблон и удалить переменные, отсутствующие в коде.
На панели Конфигурация (Configuration) выберите Входы и заглушки (Inputs & Stubbing).
Откройте существующий шаблон одним из следующих способов.
В поле Настройка ограничения введите путь к XML-файлу шаблона. Нажмите кнопку Изменить.
Нажмите кнопку Изменить. В диалоговом окне Спецификация ограничений (Constraint Specification) щелкните
значок, чтобы перейти к файлу шаблона.
Щелкните Обновить (Update).
Переменные, которые больше не присутствуют в исходном коде, отображаются в узле «Неприменимо». Чтобы удалить запись в узле Неприменимо или в самом узле, щелкните правой кнопкой мыши и выберите Удалить этот узел.
Укажите новые ограничения для любых других переменных.
В непрерывном рабочем процессе интеграции можно использовать XML-файл ограничений из предыдущего прогона. Если представление нового кода требует дополнительных ограничений:
Укажите ограничения для переменных из новых представлений кода в XML-файле ограничений. См. раздел Создание шаблона зависимости: Командная строка.
Объедините XML-файл ограничений с новыми ограничениями и XML-файл ограничений из предыдущего прогона.
Указание ограничений вне кода позволяет выполнять более точный анализ. Однако необходимо использовать код в пределах указанных ограничений, поскольку эти ограничения находятся вне кода. В противном случае результаты могут не применяться. Например, если используются функциональные входы вне заданного диапазона, во время выполнения операции может возникнуть ошибка, даже если проверки операции зеленые.
Для указания ограничений в коде можно использовать:
Соответствующие тесты обработки ошибок в коде.
Полиспейс проверяет, действительно ли могут возникнуть ошибки. Если они не возникают, тестовые блоки отображаются как недостижимый код.
assert макро. Например, для ограничения переменной var в диапазоне [0,10], можно использовать assert(var >= 0 && var <=10);.
Polyspace проверяет ваш assert инструкции, чтобы проверить, может ли условие быть ложным. После assert заявление, Polyspace считает, что assert условие истинно. Используя assert , можно ограничить переменные для оставшегося кода в той же области. Примеры см. в разделе User assertion.
Constraint setup (-data-range-specifications)