次の方法で共有


[状態] ウィンドウ

[状態] ウィンドウには、ドライバーの変数値のブール式、オペレーティン グシステム モデル、およびルールが表示されます。 SDV は、これらの式を使用して、ドライバー、オペレーティング システム モデル、および規則の抽象化を構築し、検証に使用します。

次のスクリーン ショットは、欠陥ビューアーで [状態] ウィンドウの例を示しています。

Screenshot of the State pane in the Defect Viewer.

[ソース コード] ウィンドウは、欠陥ビューアーのコンポーネントです。 [トレース ツリー] ウィンドウでコード要素が強調表示されており、[[ソース コード] ウィンドウで対応するソース コード行が強調表示されている場合、[状態] ウィンドウには、コード行が実行される前にTRUEと評価されるブール式 (sdv がドライバーを追跡する式のセット) が表示されます。

ブール式の追跡

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

[状態] ウィンドウでの式の解釈

[状態] ウィンドウに表示されるほとんどの式は、ルール コードに示されている変数に関連付けられています。 ルールのソース コード ([ソース コード] ウィンドウの RuleName ファイル) を使用して、式を解釈することができます。

ただし、一部の式は[状態] ウィンドウに表示され、内部表現の詳細が含まれていなくても、それらを解釈するのに役立つものがあります。 たとえば、 にします。

x!=x

SDV に対して、この式は、トレース内におけるこの位置の変数値 x が、トレース内の別位置にある同じ変数の値と等しくない条件を表します。 ドライバーのソースコード、ルールコード (* slic)、トレース ツリー ペインの要素を使用して、式を解釈します。

[状態] ウィンドウのステップ タブ

[状態] ウィンドウのブール式は、タブに表示されます。 各タブは、検証で使用されるすべてのソース コードを通じて、トレースの 1 つのステップを表します。 [ステップ] タブの数値は、トレース内のそのステップの順序を表します。

通常、ソース コードの各行はトレース内の 1 つのステップのみを表すため、[状態] ウィンドウには [ステップ] タブが 1 つだけ表示されます。 ただし、複雑なコードでは、多くのステップを生成できます。

たとえば、次のスクリーン ショットは、関数ポインターを含むコード行を表示する [状態] ウィンドウを示しています。 この場合、各 [ステップ] タブは、ポインターの解決、ポイント先関数の呼び出し、その結果おけるステップを表します。 ([ステップ] タブの数は、SDV が関数ポインターを解決するために必要なステップの数を表示します)。

Screenshot of the State pane displaying a line of code with a function pointer.

[状態] ウィンドウの各 [ステップ] タブを順番に表示するには、[ソース コード] ウィンドウで関連するコード行を選択します。 次に、 [ソース コード] ウィンドウでコード行を繰り返しクリックします。 選択したコード行をクリックするたびに、次の [ステップ] タブが表示され、すべての [ステップ ]タブが表示されます。 黄色の曲線矢印は、選択したステップを示します。

Icon of a curved yellow arrow indicating the selected step.

また、[状態] ウィンドウで任意のタブをクリックして、そのコンテンツを表示することもできます。

コメント

多くの場合、SDV は、ルールには表示されず、ルールに直接関連していないと思われる、 状態 ウィンドウ内の式を追跡します。 これらの式は、SDV が異なる値や異なる規則違反を関連付けるために使用する高度なヒューリスティックの結果になります。 場合によっては、SDV が式を正しく評価できないことがあります。 このような場合、SDV では、現在の状態が不明であることを示すメッセージが表示され、最後の既知の状態のステップからの式が表示されます。 説明については、次のコード例を参照してください。

Unknown state. Last known state from step 120.
sdv irql current ==2
sdv irql current!=1
sdv irql current!=0