システムのすべての入力値を考慮する、さらに厳密なチェックを実行 (-checks-using-system-input-values)

さらに厳格なチェックを有効にし、欠陥の検出につながる値の例を提供する

説明

このオプションは Bug Finder 解析のみに影響します。このオプションは、MATLAB® コードまたは Simulink® モデルから生成されたコードでは使用できません。

一部の数値、静的メモリ、データ フロー関連欠陥チェッカー、およびコーディング規約チェッカーに対し、より厳格な解析モードを有効にします。このオプションを有効にする場合は、次のようにします。

  • 解析では、問題をチェックするときに、考えられるすべてのシステム入力値が考慮されます。

  • 問題が検出された場合は、その問題を引き起こす 1 つの入力値の例が解析から提示されます。

[次の関数の入力を考慮する] (-system-inputs-from) を使用して指定した関数 foo ごとに、以下がシステム入力として考慮されます。

  • foo の引数。

  • foo またはその呼び出し先のいずれかによるグローバル変数の読み取り。

    main() 関数の場合は、解析でグローバル変数が 0 に初期化されるものと仮定されます。

  • foo またはその呼び出し先のいずれかによる volatile 変数の読み取り。

  • スタブ関数の戻り値。Bug Finder 解析は、ソース コードで関数の本体が指定されなかった場合に関数をスタブします。

  • 次のような絶対アドレスからの読み取り。

    int value = *((int*)0x1234);

このオプションの影響を受けるチェッカーについては、特定のシステム入力値から欠陥を見つけるための Bug Finder チェッカーの拡張を参照してください。

デスクトップ インターフェイスまたは Polyspace Access Web インターフェイスの [結果の詳細] ペインの [イベント] 列で欠陥の検出につながる値の例を確認できます。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [Bug Finder 解析] ノードを選択してから、このオプションを選択します。同時に有効にしなければならない他のオプションについては、依存関係を参照してください。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [欠陥とコーディング規約] 、 [チェッカー動作] ノードを選択してから、このオプションを選択します。

  • コマンド ラインとオプション ファイル: オプション -checks-using-system-input-values を使用します。コマンド ライン情報を参照してください。

このオプションを使用する理由

既定の Bug Finder 解析では、特定の不明な入力値によって引き起こされる欠陥にフラグが設定されません。入力は解析されないソース ファイルで制限または初期化される可能性がある、つまり、実際には欠陥の原因になる特定の値が発生しない可能性があるため、既定の解析動作では誤検知が最小限に抑えられます。

このオプションは、実行中にシステム入力が散発的なランタイム エラーを引き起こす可能性がある関数に対してより厳格な解析を実行するために有効にします。このオプションを使用すると、解析時間が長くなる場合があります。

設定

オン

Polyspace は、数値および静的メモリ欠陥チェッカーのサブセットに対して考えられるすべてのシステム入力値を考慮し、欠陥の検出につながる値の例を提供します。

オフ (既定の設定)

Polyspace は、assert や if などのコード内で入力が制限される場合にのみ、考えられるシステム入力値を考慮します。この解析は、欠陥の検出につながる値の例を提供しません。

依存関係

ヒント

  • グローバル変数に対する外部制約を設定した場合は、その制約内の欠陥の原因になるグローバル変数値の例だけが解析に表示されます。制約の設定 (-data-range-specifications) を参照してください。

  • 入力がポインター p の場合は、解析でそのポインターが NULL ではなく、安全にデリファレンス可能であると仮定されます。欠陥の原因になる入力値の例は、*p の値です。この値は、[結果の詳細] ペインで配列として表現されます。たとえば、このコード スニペットでは、次のようになります。 

    void func(int* x){
	int tmp= *(x+3);
	
	if(1/(tmp-4))
		return;
}
    欠陥の原因になる入力値の例は、配列が *x、*(x+1)、*(x+2)、および *(x+3) を表す {0,0,0,4} です。値 *(x+3)=4 はゼロ除算を引き起こします。

  • 解析では、外部ソースから値を読み取るこれらの標準ライブラリ関数がスタブ関数として扱われます。

    • getchar

    • getc

    • fgetc

    • scanf

  • より厳格な解析では、考えられるすべてのシステム入力値を考慮しますが、すべての値を網羅した解析ではありません。Bug Finder で特定の入力によって欠陥が引き起こされるかどうかを判断できない場合は、欠陥が表示されません。網羅的解析の詳細については、Polyspace Bug Finder と Polyspace Code Prover の違いを参照してください。

コマンド ライン情報

パラメーター: -checks-using-system-input-values
既定値: オフ
例 (Bug Finder): polyspace-bug-finder -sources file_name -checkers numerical,static_memory -checks-using-system-input-values
例 (Bug Finder Server): polyspace-bug-finder-server -sources file_name -checkers numerical,static_memory -checks-using-system-input-values

バージョン履歴

R2020a で導入

参考

トピック