Code Prover の実行時チェックの変更または無効化

Code Prover 解析は、ソース コードの一般的な実行時エラーを網羅的にチェックします。静的解析の網羅的特性は、セーフティ クリティカルなソフトウェアで実行時にエラーが発生しないように設計されています。セーフティ クリティカルという解析の目的のために、Code Prover では以下の操作が禁止されています。

  • 特定の実行時チェックを選択的に無効にする。

  • ソース コードの注釈を通して実行時チェックの結果を結果リストに表示しない。注釈を通して結果を正当化できますが、正当化された結果はそのまま結果リストに残ります。

フィルターの [after the analysis] を適用するか、フィルター済みのレポートを作成することによっても、特定の結果を抑制することができます。Code Prover の結果からフィルター済みのレポートを作成する場合は、レポートにフィルターが表示され、選択したものが反映されます。詳細は、次を参照してください。

ただし、特定のチェックの既定の動作を変更して、初期化のチェックを完全に無効にすることができます。解析結果からレポートを生成する場合は、レポートにこれらのオプションの用途が表示されます。

このトピックでは、特定の実行時チェックの既定の動作を変更するオプションについて説明します。1 つのオプションが主に 1 つの特定のタイプのチェックを対象としますが、他のタイプのチェックも影響を受けることに注意してください。レッド チェックおよびオレンジ チェック以降の Code Prover 解析を参照してください。

整数のオーバーフロー

チェック既定の動作オプション
無効なシフト演算

左シフトが符号付きオペランドで許可されません。

左シフトで負のオペランドを許可 (-allow-negative-operand-in-shift)
オーバーフロー

符号付き整数オーバーフローが禁止されます。

符号付き整数のオーバーフロー モード (-signed-integer-overflows)
オーバーフロー

符号なし整数オーバーフローが検出されません。

符号なし整数のオーバーフロー モード (-unsigned-integer-overflows)

浮動小数点オーバーフロー

チェック既定の動作オプション

非有限の浮動小数が考慮されません。
非正規浮動小数点

非正規結果が検出されません。

非正規検出モード (-check-subnormal)

初期化

チェック既定の動作オプション

変数が読み取られたときにのみ初期化のチェックが実行されます。

未初期化のチェックを無効にする (-disable-initialization-checks)

初期化コードでグローバル変数に値が割り当てられていません

変数が読み取られたときにのみグローバル変数の初期化のチェックが実行されます。

ライブラリ関数

チェック既定の動作オプション
標準ライブラリ ルーチンの無効な使用

標準ライブラリ ルーチンのみが引数の妥当性をチェックされます。ユーザー定義のライブラリ関数はチェックされません。

-code-behavior-specifications

ポインター

チェック既定の動作オプション
不適切にデリファレンスされたポインター

構造体フィールドへのポインターで別のフィールドを指すことができません。

フィールド間のポインター演算を有効にする (-allow-ptr-arith-on-struct)

不適切にデリファレンスされたポインター

構造体へのポインターには、構造体全体にとって十分なバッファーを割り当てる必要があります。

構造体の不完全または部分的割り当てを許可する (-size-in-bytes)
不適切にデリファレンスされたポインタースコープ外のスタック ポインター デリファレンスが検出されません。スコープ外のスタック ポインター デリファレンスを検出 (-detect-pointer-escape)
正確性の条件関数ポインターの不一致が許可されません。関数ポインターの許容呼び出し (-permissive-function-pointer)

到達不能コードまたはデッド コード

チェッカー既定の動作オプション

呼び出されなかった関数と到達不能コードから呼び出された関数は報告されません。

呼び出されない関数の検出 (-uncalled-function-checks)

影響仕様の違反

チェッカー既定の動作オプション

Code Prover は、ソースとシンクとして指定されているプログラム要素間の影響を確認しません。

参考

トピック