インライン (-inline)
関数呼び出しのたびに内部でクローンを作成しなければならない関数を指定
説明
このオプションは Polyspace® Code Prover™ 解析にのみ影響します。
関数呼び出しのたびに内部で検証のクローンを作成しなければならない、関数を指定します。
オプションの設定
以下のいずれかの方法を使用してオプションを設定します。
Polyspace ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [スケーリング] ノードを選択してから、このオプションの関数名を入力します。
Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [スケーリング] ノードを選択してから、このオプションの関数名を入力します。
コマンド ラインとオプション ファイル: オプション
-inlineを使用します。コマンド ライン情報を参照してください。
このオプションを使用する理由
-inline を使用して、関数呼び出しのたびに内部で関数のクローンを作成します。これにより、Polyspace Code Prover 内の解析の複雑度が低減される可能性があります。次のコードについて考えます。
void foo(int* p);
void bar(){
int* intP, intP2;
foo(intP);
foo(intP2)
}foo() と関数 bar() を解析します。オプション -inline が指定されなかった場合は、解析がポインター intP、ポインター intP2、およびパラメーター p の 3 つのオブジェクトを追跡します。オプション -inline を指定した場合は、関数呼び出しのたびに Polyspace が内部で foo のクローンを作成します。コードは実質上、次のようになります。void foo_clone1(int* p);
void foo_clone2(int* p);
void bar(){
int* intP, intP2;
foo_clone1(intP);
foo_clone2(intP2)
}foo_clone1() を解析するには、Polyspace が 3 つのオブジェクトではなく intP と p の 2 つのオブジェクトのみを追跡する必要があります。関数 foo_clone2() についても同じです。-inline を使用することにより、解析の複雑度が低減され、解析するコードの量が増加します。-inline を使用すると、解析するコードの量は増加するものの、解析の複雑度は低減される可能性があります。このオプションは、特定の状況におけるスケーリングの問題を解決するのに役立つ場合があります。テクニカル サポートから、このオプションを特定の関数に使用するように求められることがあります。このオプションを使用すると、Polyspace Code Prover チェックの色の意味が変わります。設定を参照してください。
同じ関数に対して複数の種類の呼び出しをする際に Code Prover チェックの色を区別するため、このオプションを使用しないでください。代わりに、オプション [状況依存性] (-context-sensitivity) を使用します。
設定
既定値なし
関数名を入力するか、一覧から選択します。
をクリックしてフィールドを追加し、関数名を入力します。
をクリックして、コード内の関数の一覧を表示します。その一覧から関数を選択します。
呼び出しのたびに、検証の内部で関数のクローンを作成します。たとえば、インライン化に対して関数 func を指定し、func を 2 回呼び出すと、内部で、検証用に func のコピーが 2 つ作成されます。
ただし、関数本体での実行時チェックのたびに、検証結果には色が 1 つだけ示されます。チェックの色のセマンティクスは、通常の仕様と異なります。
| チェック タイプ | オプション -inline を使用しない場合の結果の色 | オプション -inline を使用した場合の結果の色 |
|---|---|---|
| オレンジ チェック | 関数が 2 回呼び出され、その一方の呼び出しの演算で明確なエラーが引き起こされる場合、チェックの色はオレンジです。 | 関数が 2 回呼び出され、その一方の呼び出しの演算で明確なエラーが引き起こされる場合、チェックの色はダーク オレンジです。チェックは、結果のリストにオレンジ色の感嘆符とともに表示されます。 |
| グレー チェック | 関数が 2 回呼び出され、その一方の呼び出しで if ステートメントの分岐に到達できない場合、その分岐はグレーで表示されません。 | 関数が 2 回呼び出され、その一方の呼び出しで if ステートメントの分岐に到達できない場合、その分岐がグレーで表示されます。 |
インライン化された関数内の各チェックの下に、呼び出した状況に固有の情報が表示されます。たとえば、特定の関数呼び出しが明白なゼロ除算につながったことで [ゼロ除算] の横にオレンジ色の感嘆符が表示された場合は、その呼び出しとそれによって返される値を識別できます。
このオプションを、結果を理解するために使用しないでください。特定の関数がスケーリングの問題を引き起こす場合にのみ、このオプションを使用します。
ヒント
エイリアス検証で示されたヒントに基づいて、インライン化する関数を選択します。
mainを含め、このオプションをエントリ ポイント関数で使用しないでください。このオプションを使用すると、グレーの [到達不能コード] チェックの数が増加することがあります。
たとえば、以下のコードで [インライン] に
maxと入力すると、maxに対する呼び出しごとに、2 つの [到達不能コード] チェックが表示されます。int max(int a, int b) { return a > b ? a : b; } void main() { int i=3, j=1, k; k=max(i,j); i=0; k=max(i,j); }関数定義の前にキーワード
inlineを使用して、ヘッダー ファイルに定義を配置し、複数のソース ファイルから関数を呼び出した場合、結果はオプション [インライン] を使用した場合と同じになります。C++ コードの場合、このオプションはクラスのオーバーロードされたすべてのメソッドに適用されます。
コマンド ライン情報
パラメーター: -inline |
値: |
| 既定値なし |
例 (Code Prover): polyspace-code-prover -sources |
例 (Code Prover Server): polyspace-code-prover-server -sources |
