環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe)

制約を設けない限り、環境ポインターはデリファレンスに対して安全でない可能性があることを指定

説明

このオプションは Code Prover 解析のみに影響します。

このオプションは、MATLAB® コードまたは Simulink® モデルから生成されたコードでは使用できません。

制約を設けない限り環境ポインターが安全ではないと、検証で考慮されなければならないことを指定します。環境ポインターとは、コードの外部で値を代入できるポインターです。

環境ポインターとしては、次が挙げられます。

  • グローバル ポインターまたは extern ポインター。

  • スタブ関数から返されるポインター。

    コードに関数定義が含まれていない場合、またはオプション [スタブを生成する関数] (-functions-to-stub) を使用して関数定義をオーバーライドする場合、その関数はスタブ化されます。

  • 呼び出される関数のポインター パラメーターは、本ソフトウェアによって生成されます。

    モジュールまたはライブラリを検証して、そのモジュールまたはライブラリに関数への明示的な呼び出しがない場合、その関数の呼び出しが生成されます。オプション [呼び出す関数] (-main-generator-calls) を指定して、強制的に関数呼び出しを生成することもできます。

オプションの設定

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

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [検証の前提条件] ノードを選択してから、このオプションを選択します。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [検証の前提条件] ノードを選択してから、このオプションを選択します。

  • コマンド ラインとオプション ファイル: オプション -stubbed-pointers-are-unsafe を使用します。コマンド ライン情報を参照してください。

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

このオプションを使用して、検証での外部ソースからのポインターについての仮定がより保守的になるようにします。

このオプションを指定する場合、検証では環境ポインターに NULL 値を含めることができると見なされます。NULL をチェックしないで環境ポインターを読み取ると、[不適切にデリファレンスされたポインター] チェックでは可能性のあるエラーがオレンジで示されます。このオレンジ チェックに関連付けられるメッセージでは、ポインターが NULL になる可能性があることが示されます。

設定

オン

検証では、環境ポインターに NULL 値を含めることができると見なされます。

オフ (既定の設定)

検証では、環境ポインターが次のように見なされます。

  • NULL 値を含めることはできません。

  • 許容範囲内を指しています。

ヒント

  • 統合段階でこのオプションを有効にします。この段階では、検証のために完全なコードを提供します。オレンジ チェックの原因が外部ソースにある場合でも、このようなソースからの安全でないポインターに対して保護を行える可能性があります。たとえば、不明なソースからポインターを取得する場合は、このポインターを NULL 値についてチェックします。

    単体テスト段階ではこのオプションを無効にします。この段階では、単体で発生するエラーに注目します。

  • AUTOSAR ランナブルのコード実装を検証する場合、Code Prover では、ランナブルへのポインター引数および Rte_ 関数から返されるポインターが NULL ではないと仮定します。このオプションを使用してこの仮定を変更することはできません。保守的な仮定を使用した AUTOSAR コードに対する Polyspace の実行を参照してください。

  • このオプションを有効にすると、コード内でのオレンジ チェックの数が増加する場合があります。

    環境ポインターは安全環境ポインターは安全でない

    [不適切にデリファレンスされたポインター] チェックがグリーンになります。検証では、env_ptr が NULL ではなく、すべてのデリファレンスが許容範囲内にあると仮定されます。検証では、デリファレンスの結果が全範囲になると仮定されます。たとえば、次の場合、戻り値は int 型の全範囲を含みます。

      int func (int *env_ptr) {
      return *env_ptr;
  }

    [不適切にデリファレンスされたポインター] チェックがオレンジになります。検証では、env_ptr が NULL になる可能性があると仮定されます。

      int func (int *env_ptr) {
      return *env_ptr;
  }

    このオプションを有効にすると、グレー チェックの数が減少する場合があります。

    環境ポインターは安全環境ポインターは安全でない

    検証では、env_ptr が NULL にはならないと仮定されます。if 条件は常に真になり、else ブロックには到達しません。

      #include <stdlib.h>
  int func (int *env_ptr) {
      if(env_ptr!=NULL)
	         return *env_ptr;
      else
	         return 0;
  }

    検証では、env_ptr が NULL になる可能性があると仮定されます。if 条件は真になるとは限らず、else ブロックに到達する可能性があります。

      #include <stdlib.h>
  int func (int *env_ptr) {
      if(env_ptr!=NULL)
	         return *env_ptr;
      else
	         return 0;
  }

  • すべての環境ポインターを安全か安全でないかと見なすのではなく、一部の環境ポインターに制約を個別に設けることができます。Polyspace 解析の外的制約の [ポインターの初期化] の説明を参照してください。

    ポインターに制約を個別に設けるときは、[初期化モード] を最初に指定してから、[ポインターの初期化] オプションで Null、Not Null、または Maybe Null のいずれかをそのポインターに指定します。[初期化モード] に応じて、すべての環境ポインターのグローバル指定がオーバーライドされるかどうかが決まります。

    • ポインターの [初期化モード] を [INIT] または [PERMANENT] に設定すると、[ポインターの初期化] の選択によってこのオプションの指定がオーバーライドされます。たとえば、環境ポインター ptr に Not NULL を指定すると、環境ポインターが安全でないと見なさなければならないと指定しても、検証では ptr が NULL ではないと仮定されます。

    • [初期化モード] を [MAIN GENERATOR] に設定すると、このオプションの指定が検証で使用されます。

      スタブ関数から返されるポインターには、オプション [MAIN GENERATOR] は使用できません。このようなポインターのグローバル指定を制約の [ポインターの初期化] オプションを使ってオーバーライドする場合、[ポインターの初期化] オプションも変更しなければ、グローバル指定に戻すことはできません。

  • このオプションを無効にすると、検証ではポインターのすべての深さでデリファレンスが有効であると見なされます。

    たとえば、以下のコードでは、すべてのデリファレンスが有効であると見なされます。

    int*** stub(void);

void func2() {
        int ***ptr = stub();
        int **ptr2 = *ptr;
        int *ptr3 = *ptr2;
}

コマンド ライン情報

パラメーター: -stubbed-pointers-are-unsafe
既定値: オフ
例 (Code Prover): polyspace-code-prover -sources file_name -stubbed-pointers-are-unsafe
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -stubbed-pointers-are-unsafe

バージョン履歴

R2016b で導入

参考

トピック