コード動作仕様を使用して Code Prover の実行時チェックを変更する
Polyspace® Code Prover™ は C/C++ コードのランタイム エラーを網羅的にチェックします。解析の精度を向上させるため、コード外の追加情報を提供することもできます。
オプション -code-behavior-specifications を使用してほとんどの外部情報を指定できます。このオプションを使用して、動作をコード内の要素に関連付けることができます。たとえば、カスタム ライブラリ関数を標準関数にマッピングしたり、関数がメモリ管理関数として機能することを指定したりできます。このオプションは、次のいずれかの形式のファイルを引数として取ります。
XML
Datalog
Polyspace Code Prover に適用されるのは XML 形式のみです。このトピックでは、サポートされるチェック変更について説明します。実行時チェックを変更できるすべてのオプションのリストは、Code Prover の実行時チェックの変更または無効化を参照してください。
コード動作仕様 XML ファイルは、特定の動作を関数に関連付けます (または動作をグローバル スコープで定義します)。次のセクションで、Code Prover 解析に関連する動作のリストを示します。Bug Finder に関連する動作については、Modify Bug Finder Checkers Through Code Behavior Specificationsを参照してください。
サポートされる動作を Polyspace インストールで提供されるサンプル テンプレート ファイル code-behavior-specifications-template.xml で確認することもできます。このファイルは polyspaceroot\polyspace\verifier\cxx\polyspaceroot
精度向上のための標準関数へのマッピング
XML 構文:
<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
<functions>
<function name="custom_function" std="std_function">
</function>
</functions>
</specifications>XML ファイルでこのエントリを使用すると、関数の Code Prover 解析の精度が低いことによるオレンジ チェックの数 (または、Bug Finder 解析の精度が低いことによる偽陰性の数) が減少します。場合によっては、静的検証固有の制限により、検証では特定の種類の関数が正確に解析されないことがあります。そのような場合、独自の関数によく似た標準関数があれば、このマッピングを使用します。独自の関数自体は解析されませんが、その関数を呼び出す位置での解析精度が上がります。たとえば、検証では独自の関数 cos32 の解析精度が低く、戻り値の全範囲を考慮する場合、戻り値の範囲 [-1,1] について関数 cos にマップします。
検証では、関数本体は無視されます。ただし、検証では、次の方法で関数の動作がエミュレートされます。
検証では、関数と標準関数の戻り値は同じであると仮定されます。
たとえば、関数
cos32を標準関数cosにマップする場合、検証ではcos32が [-1,1] の値を返すと仮定されます。検証では、標準関数を使用してチェックするのと同じ問題がチェックされます。
たとえば、関数
acos32を標準関数acosにマップする場合、[標準ライブラリ ルーチンの無効な使用]チェックでは、acos32の引数が [-1,1] に含まれるかどうかが判断されます。
マップできる関数には、以下が含まれます。
math.hの標準ライブラリ関数。string.hのメモリ管理関数。__ps_meminit:Polyspace 固有の、メモリ領域初期化関数。場合によっては、検証ではメモリ初期化関数が認識されず、この関数を使って初期化した変数に
[未初期化ローカル変数]オレンジ チェックが生成されることがあります。メモリ初期化関数がメモリ アドレスを使って変数を初期化することがわかっている場合、関数を__ps_meminitにマップします。チェックはグリーンに変わります。__ps_lookup_table_clip:Polyspace 固有の、入力配列の範囲内の値を返す関数。場合によっては、検証では、大きな配列の値を調べる関数 (ルックアップ テーブル関数) の戻り値に全範囲の値が返されると見なされます。ルックアップ テーブル関数の戻り値が入力配列の範囲内の値にならなければならないことがわかっている場合、関数を
__ps_lookup_table_clipにマップします。モデル生成コードの場合、検証は既定で、ルックアップ テーブル関数に対してこの仮定が行われます。ルックアップ テーブルが線形内挿あり、外挿なしを使用しているかどうかを特定するために、検証では関数名が使用されます。たとえば、C/C++ S-Function (Simulink) ブロック内の関数など、手書きの関数でのみマッピングを使用します。これらの関数の名前は特定の規則に従いません。これらは明示的に指定しなければなりません。
同時実行検出のための標準関数へのマッピング
XML 構文:
<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
<functions>
<function name="custom_function" std="std_function">
</function>
</functions>
</specifications>スレッド作成関数およびクリティカル セクションを開始、終了する関数を自動検出する場合、XML ファイルでこのエントリを使用します。Polyspace は、マルチタスキング プリミティブの特定ファミリのみの自動検出をサポートします。この XML エントリを使用してサポートを拡張します。
たとえば、スレッド作成関数がサポート対象ファミリのいずれにも属さない場合、関数をサポート対象の同時実行プリミティブにマッピングします。
初期化チェックの拡張
XML 構文:
<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
<functions>
<function name="my_func">
<check name=name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="n"/>
</function>
</functions>
</specifications>関数 my_funcn
スタブ関数からのスタック サイズへの寄与の指定
XML 構文:
<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
<functions>
<function name="my_func">
<behavior name="STACK_SIZE_LOCAL_VARIABLES" value="size"/>
</function>
</functions>
</specifications>XML ファイルのこのエントリを使用して、関数 my_funcsizemy_func
固定サイズの代わりに、関数からのスタック サイズ寄与の下限と上限を指定することもできます。次のように、value 属性にローカル変数の最小サイズ min_sizemax_size
<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
<functions>
<function name="my_func">
<behavior name="STACK_SIZE_LOCAL_VARIABLES" value="min_size,max_size"/>
</function>
</functions>
</specifications>テンプレート関数の場合、インスタンス化されたすべての関数から同じスタック サイズ寄与を指定する必要があります。別のインスタンス化に対して別の値を指定することはできません。
