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