Polyspace Bug Finder の volatile 変数

volatile キーワードを使用して、明示的な書き込み操作が行われなくても、いつでも変数の値が変更される可能性があることをコンパイラに通知します。解析を実行すると、Polyspace® Bug Finder™ は volatile 変数について以下のように仮定します。

  • グローバル volatile 変数

    • グローバル volatile 変数を const として宣言すると、Polyspace は変数の初期化値、または初期化範囲 ([初期化モード] を [PERMANENT] に設定している場合) を使用して変数の範囲を外部で制約します。Polyspace は変数を読み取るときには毎回、初期化値または範囲を使用します。Polyspace 解析の外的制約を参照してください。

      たとえば、このコードでは次のようになります。

      const volatile volatile_var; // Global variable initialized to 0
const volatile volatile_var_10=10;
const volatile volatile_var_drs=3; // Variable constrained to range [-5 .. 5]

int func(void){
    int i= 10 % volatile_var; // Defect
    int j= 10 % volatile_var_10; // No defect
    int k= 10 % volatile_var_drs; // Defect
    return i+j+k;
}
      Polyspace は、volatile_var がゼロに初期化されることから、[整数のゼロ除算] の欠陥を検出します。また、Polyspace は volatile_var_drs でも [整数のゼロ除算] を検出します。これは外部で次の範囲に制約されているためです。[-5 ..5]。volatile_var_10 のすべての読み取りで、欠陥は発生しません。

    • 非 const グローバル volatile 変数については、Polyspace は変数の初期化値を無視し、変数のそれぞれの読み取りで入力は不明であると見なします。[入力モード] として [PERMANENT] を使用して変数の範囲を外部で制約する場合、Polyspace は変数のそれぞれの読み取りでこの範囲を使用します。Polyspace 解析の外的制約を参照してください。

      たとえば、このコードでは次のようになります。

      volatile volatile_var; // Global variable initialized to 0
volatile volatile_var_drs=3; // Variable constrained to range [-5 .. 5]

int func(void){
    int i= 10 % volatile_var; // No defect
    int j= 10 % volatile_var_drs; // Defect
    return i+j;
}

    Polyspace は、volatile_var_drs で [整数のゼロ除算] の欠陥を検出します。これは外部で次の範囲に制約されているためです。[-5 ..5]。volatile_var のすべての読み取りで、欠陥は発生しません。

  • ローカル volatile 変数

    Polyspace は、ローカル volatile 変数の初期化値を無視し、変数のそれぞれの読み取りで入力を不明であると見なします。たとえば、このコードでは次のようになります。

    int foo(void){
    volatile var=0;
    return 1/var; // No defect
}
    Polyspace は欠陥を検出しません。外部制約を使用してローカル変数の範囲を制約することはできません。

ランタイムが長くなる可能性はありますが、Polyspace が volatile 変数のそれぞれの読み取りですべての値を考慮する、より徹底的な解析を実行できます。[システムのすべての入力値を考慮する、さらに厳密なチェックを実行 (-checks-using-system-input-values)] を参照してください。このオプションを使用して上記のコードの例のすべてを解析すると、Polyspace は、ローカル volatile 変数の例を含め、コメント // No defect のラベルが付いた行でも [整数のゼロ除算] の欠陥を検出します。

参考

|