Формат файлов XML для ограничений

Для более точного анализа Polyspace® можно задать ограничения на глобальные переменные, входные параметры функции и заблокированные функции. Можно задать ограничения в пользовательском интерфейсе десктопных решений Polyspace или в командной строке как XML-файл. Для общего рабочего процесса смотрите, Задают Внешние Ограничения.

Эта тема описывает детали ограничительной схемы XML-файла. Вы обычно запрашиваете эту информацию, только если вы создаете ограничение XML с нуля. Если при запуске верификацию однажды, программное обеспечение автоматически генерирует ограничительный файл шаблона drs-template.xml в вашей папке результатов. Вместо того, чтобы создать ограничительный XML-файл с нуля, легче отредактировать этот XML-файл шаблона, чтобы задать ваши ограничения. Для некоторых примеров см.:

Для другого объяснения какой среднее значение XML-тэгов, смотрите Внешние Ограничения для Анализа Polyspace.

Можно также видеть информацию в этой теме и базовую XML-схему в polyspaceroot\polyspace\drs. Здесь, polyspaceroot папка установки Polyspace, например, C:\Program Files\Polyspace\R2019a.

Описание синтаксиса — элементы XML

Ограничительный файл содержит следующие элементы 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> Элемент

Поле Синтаксис
namefilepath_or_filename
commentstring

<scalar> Элемент

Поле Синтаксис
name (**)name
line (*)line
base_type (*) intx
uintx
floatx
Attributes (***)энергозависимый
экстерн
статический
const
complete_type (*) type
init_mode MAIN_GENERATOR
ПРОИГНОРИРОВАТЬ
INIT
ПОСТОЯННЫЙ
отключенный
неподдерживаемый
init_modes_allowed (*)single value (****)
init_range range
отключенный
неподдерживаемый
global_ assert ДА
НЕТ
отключенный
неподдерживаемый
assert_rangerange
отключенный
неподдерживаемый
comment(*)string

<pointer> Элемент

Поле Синтаксис
Name (**) name
line (*) line
Attributes (***)энергозависимый
экстерн
статический
const
complete_type (*)type
init_mode MAIN_GENERATOR
ПРОИГНОРИРОВАТЬ
INIT
ПОСТОЯННЫЙ
отключенный
неподдерживаемый
init_modes_allowed (*)single value (****)
initialize_ pointerМожет быть:
Пустой указатель
Не ПУСТОЙ
Пустой указатель
number_ allocatedsingle value
отключенный
неподдерживаемый
init_pointed (******)

MAIN_GENERATOR

NONE

SINGLE

MULTI

SINGLE_CERTAIN_WRITE

MULTI_CERTAIN_WRITE

disabled

commentstring

<array> and <struct> Элементы

Поле Синтаксис
Name (**) name
line (*) line
complete_type (*)type
attributes (***)энергозависимый
экстерн
статический
const
commentstring

<function> Элемент

Поле Синтаксис
Name (**) name
line (*) line
main_generator_calledMAIN_GENERATOR
ДА
НЕТ
отключенный
attributes (***) статический
экстерн
неиспользованный
commentstring

Допустимые режимы и значения по умолчанию

ОсциллографВвод Режимы 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

Похожие темы