Для более точного Polyspace® анализ, можно задать ограничения на глобальные переменные, входные параметры функции и упрямые функции. Можно задать ограничения в пользовательском интерфейсе рабочего стола Polyspace продуктов или в командной строке в виде XML- файле. Общие рабочие процессы см. в разделе «Задание внешних ограничений».
В этом разделе описываются подробные сведения об ограничительной схеме XML- файле. Обычно эти сведения требуются только при создании ограничительного XML с нуля. Если вы запускаете верификацию один раз, программное обеспечение автоматически генерирует файл ограничения шаблона drs-template.xml в папке результатов. Вместо создания ограничительного XML- файл с нуля легче отредактировать этот шаблон XML- файл, чтобы задать ограничения. Для некоторых примеров смотрите:
Другое объяснение того, что означают теги XML, см. в разделе Внешние ограничения для анализа Polyspace.
Вы также можете увидеть информацию в этом разделе и базовую XML-схему в polyspaceroot\ polyspace\drspolyspacerootC:\Program Files\Polyspace\R2019a.
Файл ограничений содержит следующие элементы XML:
<global> element - Объявляет глобальные возможности и является корневым элементом XML- файлом.
<file> элемент - Объявляет возможности. Должно быть заключено в <global> элемент. Может содержать любую переменную или объявление функции. Статические переменные должны быть заключены в элемент файла, чтобы избежать конфликтов.
<scalar> элемент - Объявляет целое число или переменную с плавающей точкой. Может быть заключен в любой распознанный элемент, но не может окружать какой-либо элемент. Устанавливает init/permanent/global значения переменных.
<pointer> элемент - Объявляет переменную указателя. Может содержать любые другие объявления переменных (включая саму себя), для определения заостренных объектов. Задает, какое значение записывается в указатель (NULL или нет), сколько объектов выделено и как инициализируются заостренные объекты.
<array> элемент - Объявляет переменную массива. Может включать любое другое определение переменной (включая ее саму), чтобы задать представители массива.
<struct> элемент - Объявляет структурную переменную или объект (образец класса). Может содержать любое другое определение переменной (включая ее саму), для определения полей структуры.
<function> элемент - Объявляет возможности метода функции или класса. Может содержать любое определение переменной, чтобы задать аргументы и возврат значение функции. Аргументы должны быть именованы arg1, arg2, …argn и значение возврата должно называться return.
Следующие примечания относятся к конкретным полям в каждом элементе XML:
(*) - Поля, используемые только графический интерфейс пользователя. Эти поля не являются обязательными для верификации для принятия областей значений. Поле линия содержит номер линии, где переменная объявлена в исходном коде, complete_type содержит строку с полным типом переменной и base_type используется графический интерфейс пользователя для вычисления значений min и max. Комментарий поля используется для добавления информации о любом узле.
(* *) - Имя поля обязательно для элементов возможностей <file> и <function> (кроме указателей на функцию). Для других элементов имя должно быть задано при объявлении корневого символа или struct поле.
(* * *) - Если к переменной применяется несколько атрибутов, атрибуты должны быть разделены пространством. Только статический атрибут является обязательным, чтобы избежать конфликтов между статическими переменными с таким же именем. Атрибут может быть задан несколько раз без влияния.
(* * * *) - Этот элемент используется только графический интерфейс пользователя, чтобы определить, какой init разрешены режимы для текущего элемента (согласно его типу). Значение работает как маска, где добавляются следующие значения, чтобы указать, какие режимы разрешены:
1: Режим "NO"разрешено.
2 : Режим "INIT"разрешено.
4: Режим "PERMANENT"разрешено.
8: Режим "MAIN_GENERATOR"разрешено.
Для примера значение "10«означает, что режимы» INIT«и» MAIN_GENERATOR"разрешены. Чтобы увидеть, как это значение вычисляется, смотрите Допустимые режимы и Значения по умолчанию.
(* * * * *) - подэлемент массива указателя (т.е. заостренный объект) будет учитываться только в том случае, если init_pointed равно SINGLE, MULTI, SINGLE_CERTAIN_WRITE или MULTI_CERTAIN_WRITE.
(* * * * * *) - SINGLE_CERTAIN_WRITE или MULTI_CERTAIN_WRITE доступны для параметров и возвращаемых значений упрямых функций, только если они являются указателями. Если параметром или возвращаемым значением является структура, а у структуры есть поле указателя, они также доступны для поля указателя.
<file> Элемент| Область | Синтаксис |
|---|---|
name | filepath_or_filename |
comment | string |
<scalar> Элемент| Область | Синтаксис |
|---|---|
name (**) | name |
line (*) | line |
base_type (*) | intx
|
Attributes (***) | изменчивый |
complete_type (*) | type |
init_mode | MAIN_GENERATOR |
init_modes_allowed (*) | single value (****) |
init_range | range отключенный |
global_ assert | ДА |
assert_range | range отключенный |
comment(*) | string |
<pointer> Элемент| Область | Синтаксис |
|---|---|
Name (**) | name |
line (*) | line |
Attributes (***) | изменчивый |
complete_type (*) | type |
init_mode | MAIN_GENERATOR |
init_modes_allowed (*) | single value (****) |
initialize_ pointer | Могут быть: ПУСТОЙ УКАЗАТЕЛЬ |
number_ allocated | single value отключенный |
init_pointed (******) |
|
comment | string |
<array> и <struct> Элементы| Область | Синтаксис |
|---|---|
Name (**) | name |
line (*) | line |
complete_type (*) | type |
attributes (***) | изменчивый |
comment | string |
<function> Элемент| Область | Синтаксис |
|---|---|
Name (**) | name |
line (*) | line |
main_generator_called | MAIN_GENERATOR |
attributes (***) | статичный |
comment | string |
| Возможности | Напечатать | Режимы Init | Режим Гассерта | Инициализируйте указатель | Init выделен | Дефолт | |
|---|---|---|---|---|---|---|---|
| Глобальные переменные | Базовый тип | Неквалифицированный/ статический/ const скаляр | MAIN_ ГЕНЕРАТОР ПРОИГНОРИРОВАТЬ В этом ПОСТОЯННЫЙ | ДА НЕТ | Зависимый основной генератор | ||
| Летучий скаляр | ПОСТОЯННЫЙ | отключенный | ПОСТОЯННЫЕ мин. макс. | ||||
| Внешние скаляры | INIT PERMANT | ДА НЕТ | INIT min.. max | ||||
| Struct | Структурное поле | См. тип поля | |||||
| Массив | Элемент массива | См. тип элемента | |||||
| Глобальные переменные | Указатель | Неквалифицированный/ статический/ const скаляр | MAIN_ ГЕНЕРАТОР ПРОИГНОРИРОВАТЬ В этом | Может иметь значение NULL Не NULL ПУСТОЙ УКАЗАТЕЛЬ | Ничего Одинок МНОГО | Зависимый основной генератор | |
| Волатильный указатель | не- поддержанный | не- поддержанный | не- поддержанный | ||||
| Указатель на Экстерн | ПРОИГНОРИРОВАТЬ В этом | Может иметь значение NULL Не NULL ПУСТОЙ УКАЗАТЕЛЬ | Ничего Одинок МНОГО | INIT Может быть NULL max МНОГО | |||
| Остроконечный летучий скаляр | не- поддержанный | не- поддержанный | |||||
| Остроконечный экстерн скаляр | В этом | не- поддержанный | В этом min.. max | ||||
| Заострённые другие скаляры | MAIN_ ГЕНЕРАТОР В этом | не- поддержанный | MAIN_ ГЕНЕРАТОР иждивенец | ||||
| Указатель на точку | MAIN_ ГЕНЕРАТОР В этом | не- поддержанный | Может иметь значение NULL Не NULL ПУСТОЙ УКАЗАТЕЛЬ | Ничего Одинок МНОГО | MAIN_ ГЕНЕРАТОР иждивенец | ||
| Заостренная функция | не- поддержанный | не- поддержанный | |||||
| Параметры функции | Функция Userdef | Скалярные параметры | MAIN_ ГЕНЕРАТОР В этом | не- поддержанный | В этом min.. max | ||
| Параметры указателя | MAIN_ ГЕНЕРАТОР В этом | не- поддержанный | Может иметь значение NULL Не NULL ПУСТОЙ УКАЗАТЕЛЬ | Ничего Одинок МНОГО | INIT Может быть NULL max МНОГО | ||
| Другие параметры | См. тип параметра | ||||||
| Упрямая функция | Скалярный параметр | отключенный | не- поддержанный | ||||
| Параметры указателя | отключенный | отключенный | Ничего Одинок МНОГО SINGLE_CERTAIN_WRITE MULTI_CERTAIN_WRITE | МНОГО | |||
| Заостренные параметры | ПОСТОЯННЫЙ | не- поддержанный | ПОСТОЯННЫЙ min.. max | ||||
| Параметры Pointed const | отключенный | не- поддержанный | |||||
| Возврат функции | Функция Userdef | Вернуть | отключенный | не- поддержанный | отключенный | отключенный | |
| Упрямая функция | Скалярный возврат | ПОСТОЯННЫЙ | не- поддержанный | ПОСТОЯННЫЙ min.. max | |||
| Возврат указателя | ПОСТОЯННЫЙ | не- поддержанный | Может иметь значение NULL Не NULL ПУСТОЙ УКАЗАТЕЛЬ | Ничего Одинок МНОГО SINGLE_CERTAIN_WRITE MULTI_CERTAIN_WRITE | ПОСТОЯННЫЙ Может быть NULL MAX MULTI | ||