How to View SDV Reports

After SDV completes a verification, it produces a report of the defects it detected. For each defect, SDV generates a Defect Viewer, which is a set of windows that display a trace of the path to the defect. You can view the list of defects in the Static Driver Verifier Report Page, where you can open Defect Viewer to examine SDV results.

In some cases, a defect trace leads to a defective C statement that can be seen as the root cause of the defect. In more complicated cases, the defect root cause cannot be associated with a single C statement. For example, consider the imaginary rule discussed in "Under the Hood: How the SDV Verification Engine Works" earlier in this chapter:

• If a path in a driver violates this rule, SDV might find the path but be unable to determine whether the violation was caused by a call to MyFunctionA or a call to MyFunctionB.

• However, this defect will be associated with a pair of statements: a call to MyFunctionB followed by a call to MyFunctionA.

To Open the SDV Report

1. In a build environment window, type the following:

   • staticdv /view

2. In the Static Driver Verifier Report Page, double-click a rule name under the Defect(s) node to review information about the defect in Defect Viewer.

SDV displays the violated rules under the Defect(s) node in the Results pane. Figure 24-1 shows a sample SDV report for the verification of the BufAfterReq* rules on the KMDF Fail_driver6 sample driver.

Figure 24-1: Results pane in an SDV report

SDV results appear as a multilevel list of nodes. Nodes are shown by icons with text messages. The upper level nodes stand for result categories, the most important of which are Passed, Defect, Timeout, Spaceout, Not Applicable, and Uncertain. The lower level nodes show results per rule. Figure 24-2 shows all possible node icons with their meanings.

Figure 24-2: Icons used in SDV results

 Tip  See "Results Pane" in the WDK for details about the Results pane icons, plus information about how to use the Results pane-online at http://go.microsoft.com/fwlink/?LinkId=80081.

About SDV Defect Viewer

In Figure 24-3, Defect Viewer displays information about a violation of the FDOPowerPolicyOwnerAPI rule in the KMDF Fail_Driver3 sample driver. See "Example: Walkthrough SDV Analysis of Fail_Driver3" later in this chapter for steps to build and verify this driver by using SDV.

Figure 24-3: A rule violation in SDV Defect Viewer

In Figure 24-3, the numbers refer to these elements, which provide information about the results:

1. The Trace Tree pane on the top left displays a trace of the critical elements of the source code that were executed in the path to the rule violation.

2. The Source Code pane in the center highlights the corresponding line of code as you step through the source code in the Trace Tree pane, where trace fragments are displayed in red.

   Each tab for the Source Code pane represents a step in the trace through all the source code in the verification. The number of the tab represents the order of that step in the trace.

3. The State pane at the bottom left displays Boolean expressions on tabs for the values of variables in the driver, the SDV operating system model, and the rule.

   SDV uses these expressions to construct the Boolean abstraction used in the verification. If the source code element selected in the Trace Tree or Source Code panes changes the values of the variables in such a way that some of the Boolean expressions also change their values, then those changes appear automatically in the State pane.

4. The status bar at the bottom of the window presents a description of the defect.

5. The Results pane was described earlier in Figure 24-1.

 Tip  See "Defect Viewer" in the WDK for details about how to use Defect Viewer to filter and manage SDV results-online at http://go.microsoft.com/fwlink/?LinkId=80066.

Best Practice: Check SDV Results

Tip 

In some cases, SDV reports errors that you might believe cannot actually occur-sometimes called "false positives." However, a false positive usually indicates that the code is ambiguous in some way and depends on assumptions that you might know to be valid but that SDV cannot verify. You should always investigate false positives to determine whether your assumptions are justified. As a best practice:

• If the error is a false positive, add a code comment that tells subsequent developers that the issue had been considered.

• If the error is a genuine defect, either fix it immediately or, if the root cause is not clear, investigate and test the driver's behavior along the defect trace that SDV reported.

 SDV known issues  If SDV reports an error that you think is inaccurate, review the SDV limitations and look for known issues that might prevent SDV from correctly interpreting the driver code. Specifically, SDV:

• Assumes that the statically declared type of a pointer is always correct and accurately reflects its actual dynamic type.

• Does not recognize that 32-bit integers are limited to 32 bits.

  As a result, SDV does not detect overflow or underflow errors.

• Uses 31 bits to represent integers.

  This limitation can result in both false negative and false positive results.

• Ignores pointer arithmetic.

  For example, SDV misses situations in which a pointer is incremented or decremented. This limitation can result in false negative and false positive results.

• Ignores unions.

• Ignores bit-level operations.

  This imprecision can result in false positive and false negative results.

• Ignores casting operations.

  SDV misses both errors that are solved by recasting and errors that are caused by casting. For example, SDV assumes that an integer that is recast as a character still has the integer value.

• Cannot verify driver callback functions that are declared as static.

  To avoid this problem, remove the static keyword from the declaration.

• Does not interpret structured exception handling and does not analyze the expression or the exception handler code.

  For __try/__except statements, SDV analyzes the guarded section as if no exception is thrown, but does not analyze the expression or the exception handler code, as shown in the following example:

   // The try/except statement __try {    // guarded section } __except (expression) {    // exception handler } 

  For __try/__finally statements, SDV analyzes the guarded section and then the termination handler as if no exception is thrown, as shown in the following example:

   // The try/finally statement __try {    // guarded section } __finally {    // termination handler } 

  For both __try/__except and __try/__finally statements, SDV ignores the leave statement.

• Cannot interpret driver callback functions that are defined in an export driver where the export driver has a module-definition (.def) file that hides the driver dispatch function.

  To avoid this issue, add the driver dispatch function to the EXPORTS section of the .def file.

 Tip  See "Static Driver Verifier Limitations" in the WDK for details-online at http://go.microsoft.com/fwlink/?LinkId=80086.