使用静态驱动程序验证程序报告

SDV 报告是验证结果的交互式显示。 本部分介绍如何使用 SDV 报告在驱动程序中查找编码错误。 有关报表、窗口功能和窗口中元素的详细信息,请参阅 静态驱动程序验证程序报告

打开静态驱动程序验证程序缺陷查看器

如果 SDV 在“ 结果 ”窗格中) 报告了任何“缺陷” (规则冲突,则可以在静态驱动程序验证程序报告的 “缺陷查看器 ”窗口中查看冲突所涉及的代码。 “缺陷查看器”窗口显示规则冲突路径中的代码。 违反的每个规则都有一个 缺陷查看器 窗口, () 一次只能查看一个 缺陷查看器 窗口。

打开缺陷的“缺陷查看器”窗口:

  • 从“ 缺陷” () 节点下的列表中选择一个规则。

带有白色 X 的红色圆圈图标,表示缺陷。

此过程仅适用于缺陷。 如果验证的结果不是缺陷(例如通过、超时、空格、不适用或任何其他非缺陷结果),SDV 不会生成缺陷 查看器 窗口。

以下屏幕截图显示了“静态驱动程序验证程序报告”页。

“静态驱动程序验证程序报告”页的屏幕截图。

查看规则

在尝试在代码中查找规则冲突之前,请先熟悉驱动程序违反的规则。

“静态驱动程序验证程序规则”部分包含一个介绍每个规则的主题,例如 CancelSpinLock

若要查看规则的代码,请在静态驱动程序验证程序报告的“ 源代码 ”窗格中,单击包含规则代码的选项卡,例如 CancelSpinLock.slic。

例如,如果驱动程序按顺序调用 IoAcquireCancelSpinLockIoReleaseCancelSpinLock,或者驱动程序在释放旋转锁之前退出例程,则会违反 CancelSpinLock 规则。

跟踪缺陷路径

“缺陷查看器 ”窗口打开时,将选中“ 跟踪树 ”窗格中表示缺陷路径中第一个关键驱动程序调用的元素。 在“ 源代码 ”窗格中,关联的源代码行以蓝色突出显示。

以下屏幕截图显示了 静态驱动程序验证程序缺陷查看器 窗口的打开视图,该窗口显示Fail_Driver1示例驱动程序违反 CancelSpinLock 规则的情况。 在此示例中,违反 CancelSpinLock 规则的路径中的第一个驱动程序调用是调用驱动程序的 DispatchSystemControl 例程中的 IoAcquireCancelSpinLock

“静态驱动程序验证程序缺陷查看器”窗口的打开视图的屏幕截图,其中显示了 CancelSpinLock 规则冲突。

使用“源代码”窗格

源代码”窗格 显示验证中使用的源文件。 选择“ 跟踪树 ”窗格中的元素时,与该元素关联的源代码文件将显示在相邻的“ 源代码 ”窗格中文件堆栈顶部。 若要查看其他源文件,请单击“ 源代码 ”窗格中源文件的选项卡。

以下屏幕截图显示了“源代码”窗格。 在此 “源代码 ”窗格中,以淡蓝色突出显示的代码行与 “跟踪树 ”窗格中的选定元素相关联。

静态驱动程序验证程序缺陷查看器中“源代码”窗格的屏幕截图。

驱动程序代码中在缺陷路径中执行的行以红色文本显示。 通过只查看红色文本行(如本示例中的第 116 行和第 118 行),有时可以看到缺陷,尤其是此示例中使用的简单缺陷。 在这种情况下,驱动程序获取旋转锁,然后从调度例程返回,而不释放旋转锁。

单步执行跟踪

若要开始跟踪,请在“ 跟踪树 ”窗格中选择一个元素,然后按向下键。 每次按向下键时,都会选择“ 跟踪树 ”窗格中的下一个元素。

单步执行“跟踪树”窗格中的元素时,watch驱动程序代码中元素的“源代码”窗格。 若要展开代码的折叠部分,请按向右键。 若要折叠展开的代码部分,请按向左键。 游标跳过代码的所有折叠部分。

在“ 跟踪树 ”窗格中向下滚动元素时,所选元素源自的源代码文件将移动到“ 源代码 ”窗格中文件堆栈的顶部,并突出显示关联的代码行。

以下屏幕截图显示了带有“跟踪树”和“源代码”窗格的静态驱动程序验证程序缺陷查看器。

“静态驱动程序验证程序报告”页的屏幕截图,其中包含“跟踪树”和“源代码”窗格。

使用规则文件和状态窗格

可以使用 状态窗格 查看一组布尔表达式,这些表达式表示 SDV 在验证期间跟踪的变量的值。

状态 ”窗格中显示的布尔表达式是该集中计算结果为 TRUE 的表达式。 如果“跟踪树”窗格中的元素更改了任何表达式的值,则 “状态 ”窗格的内容将更改为显示计算结果为 TRUE 的新表达式集。

单步执行 “跟踪树 ”窗格时,可以观察 SDV 如何使用这些变量的值来评估规则文件 (*.slic) 中使用的表达式。

以下“静态驱动程序验证程序报告”页的屏幕截图显示了 SDV 测试如何指示驱动程序以前是否获取了旋转锁。 SDV 测试驱动程序之前是否获取了旋转锁,即 s 变量的值是否为 1,这意味着已锁定。 在这种情况下, s!=1 (未锁定) ,如 “状态”窗格中所示,因此 SDV 将 的值 设置为 1,指示已获取锁。

静态驱动程序验证程序报告页的屏幕截图,其中显示了以前获取的旋转锁的 SDV 测试。

查找 ABORT 例程

当驱动程序代码违反规则时,“ 跟踪树 ”窗格包含用于报告缺陷的 ABORT 例程。

如果缺陷的代码路径很长且复杂,通常最好在“ 跟踪树 ”窗格中向下滚动,直到找到 ABORT 例程,然后使用向上键查找最直接触发缺陷报告的代码。

例如,如以下屏幕截图所示,ABORT 例程与 CancelSpinLock.slic 文件中的一行相关联,该行在测试是否 (s==locked) 获取锁后报告缺陷。 测试是调度例程结束时执行的子例程的一部分。 根据此信息,可以推断驱动程序在从调度例程返回之前未能释放旋转锁。

静态驱动程序验证程序报告页的屏幕截图,其中显示了与 CancelSpinLock.slic 文件中的一行关联的 ABORT 例程。

关闭静态驱动程序验证程序缺陷查看器

确定导致缺陷的代码错误后,可以关闭当前规则的 “静态驱动程序验证程序缺陷查看器 ”窗口,然后打开其他规则的 缺陷查看器

关闭规则的缺陷查看器:

  • 在“ 文件 ”菜单中,选择“ 退出”。

还可以单击缺陷查看器 (X) 的“关闭”按钮。 它位于静态驱动程序验证程序报告的“ 关闭 ”按钮 (X) 下方。

以下屏幕截图显示了如何关闭缺陷查看器。

演示如何在静态驱动程序验证程序中关闭规则的缺陷查看器的屏幕截图。