このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

-code-behavior-specifications

コードの要素 (関数など) への動作の関連付け

構文

-code-behavior-specifications file

説明

-code-behavior-specifications file では、特定の動作をコードの要素に関連付けて、それらの要素に対するチェック結果に変更を加えることができます。ここで、file は特定の動作をコードの要素 (関数など) に関連付けます。次のいずれかの形式で指定できます。

  • XML ファイル。

    1 つの XML ファイルのみを引数として指定できます。サンプル テンプレート ファイル code-behavior-specifications-template.xml に XML の構文が示されています。このファイルは polyspaceroot\polyspace\verifier\cxx\ (polyspaceroot は Polyspace® インストール フォルダー) にあります。

  • Datalog (.dl) ファイル。

    複数の Datalog ファイルをコンマ区切りの引数として指定できます。

XML ファイルまたは Datalog ファイルの絶対パスあるいは相対パスを指定します。たとえば、Datalog ファイル myFile.dl がフォルダー C:\CodeBehaviorSpec 内にあり、現在のフォルダーが C:\myScript であるとします。コマンド ラインで、このファイルの絶対パスを指定するには、次のようにします。

polyspace-bug-finder ... -code-behavior-specification "C:\CodeBehaviorSpec\myFile.dl"
または、現在のフォルダーを基準とした相対パスを指定するには、次のようにします。
polyspace-bug-finder ... -code-behavior-specification "..\CodeBehaviorSpec\myFile.dl"

XML 形式と Datalog 形式ではサポートされるコードの動作が異なります。詳細は、次を参照してください。

たとえば、次のようにします。

  • ライブラリ関数を Polyspace によって認識される対応する標準関数にマッピングします。標準ライブラリ関数にマッピングすることは、精度の向上や新しいスレッドの自動検出に役立ちます。

  • 関数は特別な動作をする、または、関数は特別なチェックを受ける必要があることを指定します。

    たとえば、ある関数は初期化された変数のアドレスのみを引数として取る必要がある、または、ある関数をまったく使用してはならないということを指定できます。

Polyspace デスクトップ製品のユーザー インターフェイス、コマンド ライン、または IDE で、このオプションを指定できます。

  • コマンド ラインから検証を実行する場合、XML ファイルへの絶対パスか、コマンドを実行するフォルダーからの相対パスを指定します。

  • ユーザー インターフェイスから検証を実行する場合 (デスクトップ製品のみ)、[その他] フィールドで、XML ファイルの絶対パスまたは Polyspace プロジェクトの場所からの相対パスとともにこのオプションを指定します。Otherを参照してください。

  • IDE で Polyspace as You Code の拡張機能を使用する場合は、このオプションを解析オプション ファイルに入力します。オプション ファイルを参照してください。

解析結果から生成されるレポートには、このオプションが使用されていることだけが示されます。コードの要素に関連付けられた動作の詳細は示されません。

例

標準関数へのマッピングを指定

Polyspace のインストールで提供されるサンプル マッピング XML ファイルを適用して、関数を標準関数にマップできます。

既定の検証では、このコードで [ユーザー アサーション] オレンジ チェックが発生するものとします。

double x = acos32(1.0);  
assert(x <= 2.0);
関数 acos32 が関数 acos と同様に動作し、戻り値が 0 であるとします。その結果、assert ステートメントのチェックはグリーンになると考えられます。しかし、acos32 の解析精度が低いため、検証では acos32 が double 型の範囲の任意の値を返すと見なされます。チェックはオレンジになります。関数 acos32 を acos にマップするには、以下を行います。

  1. polyspaceroot\polyspace\verifier\cxx\ のファイル code-behavior-specifications-template.xml を別の場所 ("C:\Polyspace_projects\Common\Config_files" など) へコピーします。ファイルの書き込み権限を変更します。

  2. 関数を標準関数にマップするには、XML ファイルの内容を変更します。関数 acos32 を標準ライブラリ関数 acos にマップするには、次のコードを変更するとします。 

    <function name="my_lib_cos" std="acos"> </function>
    次に変更します。
    <function name="acos32" std="acos"> </function>

  3. 検証用にファイルの場所を指定します。

    • Code Prover:

      polyspace-code-prover -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"

    • Code Prover Server:

      polyspace-code-prover-server -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"

引数再マッピングによる標準関数へのマッピングの指定

場合によっては、関数の引数と標準関数の引数が 1 対 1 に対応しないことがあります。そのような場合、関数の引数を標準関数の引数に再マッピングします。次に例を示します。

  • __ps_lookup_table_clip:

    この Polyspace 固有の関数は、引数としてルックアップ テーブル配列のみを受け取り、ルックアップ テーブルの範囲内の値を返します。独自のルックアップ テーブル関数では、ルックアップ テーブル配列自体のほかに、追加の引数を受け取ることがあります。この場合、引数再マッピングを使用して、関数の引数のうちルックアップ テーブル配列に当たる引数を指定します。

    たとえば、関数 my_lookup_table を次のように宣言しているとします。

    double my_lookup_table(double u0, const real_T *table,
                                     const double *bp0);
    関数 my_lookup_table の 2 番目の引数が、ルックアップ テーブル配列です。ファイル code-behavior-specifications-template.xml に次のコードを追加します。
    <function name="my_lookup_table" std="__ps_lookup_table_clip">
    <mapping std_arg="1" arg="2"></mapping>
</function>

    この関数を以下のように呼び出しているとします。

    res = my_lookup_table(u, table10, bp);
    検証では、この呼び出しが次のように解釈されます。
    res =__ps_lookup_table_clip(table10);
    検証では、res の値が、table10 の値の範囲内にあると仮定されます。

    Polyspace は、次のルックアップ テーブルの __ps_lookup_table_clip へのマッピングをサポートしています。

    • 整数から整数へのルックアップ テーブル: int* テーブルで値を検索して int 値を返す

    • 整数から浮動小数点へのルックアップ テーブル: int* テーブルで値を検索して float 値を返す

    • 浮動小数点から浮動小数点へのルックアップ テーブル: float* テーブルで値を検索して float を返す

  • __ps_meminit:

    この Polyspace 固有の関数では、最初の引数にメモリ アドレス、2 つ目の引数にバイト数を受け取ります。この関数では、メモリ アドレスから始まるメモリがバイト数分有効な値で初期化されると仮定します。独自のメモリ初期化関数では、追加の引数を受け取ることがあります。この場合、引数再マッピングを使用して、関数の引数のうち、開始アドレスとバイト数に当たる引数を指定します。

    たとえば、関数 my_meminit を次のように宣言しているとします。

         void my_meminit(enum InitKind k, void* dest, int is_aligned, unsigned int size);
    この関数の 2 番目の引数が開始アドレスで、4 番目の引数がバイト数です。ファイル code-behavior-specifications-template.xml に次のコードを追加します。
    <function name="my_meminit" std="__ps_meminit">
    <mapping std_arg="1" arg="2"></mapping>
    <mapping std_arg="2" arg="4"></mapping>
</function>

    この関数を以下のように呼び出しているとします。

    my_meminit(INIT_START_BY_END, &buffer, 0, sizeof(buffer));
    検証では、この呼び出しが次のように解釈されます。
    __ps_meminit(&buffer, sizeof(buffer));
    検証では、&buffer から始めて sizeof(buffer) バイト分が初期化されると仮定されます。

  • memset:可変個の引数。

    独自の関数の引数が可変個の場合、引数を明示的に再マッピングしなければ、その関数を標準関数に直接マップできません。たとえば、独自の関数を次のように宣言しているとします。

    void* my_memset(void*, int, size_t, ...)
    この関数を関数 memset にマップする場合は、以下のマッピングを使用します。
    <function name="my_memset" std="memset">
    <mapping std_arg="1" arg="1"></mapping>
    <mapping std_arg="2" arg="2"></mapping>
    <mapping std_arg="3" arg="3"></mapping>
</function>

精度へのマッピングの影響

以下の例は、特定の関数から標準関数にマッピングした結果を示します。

  • my_acos → acos:

    マッピングを使用すると、[ユーザー アサーション] チェックがグリーンに変わります。検証では、my_acos の戻り値が 0 であると仮定されます。

    • マッピング前:

      double x = my_acos(1.0);  
assert(x <= 2.0);

    • マッピングの指定:

      <function name="my_acos" std="acos">
</function>

    • マッピング後:

      double x = my_acos(1.0);  
assert(x <= 2.0);

  • my_sqrt → sqrt:

    マッピングを使用すると、[標準ライブラリ ルーチンの無効な使用] チェックがレッドに変わります。それ以外の場合、検証では my_sqrt の引数が非負かどうかチェックされません。

    • マッピング前:

      res = my_sqrt(-1.0);

    • マッピングの指定:

      <function name="my_sqrt" std="sqrt"> 
</function>

    • マッピング後:

      res = my_sqrt(-1.0);

  • my_lookup_table (引数 2) →__ps_lookup_table_clip (引数 1):

    マッピングを使用すると、[ユーザー アサーション] チェックがグリーンに変わります。検証では、my_lookup_table の戻り値がルックアップ テーブル配列 table の範囲内にあると仮定されます。

    • マッピング前:

      double table[3] = {1.1, 2.2, 3.3}
.
.
double res = my_lookup_table(u, table, bp);
assert(res >= 1.1 && res <= 3.3);

    • マッピングの指定:

      <function name="my_lookup_table" std="__ps_lookup_table_clip">
    <mapping std_arg="1" arg="2"></mapping>
</function>

    • マッピング後:

      double table[3] = {1.1, 2.2, 3.3}
.
.
res_real = my_lookup_table(u, table9, bp);
assert(res_real >= 1.1 && res_real <= 3.3);

  • my_meminit →__ps_meminit:

    マッピングを使用すると、[未初期化ローカル変数] チェックがグリーンに変わります。検証では、構造体 x のすべてのフィールドが有効な値で初期化されていると仮定されます。

    • マッピング前:

      struct X {
  int field1;
  int field2;
};
.
.
struct X x;
my_meminit(&x, sizeof(struct X));
return x.field1;

    • マッピングの指定:

      <function name="my_meminit" std="__ps_meminit">
     <mapping std_arg="1" arg="1"></mapping>
     <mapping std_arg="2" arg="2"></mapping>
</function>

    • マッピング後:

      struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(struct X));
return x.field1;

  • my_meminit →__ps_meminit:

    マッピングを使用すると、[未初期化ローカル変数] チェックがレッドに変わります。検証では、構造体 x のフィールド field1 のみが有効な値で初期化されていると仮定されます。

    • マッピング前:

      struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(int));
return x.field2;

    • マッピングの指定:

      <function name="my_meminit" std="__ps_meminit">
</function>

    • マッピング後:

      struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(int));
return x.field2;

制限

オプション -code-behavior-specifications を使用して、カスタム関数を同様の標準ライブラリ関数にマッピングできます。その場合、以下の制約が適用されます。

  • カスタム関数には、標準ライブラリ関数と同じ数あるいはそれ以上の数の引数が必要です。標準ライブラリ関数のすべての引数がカスタム関数の引数にマッピングされるようにします。

  • マッピングされた関数の引数には、互換性のあるデータ型がなければなりません。同様に、カスタム関数の戻り値の型には、標準ライブラリ関数との互換性がなければなりません。次に例を示します。

    • 整数型 (char、int など) には、浮動小数点型 (float、double など) との互換性がありません。

    • 基本型には、構造体または列挙値との互換性がありません。

    • ポインター型には、非ポインター型との互換性がありません。

バージョン履歴

R2016b で導入

参考

トピック