このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
手動スタブと手動の main() 関数を使用した Polyspace 解析の変数範囲の制約
このトピックは主に Polyspace® Code Prover™ 解析に適用されます。
Polyspace Code Prover 解析から最も精度が高い結果を得るには、解析対象となるプログラムをできるだけ完全なものにしておく必要があります。しかし、複数の理由により、解析のために完全なプログラムを提供できない場合もあります。完全なアプリケーションであっても、外部入力に対する制約など、一部の情報はプログラムの外部に存在します。このトピックでは、不完全なアプリケーションであっても精度の高い結果を得ることができるように、解析に制約を設定する方法を示します。
より単純な制約では、制約を指定するためのグラフィカル インターフェイスが Code Prover で提供されます。たとえば、Polyspace 解析の外的制約の指定を参照してください。ご使用のコンテキストにおいてインターフェイスのオプションでは不十分で、解析をさらに微調整する必要がある場合は、プログラム境界の詳細を明示的に定義することができます。このトピックでは、プログラム境界の定義を始めるための概念的枠組みを示します。
プログラム境界における変数範囲に関する Code Prover の仮定
Polyspace Code Prover 解析では、正常な結果を得るために、プログラム境界における変数範囲に関して仮定を行う必要があります。
Polyspace Code Prover がプログラムの解析を行うと、特定のタイプのランタイム エラーを発生させる可能性があるすべての操作がチェックされます。1 .この目的は、チェック対象となった操作がランタイム エラーを引き起こさないこと、あるいは確実にランタイム エラーを引き起こすことを数学的に証明することです。解析でエラーの有無を証明できない場合、手動で検査するために、その操作がオレンジで強調表示されます。これらのオレンジ チェックの一部は、ランタイム エラーの可能性を示しています。ただし、解析のセットアップ方法によっては、ほとんどのオレンジ チェックの原因が、解析時におけるアプリケーションに関する情報不足である場合があります。PolyspaceCode Prover のオレンジ チェックも参照してください。
Polyspace Code Prover 解析から証明済みの解析結果を最も多く取得するには、解析対象となるプログラムをできるだけ完全なものにしておく必要があります。しかし、複数の理由により、解析のために完全なアプリケーションを提供できない場合もあります。たとえば、ライブラリのロバスト性を解析している場合や、完全なアプリケーションが大きすぎるために Code Prover 解析がアプリケーションに対応できない場合です。このような場合、解析対象となるプログラム モジュールは次の 2 つの原因により不完全となる可能性があります。
アプリケーションのエントリ ポイントを定義する
main()関数がない。解析にすべての関数実装を利用できるわけではない。たとえば、解析対象のプログラム モジュールが、解析に提供されていない別のモジュールで定義された関数を呼び出している場合があります。
次の単純なプログラム モジュールについて考えます。
#include <stdint.h>
int8_t getAnInput(void);
int32_t calculateSum(int32_t numberToProcess) {
int32_t sum = 0;
for(int32_t i = 0; i <= numberToProcess; i++) {
sum += getAnInput();
}
return sum;
}関数
getAnInput()の実装。関数
calculateSum()の呼び出しコンテキスト。
解析対象となるプログラムが不完全である場合、Code Prover は、解析を引き続き行うために main() 関数と未定義の関数に関して特定の仮定を行います。この仮定の範囲は、正常な結果を得るには十分に広範ですが、実際のコンテキストにおいては広範すぎる可能性があります。たとえば、ある関数が定義されていない場合、Code Prover はその関数の戻り値の型に基づき、候補となる戻り値の範囲を仮定します。前述の例では、Code Prover は int8_t データ型に基づいて getAnInput() の戻り値の範囲が [-128, 127] であると仮定します。しかしこの場合、広い範囲の値が仮定されていますが、実際に関数が返す値はそれより狭い範囲になる可能性があります。
手動 main() と手動スタブを定義してプログラム境界における範囲を制約する
通常、Code Prover の解析オプションを使用してプログラム境界を制約することができます。たとえば、calculateSum() への入力や getInput() の戻り値を制約する場合、オプション [制約の設定] (-data-range-specifications) を使用できます。ただし、このオプションがサポートするのは特定のタイプの制約です。より複雑な制約を指定する場合は、独自のスタブと main() を定義する必要があります。
次の情報が既知であるとします。
calculateSum()は、常に 100 以下の正の引数で呼び出される。getAnInput()は、0 の値、または 10 から 30 まで (10 と 30 を含む) の値を返す。
次の制約範囲を指定できます。
calculateSum()への入力に対して範囲 [1,100]。この範囲を指定するために、
calculateSum()を呼び出す手動main()を定義できます。getAnInput()の戻り値に対して範囲 0 ∪ [10, 30]。この範囲を指定するには、関数
getAnInput()に対して手動スタブを定義できます。
手動 main() と手動スタブは元のプログラム モジュールとは別のファイルで定義して、これらのファイルを Code Prover 解析に提供できます。
手動 main() の定義
関数 calculateSum() への入力に制約を課すには、制約された引数を使って calculateSum() を呼び出す main() 関数を定義します。この main() 関数は次のような単純なものにできます。
#include <stdint.h>
int32_t calculateSum(int32_t numberToProcess);
extern int32_t arg_calculateSum;
void main() {
int32_t sum;
unchecked_assert(arg_calculateSum >= 1 && arg_calculateSum <= 100);
sum = calculateSum(arg_calculateSum);
}unchecked_assert マクロに続き、このアサーションがこのブロック内の残りのコードに当てはまるという仮定で検証が行われます。そのためこの例では、calculateSum() への入力の範囲が [1,100] に制約されていると仮定して検証が行われます。手動スタブの定義
getAnInput() の戻り値に制約を課すには、この関数から値が返される前に、外部変数の範囲を制約するスタブを定義します。スタブは次のようになります。
#include <stdint.h>
extern int8_t arg_getAnInput;
int8_t getAnInput(void) {
unchecked_assert(arg_getAnInput == 0 || (arg_getAnInput >= 10 && arg_getAnInput <= 30));
return arg_getAnInput;
}
制約が実際に適用されることをチェックするには、手動 main() と手動スタブを設定した場合と設定しなかった場合のそれぞれのプログラム モジュールを検証します。前者の場合、2 つのオレンジのオーバーフローが表示されますが、制約が適用されると緑に変わります。ソース コード ツールヒントを使用して、制約の適用を検証することもできます。ツールヒントの詳細については、Code Prover 解析後のソース コード ツールヒントでの変数の範囲を参照してください。
参考
制約の設定 (-data-range-specifications)
トピック
1 A Code Prover analysis checks all operations for run-time errors, but subject to verification assumptions. In particular, if the same value causes run-time errors in successive operations on an execution path, to avoid duplication of review efforts, only the first error is shown. See also レッド チェックおよびオレンジ チェック以降の Code Prover 解析.
