Polyspace 解析制約の XML ファイル形式

Polyspace® 解析の精度を高めるために、グローバル変数、関数入力、およびスタブ関数に制約を指定できます。Polyspace デスクトップ製品のユーザー インターフェイスまたはコマンド ラインで、制約を XML ファイルとして指定できます。一般的なワークフローについては、Polyspace 解析の外的制約の指定を参照してください。

このトピックでは、制約 XML ファイルのスキーマの詳細について説明します。通常、この情報は制約 XML をゼロから作成する場合にのみ必要です。検証を一度実行すると、ソフトウェアによって自動的に結果フォルダーにテンプレート制約ファイル drs-template.xml が生成されます。制約 XML ファイルをゼロから作成する代わりに、このテンプレート XML ファイルを編集すると制約をより簡単に指定できます。例については、次を参照してください。

XML タグの意味についての別の説明は、Polyspace 解析の外的制約を参照してください。

また、このトピックの情報や polyspaceroot\polyspace\drs の基となる XML スキーマを確認することもできます。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2019a です。

構文説明 — XML 要素

制約ファイルには、以下の XML 要素が含まれます。

  • <global> 要素 — グローバル スコープを宣言します。XML ファイルのルート要素です。

  • <file> 要素 — ファイル スコープを宣言します。<global> 要素で囲まれていなければなりません。任意の変数または関数宣言を囲むことができます。競合を防ぐため、静的変数は file 要素で囲まなければなりません。

  • <scalar> 要素— 整数または浮動小数点の変数を宣言します。認識される任意の要素で囲まれる場合がありますが、いずれの要素も囲むことはできません。初期、永続、グローバルのアサートを変数に設定します。

  • <pointer> 要素 — ポインター変数を宣言します。他の任意の変数宣言 (この要素自体も含む) を囲み、参照されるオブジェクトを定義できます。ポインターに書き込む値 (NULL またはそれ以外)、割り当てられるオブジェクトの個数、参照されるオブジェクトの初期化方法を指定します。

  • <array> 要素 — 配列変数を宣言します。他の任意の変数定義 (この要素自体も含む) を囲み、配列のメンバーを定義できます。

  • <struct> 要素 — 構造体変数またはオブジェクト (クラスのインスタンス) を宣言します。他の任意の変数定義 (この要素自体も含む) を囲み、構造体のフィールドを定義できます。

  • <function> 要素 — 関数またはクラス メソッドのスコープを宣言します。任意の変数定義を囲み、関数の引数と戻り値を定義できます。引数は、arg1, arg2, …argn と指定します。戻り値は、return を呼び出す必要があります。

各 XML 要素内の特定のフィールドについては、以下の注意事項があります。

  • (*) — フィールドは、GUI によってのみ使用されます。これらのフィールドについて、検証が範囲を受け入れることは必須ではありません。フィールド line には、ソース コード内で変数が宣言されている場所の行番号が含まれます。complete_type には、完全な変数型の文字列が含まれます。base_type は、GUI で最小値と最大値を計算するために使用されます。フィールド comment は、任意のノードについて情報を追加するために使用します。

  • (**) — フィールド name は、スコープ要素 <file> および <function> (関数ポインターを除く) の場合は必須です。他の要素の場合、name は、ルート シンボルまたは struct フィールドを宣言する場合に指定しなければなりません。

  • (***) — 複数の属性を変数に適用する場合、各属性はスペースで区切らなければなりません。static 属性のみ必須です。これは、名前が同じ複数の静的変数についての競合を避けるためです。1 つの属性を複数回定義しても影響はありません。

  • (****) — この要素は 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> 要素

フィールド構文
namefilepath_or_filename
commentstring

<scalar> 要素

フィールド構文
name (**)name
line (*)line
base_type (*) intx
uintx
floatx
Attributes (***)volatile
extern
static
const
complete_type (*) type
init_mode MAIN_GENERATOR
IGNORE
INIT
PERMANENT
disabled
unsupported
init_modes_allowed (*)single value (****)
init_range range
disabled
unsupported
global_ assert YES
NO
disabled
unsupported
assert_rangerange
disabled
unsupported
comment(*)string

<pointer> 要素

フィールド構文
Name (**) name
line (*) line
Attributes (***)volatile
extern
static
const
complete_type (*)type
init_mode MAIN_GENERATOR
IGNORE
INIT
PERMANENT
disabled
unsupported
init_modes_allowed (*)single value (****)
initialize_ pointer以下が可能です。
NULL
Not NULL
NULL
number_ allocatedsingle value
disabled
unsupported
init_pointed (******)

MAIN_GENERATOR

NONE

SINGLE

MULTI

SINGLE_CERTAIN_WRITE

MULTI_CERTAIN_WRITE

disabled

commentstring

<array> 要素および <struct> 要素

フィールド構文
Name (**) name
line (*) line
complete_type (*)type
attributes (***)volatile
extern
static
const
commentstring

<function> 要素

フィールド構文
Name (**) name
line (*) line
main_generator_calledMAIN_GENERATOR
YES
NO
disabled
attributes (***) static
extern
unused
commentstring

有効なモードと既定値

スコープタイプ 初期化モードGassert モードポインターの初期化初期化の割り当て既定の設定
グローバル変数基本データ型非修飾/
static/
const
スカラー		MAIN_
GENERATOR
IGNORE
INIT
YES
NO 		  main ジェネレーターに依存
PERMANENT 無効
Volatile スカラー PERMANENT無効  PERMANENT min..max
Extern スカラー INITYES
NO 		  INIT min..max
PERMANENT無効
structstruct のフィールドフィールドの型を参照
配列配列の要素要素の型を参照
グローバル変数ポインター非修飾/
static/
const
スカラー		MAIN_
GENERATOR
IGNORE
INIT 		 以下が可能です。NULL
Not NULL
NULL 		NONE
SINGLE
MULTI 		main ジェネレーターに依存
Volatile ポインターサポート
なし		 サポート
なし		サポート
なし		 
Extern ポインター IGNORE
INIT		 以下が可能です。NULL
Not NULL
NULL 		NONE
SINGLE
MULTI 		INIT は以下が可能です。
NULL max
MULTI
参照される volatile スカラーサポート
なし		サポート
なし		   
参照される extern スカラーINITサポート
なし		  INIT
min..max
参照されるその他のスカラーMAIN_
GENERATOR
INIT		サポート
なし		  MAIN_
GENERATOR
依存
参照されるポインターMAIN_
GENERATOR
INIT/ 		サポート
なし		以下が可能です。NULL
Not NULL
NULL 		NONE
SINGLE
MULTI 		MAIN_
GENERATOR
依存
参照される関数サポート
なし		サポート
なし		   
関数パラメーターUserdef (ユーザー定義) 関数スカラー パラメーターMAIN_
GENERATOR
INIT		サポート
なし		  INIT
min..max
ポインター パラメーターMAIN_
GENERATOR
INIT		サポート
なし		以下が可能です。NULL
Not NULL
NULL 		NONE
SINGLE
MULTI 		INIT は以下が可能です。
NULL max
MULTI
その他のパラメーターパラメーター タイプを参照
スタブ関数スカラー パラメーター 無効サポート
なし		   
ポインター パラメーター 無効 無効

NONE

SINGLE

MULTI

SINGLE_CERTAIN_WRITE

MULTI_CERTAIN_WRITE

MULTI
参照されるパラメーターPERMANENTサポート
なし		  PERMANENT
min..max
参照される定数パラメーター無効サポート
なし		   
関数の戻り値Userdef (ユーザー定義) 関数戻り値無効サポート
なし		無効無効 
スタブ関数スカラーの戻り値PERMANENTサポート
なし		  PERMANENT
min..max
ポインターの戻り値PERMANENTサポート
なし		以下が可能です。NULL
Not NULL
NULL

NONE

SINGLE

MULTI

SINGLE_CERTAIN_WRITE

MULTI_CERTAIN_WRITE

PERMANENT
以下が可能です。 NULL 最大値 MULTI

参考

トピック