標準ライブラリ ルーチンの無効な使用チェックのレビューと修正

このトピックでは、Polyspace® Code Prover™ で [標準ライブラリ ルーチンの無効な使用] チェックの結果を体系的にレビューする方法を説明します。

[標準ライブラリ ルーチンの無効な使用] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。チェックおよびコードの例については、標準ライブラリ ルーチンの無効な使用を参照してください。

特にオレンジ チェックに対して、チェックが実際のエラーを表すのではなく、コードに該当しない Polyspace 前提条件を表していると判定できます。前提条件を緩和するのに解析オプションを使用できる場合、そのオプションを使用して検証を再実行します。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加できます。

すべてのチェックに適用される一般的なワークフローについては、Polyspace デスクトップ ユーザー インターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。

手順 1: チェック情報の解釈

[結果のリスト] ペインで、チェックを選択します。[結果の詳細] ペインで、チェックに関する詳細を確認します。チェックは無効な関数の引数のためレッドまたはオレンジです。

レッド チェックまたはオレンジ チェックの原因は使用する標準ライブラリ関数に依存します。次の表は、一般的に使用される関数の一部について考えられる原因を示しています。

関数レッド チェックまたはオレンジ チェックの原因
islower、isdigit および ctype.h でのその他の文字処理関数

引数の値は unsigned char 変数に許容された範囲外である可能性があります。

引数としてマクロ EOF を使用できます。

math.h 内の関数

ソフトウェアでは、複数の種類のエラーについて順番にチェックしていきます。各チェックは前のチェックにパスした実行パスについてのみ実行されます。

次にいくつかの例を示します。詳細および関数の一覧については、標準ライブラリの浮動小数点ルーチンの無効な使用を参照してください。

sqrt引数の値は負になることがあります。
pow最初の引数は負の可能性があり、2 番目の引数は非整数です。
exp、exp2 または双曲線関数引数が大きすぎて、結果が double で許容される値を超えている可能性があります。
log引数はゼロまたは負になることがあります。
asin または acos引数は [-1,1] の範囲外にある可能性があります。
tan引数の値は HALF_PI になることがあります。
acosh引数は 1 未満になる場合があります。
atanh引数は 1 より大きく、-1 未満である場合があります。
fprintf、fscanf およびその他のファイル処理関数ファイル ポインター引数は読み取り可能ではない場合があります。たとえば、引数が NULL の場合があります。
文字列引数を取る関数文字列引数は無効な文字列である可能性があります。たとえば、終了の '\0' で終わっていません。
memmove または memcpy この関数の 3 番目の引数は 2 番目の引数から最初の引数にコピーするバイト数を指定しています。この数値は最初または 2 番目の引数に割り当てられたメモリを超える可能性があります。

手順 2: Polyspace の前提条件へのチェックをトレース

コードの前方で発生する Polyspace 前提条件にオレンジ チェックをトレースできるかどうかを確認します。前提条件があてはまらない場合、結果またはコードにコメントまたは正当化情報を追加します。Polyspace ユーザー インターフェイスでのバグ修正または正当化による結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。

たとえば、値を未定義の関数から取得し、その値に sqrt 演算を実行するとします。ここで、次のようにします。

  1. Polyspace は、関数が負の値を返す可能性があると仮定します。

  2. したがって、sqrt 関数呼び出しで [標準ライブラリ ルーチンの無効な使用] オレンジ チェックが生成されます。

  3. 関数が正の値を返すことがわかっている場合、オレンジを回避するには関数の戻り値に制約を指定することができます。スタブ関数に関する Code Prover の仮定を参照してください。あるいは、コメントおよび正当化情報を追加し、コードを変更しなかった理由を説明します。

詳細については、Code Prover 解析の前提条件を参照してください。