状态窗格

“ 状态 ”窗格显示驱动程序、操作系统模型和规则中变量值的布尔表达式。 SDV 使用这些表达式来构造驱动程序、操作系统模型和规则的抽象，并在验证中使用它们。

以下屏幕截图显示了缺陷查看器中的示例 “状态 ”窗格。

“ 状态 ”窗格是缺陷查看器的一个组件。 当代码元素在 “跟踪树”窗格中突出显示，并在“ 源代码”窗格中突出显示相应的源代码行时，“ 状态 ”窗格将显示从 SDV 跟踪的驱动程序) 表达式集中的布尔表达式 (，这些表达式在执行代码行之前计算结果为 TRUE 。

跟踪布尔表达式

在验证驱动程序的每个规则时，SDV 跟踪一组布尔表达式。 “ 状态 ”窗格中显示的布尔表达式是该集中计算结果为 TRUE 的表达式。 如果“ 跟踪树 ”窗格中的元素更改了任何表达式的值，则 “状态 ”窗格的内容将更改为显示计算结果为 TRUE 的新表达式集。

解释状态窗格中的表达式

“ 状态 ”窗格中显示的大多数表达式都与规则代码中显而易见的变量相关。 可以在“源代码”窗格) 的 RuleName.slic 文件中使用规则 (源代码来帮助解释表达式。

但是，某些表达式显示在“ 状态 ”窗格中，其中没有任何有关其内部表示形式的详细信息，这可能会帮助你解释它们。 例如，

x!=x

对于 SDV，此表达式表示跟踪中此点变量 x 的值不等于跟踪中不同点处同一变量的值的条件。 使用驱动程序源代码、规则代码 (*.slic) ，以及 “跟踪树 ”窗格中的元素来帮助你解释表达式。

“状态”窗格中的“步骤”选项卡

“ 状态 ”窗格中的布尔表达式显示在选项卡上。 每个选项卡都表示验证中使用的所有源代码的跟踪步骤。 步骤选项卡上的数字表示该步骤在跟踪中的顺序。

通常，由于每行源代码仅表示跟踪中的一个步骤，因此“ 状态 ”窗格中只有一个步骤选项卡。 但是，复杂的代码可以生成许多步骤。

例如，以下屏幕截图显示了“状态”窗格，其中显示了包含函数指针的代码行。 在这种情况下，每个步骤选项卡表示指针的解析、指向函数的调用及其结果中的一个步骤。 (步骤选项卡数显示 SDV 解析函数 pointer 所需的步骤数。)

若要按顺序查看“ 状态 ”窗格中的每个步骤选项卡，请在“ 源代码 ”窗格中选择关联的代码行。 然后，重复单击“ 源代码 ”窗格中的代码行。 每次单击所选代码行时，SDV 都会显示“下一步”选项卡，直到你循环遍历所有步骤选项卡。 弯曲的黄色箭头指示所选步骤。

还可以单击“ 状态 ”窗格中的任意选项卡以查看其内容。

评论

SDV 通常跟踪“ 状态 ”窗格中未出现在规则中且似乎与规则不直接相关的表达式。 这些表达式源于 SDV 在尝试关联不同值和不同规则冲突时使用的复杂启发法。 在某些情况下，SDV 无法正确计算表达式。 在这些情况下，SDV 会提供一条消息，指出当前状态未知，并显示具有最后一个已知状态的步骤中的表达式。 有关说明，请参阅以下代码示例：

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