Polyspace Code Prover の結果でコードがチェックされない理由

問題

プログラムの実行フローの早期にコンパイラ エラーまたはレッド チェックがある場合、Polyspace® Code Prover™ はそれ以降のプログラムを解析しません。検証後、コードの大部分でランタイム エラーがチェックされていないことがわかります。このトピックでは、Code Prover により解析されたコードで低い値が示される場合のさまざまな理由を説明します。

たとえば、[実行時チェック] ダッシュボードの次のグラフでは、ランタイム エラーがチェックされなかった関数が 60% もあることが示されています。

考えられる原因: コンパイル エラー

コンパイル エラーのないファイルのみが完全に解析されます。コンパイル エラーのあるファイルでは、コンパイル エラーの性質によって、一部の関数が解析されない場合があります。

  • コンパイル エラーが関数本体内で発生した場合、そのファイル内のコンパイル エラーがない残りの関数のみが解析されます。

  • 関数シグネチャなど、関数本体以外でコンパイル エラーが発生する場合は、コンパイル エラーの性質によって、ファイル内の残りの関数は解析される場合と解析されない場合があります。

コンパイルされなかったファイルがあるか確認するには、解析ログをチェックします。詳細については、View Compilation Errors When Running Polyspace Static Analysisを参照してください。

解決法

コンパイル エラーを修正して解析を再実行します。

詳細については、それぞれ以下を参照してください。

考えられる原因: 早い段階でのレッド チェックまたはグレー チェック

関数呼び出し階層の先頭方向にレッド チェックまたはグレー チェックがあります。レッド チェックやグレー チェックがあると、その後のコードがチェックされないことがあります。

  • レッド チェック: 検証では、レッド チェックを含むコード ブロックのその後の操作がチェックされません。

  • グレー チェック: グレー チェックは、到達不能コードを示します。検証では、到達不能コードの操作に対してランタイム エラーがチェックされません。

チェックされないコード ブロックから関数を呼び出している場合、検証ではそれらの関数もチェックされません。関数呼び出し階層の先頭方向にレッド チェックまたはグレー チェックがある場合、それ以降の階層にある関数はチェックされない場合があります。その結果、膨大な量のコードがチェックされなくなります。

たとえば、次のコードでは、4 つの関数のうち 1 つしかチェックされていません。関数 func_called_from_unreachable_1、func_called_from_unreachable_2、および func_called_after_red はチェックされません。main のみチェックされます。

void func_called_from_unreachable_1(void) {
}

void func_called_from_unreachable_2(void) {     
}

void func_called_after_red(void) {
}

int glob_var;

void main(void) {
     int loc_var;
     double res;
     
     glob_var=0;
     glob_var++;
     
     if (glob_var!=1) {
           func_called_from_unreachable_1();
           func_called_from_unreachable_2();
     }
     
     res=0;
     /* Division by zero occurs in for loop */
     for(loc_var=-10;loc_var<10;loc_var++) {
	          res += 1/loc_var;
     }
     
     func_called_after_red();
}

解決法

main 関数または別のエントリポイント関数がレッド チェックまたはグレー チェックになっているかどうかを確認します。その後のチェックされないコードから関数の大半を呼び出しているかどうかを確認します。

あるいは、チェックされていない任意の関数を考慮して、その関数がチェックされない理由を調べることができます。同じ理由が多くの関数に当てはまるかどうかを確認します。エントリ ポイントからまったく呼び出されない関数または到達不能コードから呼び出される関数を検出するには、オプション呼び出されない関数の検出 (-uncalled-function-checks)を使用します。

レッド チェックまたはグレー チェックをレビューして修正します。

考えられる原因: 不適切なオプション

必要な解析オプションを指定していません。次のオプションは、指定が不適切だとコードがチェックされない原因になる可能性があります。

  • マルチタスキング チェックの構成:マルチタスキング コードを検証している場合、このオプションを使ってエントリ ポイント関数を指定します。

    考えられる指定エラーには次のようなものがあります。

    • 同時実行の自動検出によってスレッド作成を検出することを想定したが、まだ自動検出をサポートしないスレッド作成プリミティブを使用している。

    • 手動マルチタスキング設定で、エントリ ポイントをすべて指定しなかった。

  • ライブラリの検証の構成:main 関数がコードに存在しない場合はこのオプションを使って生成します。モジュールまたはライブラリを検証するときは、このオプションを使用します。

    生成した main が呼び出さなければならないすべての関数を指定していません。

  • コード制約の構成:これらのオプションを使って、コードの外側から変数の範囲を制約するか、関数のスタブ化を強制します。

    考えられる指定エラーには次のようなものがあります。

    • 指定した変数の範囲が狭すぎるため、到達可能だったコードが到達不能になった。

    • 一部の関数を意図しないでスタブ化した。

  • ソースとビルド オプションの構成:このオプションを使用して、ビルド システムをエミュレートするか、コンパイラを指定するか、またはプリプロセッサ マクロを定義または定義解除します。

    コンパイラが暗黙的に定義されていると見なすマクロを明示的に定義しなければならない場合があります。

解決法

前述の順序でオプションをチェックします。指定が不適切な場合は修正します。

考えられる原因: main 関数が終了しない

この原因は、エントリ ポイント関数全体がチェックされない場合のマルチタスキング コードにのみ当てはまります。

マルチタスキング オプションを手動で設定する場合、Polyspace マルチタスキング モデルに対する制限に従わなければなりません。特に、main 関数には無限ループやランタイム エラーが含まれていてはなりません。そうでない場合、エントリポイント関数がチェックされません。

たとえば、次の例では、task2 をエントリ ポイントとして指定してもチェックされません。その理由は、main 関数に無限ループがあるためです。

void performTask1Cycle(void);
void performTask2Cycle(void);

void main() {
 while(1) {
    performTask1Cycle();
  } 
}

void task2() {
 while(1) {
    performTask2Cycle();
  }
}

main 関数の while キーワードは赤の破線の下線付きで表示されます。ツールヒントには、ループが終了しない可能性があることが示されます。

同様に、ランタイム エラーが発生すると、ランタイム エラーにつながる関数呼び出しは、赤の破線の下線付きで付随するツールヒントと共に表示されます。

解決法: main 関数を終了させる

main 関数が終了しない理由を修正します。

  • 理由が明確なランタイム エラー (レッド チェック) である場合、エラーを修正します。

  • 理由が無限ループの場合、ループが無限になる理由を確認します。

    main 関数の無限ループが周期タスクを表している場合、main 関数を終了して無限ループを別のエントリポイント関数に移します。main 関数を実際に変更することなく Polyspace 解析を行う目的でのみ、この変更を行うことができます。Polyspace マルチタスキング解析の手動設定を参照してください。