オレンジ チェックの原因

[オレンジ ソース] ペインには、Code Prover 解析で複数のオレンジ チェック (未証明の結果) の原因となる可能性がある volatile 変数やスタブ関数などの制約なしのソースが表示されます。オレンジ ソースを制約すると、複数のオレンジ チェックにまとめて対処できます。[オレンジ ソース] ペインを表示するには、[結果の詳細] ペインで ボタンをクリックします。

オレンジ ソースは基本的に、コードから値を判断できない変数を示します。これらの変数は、呼び出しコンテキストが不明な関数への入力であるか、未定義の関数の戻り値である可能性があります。Code Prover では、これらの変数がそのデータ型で許容される全範囲の値を取るものと仮定されます。この広範な仮定が、それ以降のコードで 1 つ以上のオレンジ チェックの原因となる可能性があります。

The Orange Sources pane contains columns such as Source Type, Name, File, Line and Max Oranges.

たとえば、次の例では、関数 random_float が定義されていない場合、3 つの [オーバーフロー] のオレンジ チェックが発生します。

float random_float(void)
static void Close_To_Zero(void)
{
    float xmin = random_float();
    float xmax = random_float();
    float y;

    if ((xmax - xmin) < 1.0E-37f) { /* Overflow 1 */
        y = 1.0f;
    } else {
        /* division by zero is impossible here */
        y = (xmax + xmin) / (xmax - xmin); /* Overflows 2 and 3 */
    }
}
そのため、関数 random_float は、最大 3 つのオレンジ チェックの原因となるオレンジ ソースです。

[オレンジ ソース] ペインを使用すると、次のことができます。

  • 同じソースから発生したすべてのオレンジ チェックをレビューする。

    前述の例では、関数 random_float を選択すると、結果のリストには、このソースが原因で発生した 3 つのオレンジ チェックのみが表示されます。Filter Using Orange Sources (Polyspace Access)を参照してください。

  • 外部制約を指定するか、追加のコードを使用して、変数の範囲を制約する。オレンジ ソースの範囲を制約すると、過大近似に由来する複数のオレンジ チェックを削除できます。残りのオレンジ チェックは、コードの本当の問題を示します。

    前述の例では、random_float の戻り値を制約できます。

レビューを効率的に行うには、[オレンジの最大数] 列ヘッダーをクリックして、オレンジ ソースによって発生するオレンジ チェックの数でオレンジ ソースを並べ替えます。他のソースに対処する前に、オレンジ チェックの数が多いソースを制約します。

オレンジ ソースの制約

変数の範囲を制約して Polyspace® の既定の仮定を回避する方法は、オレンジ ソースのタイプによって異なります。

スタブ関数

Polyspace 解析で関数の定義を利用できない場合、関数がスタブ化されています。解析では、スタブ関数に関する複数の仮定が行われます。たとえば、スタブ関数の戻り値は、そのデータ型で許容される任意の値を取ることができます。

スタブ関数に関する仮定とこれらの仮定を回避する方法については、スタブ関数に関する Code Prover の仮定を参照してください。

volatile 変数

変数が volatile 指定子で宣言されている場合、解析では、変数がコード内の任意の位置でそのデータ型によって許容される任意の値を取ることができると仮定されます。

この仮定を回避するには、volatile 変数に関する Code Prover の仮定を参照してください。

extern 変数

変数が extern 指定子で宣言されており、コード内の他の場所では定義されていない場合、解析では、変数が最初の割り当て前にそのデータ型の範囲内の任意の値を取ることができると仮定されます。

変数が定義されている場所と、解析で定義を利用できない理由を判断します。たとえば、インクルード フォルダーを解析から除外している可能性があります。

main ジェネレーターによって呼び出される関数

コードに main 関数が含まれない場合、解析用の main 関数が生成されます。既定では、生成された main 関数は、そのデータ型で許容される任意の値を取ることができる入力を使用して、呼び出されていない関数を呼び出します。

詳細は、以下を参照してください。

main ジェネレーターによって初期化される変数

コードに main 関数が含まれない場合、解析用の main 関数が生成されます。既定では、グローバル変数は、生成された main によって呼び出された各関数で、最初の割り当て前はそのデータ型の範囲内の任意の値を取ることができます。

生成された main によってグローバル変数が初期化される方法については、グローバル変数の初期化に関する Code Prover の仮定を参照してください。

main ジェネレーターによって永続的な範囲に設定される変数

グローバル変数を永続モードで特定の範囲に明示的に制約すると、解析では、変数がコード内の任意の位置でこの範囲内にある任意の値を取ることができると仮定されます。

変数が永続的な範囲を取る方法の詳細は、Polyspace 解析の外的制約を参照してください。誤って永続的な範囲を割り当てていないか、または範囲を狭くして実際値を反映しなければならないかを確認します。

絶対アドレス

ポインターに絶対アドレスが割り当てられている場合、解析では、ポインターのデリファレンスによって潜在的な値の範囲がポインターのデータ型で決まると仮定されます。

絶対アドレスの使用と対応する Code Prover の仮定の例については、絶対アドレスの使用を参照してください。この仮定を削除して、絶対アドレスのすべての使用にフラグを設定するには、オプション -no-assumption-on-absolute-addresses を使用します。

場合によっては、複数のオレンジ ソースが 1 つのオレンジ チェックの原因となることがあります。オレンジ ソースを解消しても想定どおりにオレンジ チェックの表示が消えない場合、別のソースがチェックの原因となっていないかを検討してください。

参考

トピック