コード内の変数間の関係の検出

このチュートリアルでは、コード内の任意の操作に含まれる変数が前の操作に関連しているかどうかを判断する方法を説明します。

たとえば、次の操作を考えます。

return(var1 - var2);

  • IDE で、実行を停止するブレークポイントを設定し、"特定の実行" における var1 と var2 の値を判断します。

  • Polyspace® で、コードの解析後、var1 と var2 のツールヒントにその検証で考慮される "すべての実行" の値の範囲が表示されます。

ただし、範囲情報は、変数が関係しているかどうかを判断するのに十分ではありません。関係を判断するには追加の手順を実行しなければなりません。

変数の関係を判断するためのプラグマの挿入

この例では、強調表示された演算を考えます。ちらりと見ただけでは、wheel_speed と wheel_speed_old が関係しているかどうかはわかりません。しかし、この情報は、以降の演算で生じる可能性のあるバグを理解するために重要です。

#define MAX_SPEED 120
#define TEST_TIME 10000

int wheel_speed;
int wheel_speed_old;

int out;

int update_speed(int new_speed) {
    if(new_speed < MAX_SPEED)
	return new_speed;
    else
	return MAX_SPEED;
}

void increase_speed(void)
{
 
  int temp, index=1;

  while(index<TEST_TIME) {
    temp = wheel_speed - wheel_speed_old;
     
    if(index > 1) {
       if (temp < 0)
         out = 1;
       else
         out = 0;
    }
    
    wheel_speed_old = update_speed(wheel_speed);
    index++;
  }

}

wheel_speed と wheel_speed_old の関係が必要な理由と関係を検出する方法を理解するには、以下を行います。

  1. Polyspace 解析の変数 wheel_speed の範囲を初期値の 0..100 に制約します。解析オプション制約の設定 (-data-range-specifications)を使用します。

  2. このコードに対して解析を実行し、結果を開きます。グレーの [到達不能コード] チェックを選択します。

    if (temp < 0)
         out = 1;

    チェックは、変数 temp が非負であることを示します。temp は以下に示す前の演算に基づきます。

    temp = wheel_speed - wheel_speed_old;

  3. wheel_speed と wheel_speed_old の範囲を確認します。これらの変数の上にカーソルを置きます。次の範囲が表示されます。

    • wheel_speed:0..100

    • wheel_speed_old:int 変数の全範囲。

    wheel_speed - wheel_speed_old が常に非負である理由は、これらの範囲からは明らかではありません。変数が何らかの形で関係しているかどうかを調べる必要があります。

  4. 変数の関係を必要とする行の前にプラグマを挿入します。if(temp < 0) の直前に次の行を追加します。

    #pragma Inspection_Point wheel_speed wheel_speed_old

  5. 解析を再実行し、結果を開きます。追加した行の wheel_speed_old の上にカーソルを置きます。

    ツールヒントで wheel_speed と wheel_speed_old が関係していることを確認できます。

    wheel_speed_old <= wheel_speed

  6. 2 つの変数がどのように関係しているかを調べるには、wheel_speed_old のすべてのインスタンスを検索します。[ソース] ペインで、wheel_speed_old を右クリックし、[すべての参照を検索] を選択します。

    インスタンスを参照します。この場合、wheel_speed と wheel_speed_old を関連付けている行は次のとおりです。

      wheel_speed_old = update_speed(wheel_speed);
    この行によって、while ループの最初の実行の後 wheel_speed_old が wheel_speed_old 以下であることが確保されます。分岐 if(index > 1) には、2 回目以降の実行で入ります。この分岐では、wheel_speed と wheel_speed_old の関係が、グレーの [到達不能コード] チェックを通じて反映されています。

ヒント

ツールヒントに示される関係の詳細を無視します。ツールヒントを使用して、特定の変数が関係しているかどうかを確認します。その後、変数のインスタンスを検索して、どのように関係しているかを調べます。

その他の調査

プラグマ Inspection_Point を使用してコード内の任意の位置における変数間の関係を判断できます。#pragma ステートメントに変数を必要なだけ入力できます。

#pragma Inspection_Point var1 var2 ... varn

他の例でこの手法を試します。たとえば、[ヘルプ] 、 [例] 、 [Code_Prover_Example.psprj] を選択します。結果をファイル別にグループ化します。ファイル single_file_analysis.c に、次のコードがあります。

    if (output_v7 >= 0) {

      #pragma Inspection_Point output_v7 s8_ret
      saved_values[output_v7] = s8_ret;
      return s8_ret;
    }
最後の 2 つのステートメントの s8_ret にカーソルを置くと、s8_ret の範囲が異なっていることがわかります。2 つのステートメントの間で何が変わったかを調査します。

ヒント: #pragma ステートメントのツールヒントに、変数 s8_ret が変数 output_v7 に関係していることが示されます。output_v7 の範囲を減らすオレンジ チェックに注意します。

参考

トピック