次の方法で共有


静的ドライバー検証ツールのレポートの使用

SDV レポートは、検証結果の対話型の表示です。 このセクションでは、SDV レポートを使用して、ドライバーでコーディング エラーを見つける方法について説明します。 レポート、ウィンドウの機能、およびウィンドウ内の要素の詳細については、「静的ドライバー検証ツール レポート」を参照してください。

静的ドライバー検証ツールの欠陥ビューアーを開く

SDV が結果ウィンドウで "欠陥" (規則違反) を報告した場合は、静的ドライバー検証ツール レポートの [欠陥ビューアー] ウィンドウで違反に関連するコードを表示できます。 [欠陥ビューアー] ウィンドウには、規則違反のパスにコードが表示されます。 違反したルールごとに 1 つの欠陥ビューアー ウィンドウがあります (一度に表示できる欠陥ビューアー ウィンドウは 1 つだけです)。

欠陥ビューアー ウィンドウを開いてディフェクトを表示するには:

  • [欠陥] ノードの下の一覧からルールを選択します。

Red circle icon with a white X, representing a defect.

この手順は、欠陥に対してのみ機能します。 検証の結果が、パス、タイムアウト、スペースアウト、該当しない、その他の非欠陥の結果などの欠陥でない場合、SDV は欠陥ビューアー ウィンドウを生成しません。

次のスクリーン ショットは、静的ドライバー検証ツール レポート ページを示しています。

Screenshot of a Static Driver Verifier Report page.

ルールの確認

コードで規則違反を見つけようとする前に、ドライバーが違反した規則を理解しておいてください。

[ 静的ドライバー検証ツールの規則] セクションには、CancelSpinLock などの 各ルールについて説明するトピックが含まれています。

ルールのコードを表示するには、 静的ドライバー検証ツール レポートの [ソース コード ] ウィンドウで、CancelSpinLock.slic などのルール コードを含むタブをクリックします。

たとえば、ドライバーが IoAcquireCancelSpinLock または IoReleaseCancelSpinLock を呼び出した場合、またはドライバーがスピン ロックを解放する前にルーチンを終了した場合、CancelSpinLock ルールに違反します。

ディフェクト パスをトレースする

[欠陥ビューワー] ウィンドウが開くと、[トレース ツリー] ウィンドウ内の、欠陥パス内の最初の重要なドライバー呼び出しを表す要素が選択されます。 [ソース コード] ウィンドウで、関連付けられているソース コード行が青色で強調表示されます。

次のスクリーン ショットは、Fail_Driver1 サンプル ドライバーによる CancelSpinLock ルール違反の静的ドライバー検証ツールの 欠陥ビューアーウィンドウの開いているビューを示しています。 この例では、CancelSpinLock 規則の違反へのパスの最初のドライバー呼び出しは、ドライバーの DispatchSystemControl ルーチンの IoAcquireCancelSpinLock への呼び出しです。

Screenshot of the opening view of the Static Driver Verifier Defect Viewer window for a CancelSpinLock rule violation.

ソース コード ペインの使用

ソース コード ウィンドウ には、検証で使用されるソース ファイルが表示されます。 トレース ツリーペインの要素を選択すると、その要素に関連付けられているソース コード ファイルが、隣接するソース コード ウィンドウのファイル スタックの上部に表示されます。 別のソース ファイルを表示するには、ソース コードウィンドウでソース ファイルのタブをクリックします。

次のスクリーン ショットは、ソース コード ウィンドウを示しています。 このソース コードペインで、淡い青色で強調表示されているコード行は、トレース ツリー ペインで選択した要素に関連付けられているコード行です。

Screenshot of the Source Code pane in the Static Driver Verifier Defect Viewer.

欠陥へのパスで実行されるドライバー コードの行は、赤いテキストで表示されます。 この例の 116 行目や 118 行目など、赤いテキストの行だけを見ると、特にこの例で使用されているような単純な欠陥が見えることがあります。 この場合、ドライバーはスピン ロックを取得し、スピン ロックを解放せずにディスパッチ ルーチンから戻ります。

トレースを 1 つずつ実行する

トレースを開始するには、トレース ツリー ウィンドウで要素を選択し、↓ キーを押します。 ↓キーを押すたびに、トレース ツリー ペインの次の要素が選択されます。

トレース ツリー ウィンドウで要素をステップ実行する際は、ソース コード ウィンドウでドライバー コードの要素を確認します。 折りたたまれたコードセクションを展開するには、→ キーを押します。 コードの展開されたセクションを折りたたむには、← キーを押します。 カーソルは、折りたたまれているすべてのコード セクションをスキップします。

トレース ツリー ペイン内の要素を下にスクロールすると、選択した要素が生成されたソース コード ファイルが ソース コード ウィンドウのファイル スタックの先頭に移動し、関連付けられているコード行が強調表示されます。

次のスクリーン ショットは、トレース ツリー ウィンドウと ソース コード ペインを含む静的ドライバー検証ツールの欠陥ビューアーを示しています。

Screenshot of a Static Driver Verifier Report page with Trace Tree and Source Code panes.

ルール ファイルと状態 ウィンドウを使用する

状態ウィンドウを使用すると、検証中に SDV が追跡する変数の値を表すブール式のセットを表示できます。

[状態] ウィンドウに表示されるブール式は、そのセット内で TRUEに評価される式です。 トレース ツリー ウィンドウの要素によっていずれかの式の値が変更された場合、状態 ウィンドウの内容は、TRUE に評価される式の新しいセットを表示するように変更されます。

トレース ツリー ペインをステップ 実行すると、SDV がこれらの変数の値を使用して、ルール ファイル (*.slic) で使用される式を評価する方法を確認できます。

静的ドライバー検証ツール レポート ページの次のスクリーン ショットは、ドライバーが以前にスピン ロックを取得したかどうかを SDV テストで示す方法を示しています。 SDV は、ドライバーが以前にスピン ロックを取得したかどうかを確認するテスト、つまり、s 変数の値が 1 の場合、ロックされていることを意味します。 この場合、状態ウィンドウに表示される s!=1 (ロック解除済み) であるため、SDV は s の値を 1 に設定し、ロックが取得されたことを示します。

Screenshot of a Static Driver Verifier Report page showing SDV tests for previously acquired spin lock.

ABORT ルーチンを検索する

ドライバー コードが規則に違反すると、トレース ツリー ペインには、欠陥を報告するための ABORT ルーチンが含まれます。

欠陥へのコード パスが長く複雑な場合は、ABORT ルーチンが見つかるまでトレース ツリー ペインを下にスクロールし、上方向キーを使用して欠陥レポートを最もすぐにトリガーしたコードを見つけると便利です。

たとえば、次のスクリーン ショットに示すように、ABORT ルーチンは CancelSpinLock.slic ファイルの行に関連付けられています。このファイルは、ロックが取得されたかどうかをテストした後に欠陥を報告します (s==locked)。 このテストは、ディスパッチ ルーチンの終了時に実行されるサブルーチンの一部です。 この情報から、ドライバーがディスパッチ ルーチンから戻る前にスピン ロックを解放できなかったことを推測できます。

Screenshot of a Static Driver Verifier Report page showing the ABORT routine associated with a line from the CancelSpinLock.slic file.

静的ドライバー検証ツールの欠陥ビューアーを閉じる

欠陥の原因となったコード エラーを特定したら、現在のルールの 静的ドライバー検証ツールの欠陥ビューアー ウィンドウを閉じ、別のルールの 欠陥ビューアー を開くことができます。

ルールの欠陥ビューアーを閉じるには:

  • ファイルメニューの退出を選択します。

欠陥ビューアー閉じるボタン (X) をクリックすることもできます。 静的ドライバー検証ツール レポートの 閉じるボタン (X) のすぐ下にあります。

次のスクリーン ショットは、欠陥ビューアーを閉じる方法を示しています。

Screenshot demonstrating how to close the Defect Viewer for a rule in Static Driver Verifier.