関数引数のポインター渡しをチェックする初期化のためのチェッカーの拡張

このトピックでは、関数引数のポインター渡しを初期化でチェックするためのチェッカーの拡張方法を説明します。既定では、Bug Finder は関数呼び出し時点でのこのような引数の初期化に対するチェックを行いません。初期化は関数本体で実行される場合があるからです。しかし、特定の関数では、関数呼び出し時点で初期化に対する引数のポインター渡しをチェックするためのチェッカーを拡張できます。

既存のチェッカーに対する必要性の特定

システム境界の一部であるいくつかの関数呼び出しがあり、境界をまたいで初期化済みバッファーが確実に渡されるようにする必要があるとします。たとえば、AUTOSAR のランタイム環境または Rte_ 関数では、ソフトウェア コンポーネントから他のソフトウェア コンポーネントへの通信が許可されています。それらの関数へのポインター引数が初期化されたバッファーを指すようにする必要がある場合があります。

たとえば、次のコードの抜粋を考えます。

extern void Rte_Write_int(unsigned int, int*);

void writeValueToAddress() {
    const unsigned int module_id = 0xfe;
    int x;
    Rte_Write_int(module_id, &x);         
}
引数 x は Rte_Write_int 関数にポインター渡しされます。Bug Finder は関数呼び出し時点での x の初期化に対するチェックを行いません。Rte_Write_int の本体で x を読み取ろうとすると Bug Finder は初期化されていない変数にフラグを設定します。しかし、関数本体を含むモジュールを解析に指定できないものの、x が関数呼び出し時点で初期化されていないことを検出する必要がある場合が考えられます。

チェッカーの拡張

一部の関数へのポインター引数が初期化されたバッファーを指さなければならないことを指定できます。たとえば、Rte_Write_int がそのような関数の 1 つであることを指定するには、以下のようにします。

  1. 特定の構文で XML ファイル内に関数を列挙します。

    テンプレート ファイル code-behavior-specifications-template.xml をフォルダー polyspaceroot\polyspace\verifier\cxx から書き込み可能な場所にコピーし、そのファイルを変更します。以下の構文を使用して、ファイル内に関数を既存の同様のエントリの後ろに入力します。

    <function name="Rte_Write_int">
   <check name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="2"/>
</function>
    この構文は、Bug Finder が関数 Rte_Write_int の第 2 引数をチェックして、初期化されたバッファーを引数が指しているかどうかを判断しなければならないことを示します。警告を回避するため、ファイル内の既存のエントリは削除してください。

    関数のグループを扱うためワイルドカード * も使用できます。Rte_Write_ で始まるすべての関数を指定するには、次のように入力します。

    <function name="Rte_Write_*">
   <check name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="2"/>
</function>

  2. この XML ファイルをオプション -code-behavior-specifications の引数として指定します。

解析を再実行すると、関数 Rte_Write_int が呼び出されるとき &x の[未初期化変数] 欠陥が表示されます。

拡張可能なチェッカー

このオプションを使用することで、これらのチェッカーが拡張されます。

参考

トピック