標準ライブラリ関数用の Bug Finder チェッカーのカスタム ライブラリへの拡張
このトピックでは、カスタム ライブラリ関数を標準ライブラリ内の同等の関数にマッピングすることによって、カスタム ライブラリ関数用のチェッカーを作成する方法を説明します。
チェッカーの拡張が必要かどうかの特定
標準ライブラリ関数に適用され、カスタム ライブラリ関数に拡張可能な Bug Finder チェッカーを特定する場合に、この手法を使用します。
たとえば、標準ライブラリの数学関数と同じ定義域をもつ数学関数を定義する場合を考えます。Bug Finder が標準ライブラリ関数の使用時に定義域エラーをチェックする場合は、同等のカスタム関数に対しても同じチェックを実行できます。
範囲 [-1,1] の値を想定している関数 acos32 を定義するものとします。次のようなコード スニペットで、実行時に関数の引数がこの範囲から外れるかどうかを検出することができます。
#include<math.h>
#include<float.h>
double acos32(double);
const int periodicity = 1.0;
int isItPeriodic() {
return(abs(func(0.5) - func(0.5 + periodicity)) < DBL_MIN);
}
double func(double val) {
return acos32(val);
}acos32 への引数の 1 つが許可されている定義域から外れています。acos32 の実装を指定しなかった場合や acos32 実装の解析が正確でない場合は、Bug Finder が問題を検出しない可能性があります。ただし、関数の定義域は、標準ライブラリ関数 acos の定義域と同じです。acos の使用時の定義域エラーを検出するチェッカー [標準ライブラリの浮動小数点ルーチンの無効な使用] は、acos32 に伴う同種のエラーを検出するように拡張できます。カスタム関数の定義域は制限されていないが、返される値の範囲が制限されている場合も、その関数を他のチェッカーよりも正確な結果を返す同等の標準ライブラリ関数 (存在する場合) にマッピングできます。たとえば、範囲 [-1,1] の値を返す関数 cos32 は標準ライブラリ関数 cos にマッピングできます。
チェッカーの拡張
標準ライブラリ内の関数をカスタム ライブラリ関数にマッピングすることによって、標準ライブラリ内の関数に対するチェッカーを拡張できます。たとえば、前の例では、関数 acos32 を標準ライブラリ関数 acos にマッピングできます。
マッピングを実行するには、次のようにします。
特定の構文で XML ファイル内のマッピングを列挙します。
テンプレート ファイル
code-behavior-specifications-template.xmlをフォルダーpolyspaceroot\polyspace\verifier\cxx警告を回避するため、ファイル内の既存のエントリは削除してください。<function name="acos32" std="acos"> </function>
この XML ファイルをオプション
-code-behavior-specificationsの引数として指定します。
拡張可能なチェッカー
このような方法で以下のチェッカーを拡張できます。
制限
カスタム関数を、同様のセマンティクスを持つ標準ライブラリ関数にマッピングできます。その場合、以下の制約が適用されます。
カスタム関数には、標準ライブラリ関数と同じ数あるいはそれ以上の数の引数が必要です。標準ライブラリ関数のすべての引数がカスタム関数の引数にマッピングされるようにします。引数の再マッピングの例については、
-code-behavior-specificationsも参照してください。マッピングされた関数の引数には、互換性のあるデータ型がなければなりません。同様に、カスタム関数の戻り値の型には、標準ライブラリ関数との互換性がなければなりません。次に例を示します。
整数型 (
char、intなど) には、浮動小数点型 (float、doubleなど) との互換性がありません。基本型には、構造体または列挙値との互換性がありません。
ポインター型には、非ポインター型との互換性がありません。
