Code Prover の実行時チェックのレビュー

Polyspace^® Code Prover™ は、特定のランタイムエラーに対して C/C++ コードの各操作をチェックし、結果をレッド、グリーンまたはオレンジチェックとして表示します。詳細は、Code Prover の結果とソースコードの色を参照してください。

レッドチェックまたはオレンジチェックをレビューし、コードを修正するかどうかを判断しなければなりません。次の表は、Polyspace Code Prover が実行するチェックと、これらのチェックをレビューする方法をまとめています。

データフローチェック

以下の表は、Code Prover の一部のデータフローチェックの結果をレビューする方法を概説しています。

チェック	レビュー方法	詳細
`呼び出されない関数`	関数が `main` または別のエントリポイント関数から始まる呼び出しグラフに表示されない理由を調べる。	呼び出されていない関数チェックのレビューと修正
`到達不能の関数`	関数の呼び出しサイトを特定し、それが到達不能コードに出現する理由を調べる。	到達不能な関数チェックのレビューと修正
`未初期化ローカル変数`	変数が事前に初期化されていれば検出して、プログラムがその初期化をバイパスする可能性があるかどうか確認する。	未初期化ローカル変数チェックのレビューと修正
`未初期化ポインター`	ポインターが事前に初期化されていれば検出して、プログラムがその初期化をバイパスする可能性があるかどうかを確認する。	未初期化ポインターチェックのレビューと修正
`未初期化変数`	グローバル変数が事前に初期化されていれば検出して、プログラムがその初期化をバイパスする可能性があるかどうかを確認する。	未初期化変数チェックのレビューと修正
`初期化されていない戻り値`	関数本体全体を調べて `return` ステートメントで終了しないパスを特定する。	初期化されていない戻り値チェックのレビューと修正
`到達不能コード`	コード内の条件付きステートメントが冗長な理由 (たとえば常に ture または false になるなど) を調べる。	到達不能コードチェックのレビューと修正

数値チェック

以下の表は、Code Prover の一部の数値チェックの結果をレビューする方法を概説しています。

チェック	レビュー方法	詳細
`ゼロ除算`	分母係数がゼロ値になる操作が事前に行われていないかコード内を確認する。	ゼロ除算チェックのレビューと修正
`無効なシフト演算`	範囲外のシフト量になる操作、または左にシフトされる負の値になる操作が事前に行われていないかコード内を確認する。	無効なシフト演算チェックのレビューと修正
`オーバーフロー`	演算オーバーフローになる操作が事前に行われていないかコード内を確認する。	オーバーフローチェックのレビューと修正

静的メモリチェック

以下の表は、Code Prover の一部の静的メモリチェックの結果をレビューする方法を概説しています。

チェック	レビュー方法	詳細
`絶対アドレスの使用`	コード内での絶対アドレスの使用法を確認し、アドレスが有効であることを確認する。	絶対アドレスの使用チェックのレビューと修正
`不適切にデリファレンスされたポインター`	ポインターが割り当て済みメモリバッファー外を指すことになる操作が事前に行われていないかコード内を確認する。	不適切にデリファレンスされたポインターチェックのレビューと修正
`範囲外の配列インデックス`	配列インデックスが配列のサイズを超えることになる操作が事前に行われていないかコード内を確認する。	範囲外の配列インデックスチェックのレビューと修正

制御フローチェック

以下の表は、Code Prover の一部の制御フローチェックの結果をレビューする方法を概説しています。

チェック	レビュー方法	詳細
`無限呼び出し`	関数本体の操作を確認し、現在の関数呼び出し固有の問題によって発生するランタイムエラーを見つける。	無限呼び出しチェックのレビューと修正
`無限ループ`	ループ内の操作を確認し、ループが終了しない理由またはループ実行の 1 つで明確なランタイムエラーが発生する理由を判断する。	無限ループチェックのレビューと修正

C++ チェック

以下の表は、Code Prover の一部の C++ 固有のチェックの結果をレビューする方法を概説しています。

チェック	レビュー方法	詳細
`無効な C++ に固有の演算`	非正の配列サイズになる根本原因、または `typeid` 演算子や `dynamic_cast` 演算子の誤った使用法の根本原因を判断する。	無効な C++ に固有の演算チェックのレビューと修正
`値を返さない関数`	関数本体全体を調べて `return` ステートメントで終了しないパスを特定する。	値を返さない関数チェックのレビューと修正
`誤ったオブジェクト指向プログラミング`	特定の `virtual` メンバー呼び出し、または `this` ポインターの使用によってオブジェクト指向プログラミングの誤ったパターンが表される理由を調べる。	誤ったオブジェクト指向プログラミングチェックのレビューと修正
`null の this ポインターを呼び出すメソッド`	現在のオブジェクトを指すポインターが `NULL` 値になる可能性がある理由を調べる。	null の this ポインターを呼び出すメソッドチェックのレビューと修正
`キャッチされていない例外`	例外がどうやってキャッチされずにスローされた関数からエスケープしたのか調べる。	キャッチされていない例外チェックのレビューと修正

その他のチェック

以下の表は、Code Prover の一部の未分類のチェックの結果をレビューする方法を概説しています。

チェック	レビュー方法	詳細
`正確性の条件`	関数ポインターの誤用、配列の不適切な変換、または指定された制約外の変数値になる根本原因を見つける。	正確性の条件チェックのレビューと修正
`標準ライブラリルーチンの無効な使用`	標準ライブラリルーチンに対する現在の呼び出しの引数が無効である理由を調べる。	標準ライブラリルーチンの無効な使用チェックのレビューと修正
`ユーザーアサーション`	`assert` ステートメントの条件が失敗する理由を調べる。	ユーザーアサーションチェックのレビューと修正