Для более точного анализа Polyspace® можно задать ограничения на глобальные переменные, входные параметры функции и заблокированные функции. Можно задать ограничения в пользовательском интерфейсе десктопных решений Polyspace или в командной строке как XML-файл. Для общего рабочего процесса смотрите, Задают Внешние Ограничения.
Эта тема описывает детали ограничительной схемы XML-файла. Вы обычно запрашиваете эту информацию, только если вы создаете ограничение XML с нуля. Если при запуске верификацию однажды, программное обеспечение автоматически генерирует ограничительный файл шаблона drs-template.xml в вашей папке результатов. Вместо того, чтобы создать ограничительный XML-файл с нуля, легче отредактировать этот XML-файл шаблона, чтобы задать ваши ограничения. Для некоторых примеров см.:
Ограничьте область значений глобальной переменной (Polyspace Code Prover)
Ограничьте входные параметры функции (Polyspace Code Prover)
Для другого объяснения какой среднее значение XML-тэгов, смотрите Внешние Ограничения для Анализа Polyspace.
Можно также видеть информацию в этой теме и базовую XML-схему в polyspaceroot\polyspace\drspolyspacerootC:\Program Files\Polyspace\R2019a.
Ограничительный файл содержит следующие элементы XML:
<global> элемент — Объявляет глобальную область видимости и является корневым элементом XML-файла.
<file> элемент — Объявляет осциллограф файла. Должен быть заключен в <global> элемент. Может заключить любое объявление переменной или объявление функции. Статические переменные должны быть заключены в элемент файла, чтобы избежать конфликтов.
<scalar> элемент — Объявляет целое число или переменную с плавающей точкой. Может быть заключен в любой распознанный элемент, но не может заключить элемент. Наборы init/permanent/global утверждают на переменных.
<pointer> элемент — Объявляет переменную указателя. Может заключить любые другие объявления переменной (включая себя), чтобы задать резкие объекты. Задает то, какое значение записано в указатель (NULL или не), сколько объектов выделяется и как резкие объекты инициализируются.
<array> элемент — Объявляет переменную типа массив. Может заключить любое другое определение переменной (включая себя), чтобы задать члены массива.
<struct> элемент — Объявляет переменную структуры или объект (экземпляр класса). Может заключить любое другое определение переменной (включая себя), чтобы задать поля структуры.
<function> элемент — Объявляет осциллограф функционального или метода класса. Может заключить любое определение переменной, чтобы задать аргументы и возвращаемое значение функции. Аргументы нужно назвать arg1, arg2, …argn и возвращаемое значение должно быть названо return.
Следующие примечания применяются к определенным полям в каждом элементе XML:
(*) — Поля, используемые только графический интерфейсом пользователя. Эти поля не обязательны для верификации, чтобы принять области значений. Полевая линия содержит номер строки, где переменная объявляется в исходном коде, complete_type содержит строку с полным типом переменной и base_type используется графический интерфейсом пользователя, чтобы вычислить min и макс. значения. Полевой комментарий используется, чтобы добавить информацию о любом узле.
(**) — имя поля обязательно для элементов осциллографа <file> and <function> (за исключением указателей функции). Для других элементов имя должно быть задано при объявлении корневого символа или struct поле .
(***) — Если больше чем один атрибут применяется к переменной, атрибуты должны быть разделены пробелом. Только статический атрибут обязателен, чтобы избежать конфликтов между статическими переменными, имеющими то же имя. Атрибут может быть задан многократно без удара.
(****) — Этот элемент используется только графический интерфейсом пользователя, чтобы определить который init режимы позволены для текущего элемента (согласно его типу). Значение работает маской, где следующие значения добавляются, чтобы задать, какие режимы позволены:
1: Режим “NO” позволен.
2 : Режим “INIT” позволен.
4: Режим “PERMANENT” позволен.
8: Режим “MAIN_GENERATOR” позволен.
Например, значение “10” означает тот режимы “INIT” и “MAIN_GENERATOR” позволены. Чтобы видеть, как это значение вычисляется, обратитесь к Допустимым Режимам и Значениям по умолчанию.
(*****) — Указатель подэлемента массива (т.е. резкий объект) будет учтен только если init_pointed равно ОДНОМУ, 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> and <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 | Режим Gassert | Инициализируйте указатель | Init выделяется | Значение по умолчанию | |
|---|---|---|---|---|---|---|---|
| Глобальные переменные | Базовый тип | Дисквалифицированный / статический / const скаляр | MAIN_ ГЕНЕРАТОР ПРОИГНОРИРОВАТЬ INIT ПОСТОЯННЫЙ | ДА НЕТ | Основной зависимый генератора | ||
| Энергозависимый скаляр | ПОСТОЯННЫЙ | отключенный | Min PERMANENT макс. | ||||
| Скаляр экстерна | ПОСТОЯННЫЙ INIT | ДА НЕТ | Min INIT макс. | ||||
| Struct () | Поле Struct | Обратитесь к типу поля | |||||
| Массив | Элемент массива | Обратитесь к типу элемента | |||||
| Глобальные переменные | Указатель | Дисквалифицированный / статический / const скаляр | MAIN_ ГЕНЕРАТОР ПРОИГНОРИРОВАТЬ INIT | Может быть NULL Не ПУСТОЙ Пустой указатель | 'none' Единственный МНОГО | Основной зависимый генератора | |
| Энергозависимый указатель | не- поддерживаемый | не- поддерживаемый | не- поддерживаемый | ||||
| Указатель экстерна | ПРОИГНОРИРОВАТЬ INIT | Может быть NULL Не ПУСТОЙ Пустой указатель | 'none' Единственный МНОГО | INIT Может быть NULL макс. МНОГО | |||
| Резкий энергозависимый скаляр | не- поддерживаемый | не- поддерживаемый | |||||
| Резкий скаляр экстерна | INIT | не- поддерживаемый | INIT min.. | ||||
| Указанные другие скаляры | MAIN_ ГЕНЕРАТОР INIT | не- поддерживаемый | MAIN_ ГЕНЕРАТОР зависимый | ||||
| Резкий указатель | MAIN_ ГЕНЕРАТОР INIT/ | не- поддерживаемый | Может быть NULL Не ПУСТОЙ Пустой указатель | 'none' Единственный МНОГО | MAIN_ ГЕНЕРАТОР зависимый | ||
| Резкая функция | не- поддерживаемый | не- поддерживаемый | |||||
| Параметры функции | Функция Userdef | Скалярные параметры | MAIN_ ГЕНЕРАТОР INIT | не- поддерживаемый | INIT min.. | ||
| Параметры указателя | MAIN_ ГЕНЕРАТОР INIT | не- поддерживаемый | Может быть NULL Не ПУСТОЙ Пустой указатель | 'none' Единственный МНОГО | INIT Может быть NULL макс. МНОГО | ||
| Другие параметры | Обратитесь к типу параметра | ||||||
| Заблокированная функция | Скалярный параметр | отключенный | не- поддерживаемый | ||||
| Параметры указателя | отключенный | отключенный | 'none' Единственный МНОГО SINGLE_CERTAIN_WRITE MULTI_CERTAIN_WRITE | МНОГО | |||
| Резкие параметры | ПОСТОЯННЫЙ | не- поддерживаемый | ПОСТОЯННЫЙ min.. | ||||
| Резкие параметры const | отключенный | не- поддерживаемый | |||||
| Функциональный возврат | Функция Userdef | Возврат | отключенный | не- поддерживаемый | отключенный | отключенный | |
| Заблокированная функция | Скалярный возврат | ПОСТОЯННЫЙ | не- поддерживаемый | ПОСТОЯННЫЙ min.. | |||
| Указатель возвращается | ПОСТОЯННЫЙ | не- поддерживаемый | Может быть NULL Не ПУСТОЙ Пустой указатель | 'none' Единственный МНОГО SINGLE_CERTAIN_WRITE MULTI_CERTAIN_WRITE | ПОСТОЯННЫЙ Может быть NULL макс. MULTI | ||