フィールドに volatile 修飾子があることを考慮する (-consider-volatile-qualifier-on-fields)

コード内のどの位置にあっても、構造体の volatile 修飾子付きフィールドは取り得るすべての値を含む可能性があると仮定

説明

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

構造体のフィールドの volatile 修飾子が、検証で考慮されなければならないことを指定します。

オプションの設定

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

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

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

• コマンド ラインとオプション ファイル: オプション -consider-volatile-qualifier-on-fields を使用します。コマンド ライン情報を参照してください。

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

変数に volatile 修飾子を付けることで、コードで明示的にその変数の値を変更しなくても、連続する演算の間にその変数の値が変化する可能性があることを示します。たとえば、var が volatile 変数の場合、連続演算 res = var; res =var; では、res に読み取られる 2 つの var の値が異なる結果になる可能性があります。

このオプションを使用して、構造体のフィールドの volatile 修飾子が検証でエミュレートされるようにします。このオプションを選択すると、本ソフトウェアでは volatile 構造体フィールドはコードのどの位置でも全範囲の値を含むと仮定されます。範囲は、構造体フィールドのデータ型によってのみ決まります。

設定

オン

検証では、構造体のフィールドの volatile 修飾子が考慮されます。

次の例の場合、検証では、フィールド val1 は、コードのどの位置にあっても int 型で許容されるすべての値を取り得ると見なされます。

struct myStruct {
   volatile int val1;
   int val2;
};

val1 に具体的な値を書き込み、次の演算でこの変数を読み取る場合でも、変数の読み取り結果はその変数が取り得る任意の値になります。

struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion can fail

オフ (既定の設定)

検証では、構造体のフィールドの volatile 修飾子が無視されます。

次の例の場合、検証ではフィールド val1 の修飾子が無視されます。

struct myStruct {
   volatile int val1;
   int val2;
};

val1 に具体的な値を記述し、次の演算でこの変数を読み取ると、変数の読み取り結果は具体的に指定した値になります。

struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion passes

ヒント

• volatile フィールドがハードウェアから読み取る値を表さない場合、または連続演算の間に値が変化することが想定されない場合は、このオプションを無効にします。この場合、別に理由があって volatile 修飾子を使用しており、検証ではこのフィールドで全範囲の値を考慮する必要はありません。

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

  次の例でこのオプションを使用すると、レッド チェックまたはグリーン チェックがオレンジに変わるか、グレー チェックがなくなります。volatile 修飾子を考慮することで、チェックの色が変わります。この例では、次の構造体定義を使用します。

  struct myStruct {
     volatile int field1;
     int field2;
  };
  
  

  オプションなしの色	オプションなしの結果	オプションありの結果
  グリーン	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 == 1); }	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 ==1); }
  レッド	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 != 1); }	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 !=1); }
  グレー	void main(){ struct myStruct structVal; structVal.field1 = 1; if (structVal.field1 != 1) { /* Perform operation */ } }	void main(){ struct myStruct structVal; structVal.field1 = 1; if (structVal.field1 != 1) { /* Perform operation */ } }

• C++ コードでは、このオプションがクラス メンバーにも適用されます。

コマンド ライン情報

パラメーター: -consider-volatile-qualifier-on-fields

既定値: オフ

例 (Code Prover): polyspace-code-prover -sources file_name -consider-volatile-qualifier-on-fields

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -consider-volatile-qualifier-on-fields

バージョン履歴

R2016b で導入

参考

トピック

• Polyspace 解析オプションの指定