Edit

Share via

Passing and Failing a Verification

  • Article

The SDV verification of a rule has three basic results:

  • The driver passes the verification.

  • The driver fails the verification.

  • The result is inconclusive.

Before drawing any conclusions based on these results, you should understand each result and be aware of the many qualifications that they entail. You should not judge any result to be a final or complete evaluation of the driver.

Verification Results

A driver passes a SDV verification when, after exploring all relevant execution paths in the driver's code, the SDV verification engine cannot prove that the driver violated a rule that was selected for verification.

A driver fails a verification when the SDV verification engine proves that the driver violated a rule at least once. The violation is known as a defect. If the driver violated a rule more than once, SDV reports multiple defects.

A verification is inconclusive if it terminates before it completes because of timeouts (a Timeout result) or a memory shortage (a Spaceout result), or when SDV could not reach a passing or failing conclusion (an Uncertain result). Also, SDV might have encountered internal tool errors that prevent it from completing its tasks. (For more information about the results, see Interpreting Static Driver Verifier Results.)

When a rule does not apply to the driver, for example, if the driver does not make use of the device driver interfaces that the rule verifies, SDV reports that the rule is Not Applicable.