Code Prover 解析後のソース コード ツールヒントでの変数の範囲

Polyspace® Code Prover™ は C/C++ コードを解析してランタイム エラーを検出し、解析結果を操作に対するチェックとして報告します。チェックがパス、失敗、不確定のいずれであるかに応じて、チェックの色はグリーン、レッド、オレンジになります。チェックの他に、解析ではソース コード全体でツールヒントに変数の範囲も報告されます。このようなツールヒントに示される範囲は、報告された実行時チェックの結果を調べる際に役立ちます。また、Polyspace ユーザー インターフェイスや Polyspace Access™ Web インターフェイスで他のナビゲーション ツールを使用する際に、コードをより深く理解するうえでも役立ちます。

たとえば、変数 beta に対するこのツールヒントは、この変数がローカル変数であり、(float が 32 ビットのターゲットで) データ型は float であり、その値は範囲内にあることを示しています ([0.1 ..0.5])。この範囲は、このコード操作を通過する可能性のある、すべての実行パスに含まれる、beta の値を結合したものです。

Source Code panel showing tooltip for the beta variable.

Code Prover が変数の範囲を報告する理由

Code Prover は、ソース コードの各操作を解析し、各操作を通過するすべての実行パスを検出します (検証の前提条件に基づく)。変数または操作のインスタンスの範囲が解析によって報告される場合、この範囲は、その変数または操作に到達するすべての実行パスからの値を結合したものです。

次の例を考えます。Code Prover が関数 func を解析すると、この解析ではこの関数のほぼすべての変数の変数範囲が報告されます。各行のコードのコメントは、Code Prover 解析で報告された変数範囲を示しています。示される範囲は、行の操作の "実行後" に発生したものであることに注意してください。

int func(unsigned int count) { // count is in [0 .. UINT_MAX]
    int var;
    if(count <= 5)
        var = count; //var is in [0..5]
    else
        var = 100;
    return var; //var is 100 or in [0..5]
}

たとえば、ツールヒントでは変数範囲が次のように示されます。

  • 関数の先頭。

    func はコード内の他の場所では呼び出されないとします。Code Prover はデータ型 unsigned int に基づいて、count は範囲 [0 ..232 - 1] または [0 .. UINT_MAX] の値を取ることができると想定します。

  • 条件ステートメントの各分岐。

    実行パスが if-else ステートメントの if 分岐に入ることができるのは、count が 5 以下の場合のみです。したがって if ブロック内部では、count には次の範囲の値のみを格納できます。[0 ..5]。var 変数は、制約付き count からその値を取り、同じ制約が適用されます。

  • 末尾 (関数が戻る場合)。

    return ステートメントの var は、if 分岐からの値 [0 .. 5] または else 分岐からの値 100 のいずれかを取ることができます。return ステートメントの var のツールヒントは、この 2 つの範囲をマージし、次の範囲を表示します。100 または [0 ..5]。

変数範囲のツールヒントを使用して、コード内のデータ フローを追跡し、ランタイム エラーの原因となる可能性がある値を、変数がどのように取得するかを理解できます。

変数範囲が予想よりも狭いことがある理由

場合によっては、変数で報告される範囲が予想よりも狭いことがあります。予想よりも狭い範囲は、2 つの無関係に見える変数が、以前の操作では関連していた可能性があることを意味します。

以下の例を考えてみます。各行のコードのコメントには、"各行の操作の終わりで" Code Prover 解析で報告された変数範囲が示されています。

void func(int arg) {

    int first, second, diff;
    first = arg;
    assert( first >= 0 && first <= 256*400); // first is in [0 .. 102400]
    second = (first << 4);  // second is in [0 .. 1638400]
    diff = (first * 16) -  (second + 256);  // diff is only -256
}

一見すると、最終行の diff のツールヒントが予想と異なっているように見えます。変数 first は範囲 [0..102400] にあり、変数 second は範囲 [0 ..1638400] にありますが、差分 diff の値は -256 の 1 つだけです。

diff の値が 1 つだけである理由は、直前の操作:

second = (first << 4);
で、first と second の値に関係なく、first * 16 が常に second と同等であるように、first と second が関連付けられているためです。したがって、すべての実行パスでこれらが相殺されて、diff の値が 1 つになります。

コードで予想よりも狭い範囲が示される場合は、以前の操作で、現在の操作に関係する変数 2 つが関連付けられていなかったかどうかを調べてください。また、操作の前にプラグマ Inspection_Point を入力してから、コードを解析すると、操作に含まれる 2 つの変数の関係を特定できます。コード内の変数間の関係の検出を参照してください。

参考

トピック