volatile 変数に関する Code Prover の仮定

Polyspace^® 解析では、volatile 変数の値は明示的な書き込み操作がなくても変化する可能性があると仮定します。

グローバル volatile 変数

グローバル volatile 変数の場合、以下のようになります。

Polyspace は変数が型で許容される全範囲の値を取ると仮定。
その範囲は外部で制約できます。Polyspace 解析のグローバル変数範囲の制約を参照してください。
変数を明示的に初期化しない場合でも、変数を読み取るときに Polyspace は [未初期化変数] のグリーンチェックを生成。

ローカル volatile 変数

ローカル volatile 変数の場合、次のようになります。

Polyspace は変数が型で許容される全範囲の値を取ると仮定。
明示的に変数を初期化しない限り、変数を読み取るときに Polyspace は [未初期化ローカル変数] のオレンジチェックを生成。

この例では、Polyspace は、val1 は初期化されていない可能性があるが、val2 は初期化されていると仮定します。Polyspace は、両方の変数がその変数のデータ型で許容されるすべての値を取ると仮定するため、+ 演算がオーバーフローの原因となる可能性があると見なします。

int func (void)
{
    volatile int val1, val2=0;
    return( val1 + val2);
}

オレンジチェックの根本原因がローカル volatile 変数の場合、既定の仮定をオーバーライドして volatile 変数の値を制約することはできません。次のいずれかを試します。

volatile 変数がハードウェアから供給されたデータを表している場合、データ抽出のモデル化に関数呼び出しを使用できるかどうか確認します。たとえば、volatile int port_A を int port_A = read_location() に変更します。関数を定義する必要はありません。Polyspace は未定義の関数をスタブ化します。オプション [制約の設定] (-data-range-specifications) を使用して関数の戻り値に制約を指定できるようになります。
volatile 変数の内容をグローバルな非 volatile 変数にコピーできるかどうか試してみてください。コード全体でグローバル変数を制約できるようになります。Polyspace 解析のグローバル変数範囲の制約を参照してください。
volatile 変数をスタブ関数に置き換えてください。ただし、検証のみを目的とするものです。検証前にスタブ関数に制約を指定してください。
1. volatile 変数宣言を非 volatile 変数宣言に置き換える Perl スクリプトを作成します。ここでは、関数呼び出しから変数の値を取得します。
  たとえば、コードに volatile s8 PORT_A 行が含まれる場合、Perl スクリプトにこの置換が含まれる可能性があります。
```
$line=~ s/^\s*volatile\s*s8\s*PORT_A;/s8 PORT_A = random_s8();/g;
```
2. 解析オプション [前処理済みファイルに適用するコマンド/スクリプト] (-post-preprocessing-command) でこの Perl スクリプトの場所を指定します。
3. インクルードファイルで関数宣言を指定してください。たとえば、関数 random_s8 ではインクルードファイルに以下の宣言を含めることができます。
```
#ifndef POLYSPACE_H
#define POLYSPACE_H
signed char random_s8(void);
#endif
```
4. 関連するソースファイルのインクルードファイルに #include 命令を挿入します。
  手動で挿入する代わりに、解析オプション解析対象 (-include)でインクルードファイルの場所を指定します。

volatile パラメーター

コピー渡しの関数パラメーターに volatile 修飾子を付けても、無視されます。これは、そのコピーされたパラメーターが I/O レジスタにメモリマッピングされることはなく、またそのコピーされたパラメーターは、コード内に明示的な書き込み操作がなければその値を変更しない可能性が高いためです。volatile 修飾子は、参照渡しのパラメーターに対しては引き続き適用されます。

この例では、引数 x はコピー渡し、y は参照渡しになっています。解析では、1 番目のパラメーターに対しては全範囲の値の volatile 仮定が適用されませんが、2 番目のパラメーターが指している変数にはその仮定が引き続き適用されます。

void foo(volatile int x, volatile int *y_ptr) {
    x = 1;
    assert(x==1); 
    *y_ptr = 1;
    assert(*y_ptr==1); 
}

void foo_caller(void) {
    volatile int x;
    volatile int y;
    
    x = 1;
    assert(x==1); 
    
    y = 1;
    assert(y==1); 
    
    foo(x, &y);
}