Library Processing in Static Driver Verifier
Many drivers depend on dynamically and statically linked libraries of functions. Typically, the libraries include general processing functions, but in some situations, they include functionality that is integral to the driver.
Libraries are essential for determining whether the driver complies with interface rules. For example, without library code, a driver might appear to have missed a required call that is included in the library. Or, the library might include a call that the driver duplicates, causing a repeat error, such as releasing a lock twice.
To include a library in the verification of a driver, SDV must first process the library to prepare it for use in verifying the driver.
SDV tries to automatically detect and process all libraries on which the driver depends, but because it does not know the location of some library source files, it cannot automatically process these libraries and include them in the driver verification. When SDV detects a library dependency but cannot find the library code, it displays a warning message: "Process <library name>". You can respond by clicking the Libraries tab and click Add Library to process the libraries.
After SDV has processed a library, it retains its processing files for that library and automatically includes the library code in verifications of all drivers that require the library. You do not need to reprocess the library unless the library code changes. For instructions on reprocessing a library, see Reprocessing a Library.
This section includes:
SDV includes processed library files for system libraries. You do not need to direct SDV to process these libraries. When SDV detects that a driver depends on these libraries, it uses its processed files for these libraries without displaying a warning message. For information about library requirements, see Determining if Static Driver Verifier supports your driver or library.