PREfast for Drivers

PREfast for Drivers (PFD), an extension of PREfast, is a compile-time static verification tool that detects errors missed by the compiler and by conventional runtime testing. It detects common coding errors in C and C++ programs, and is designed to detect errors in kernel-mode driver code. You can run PFD very early in the development cycle—as soon as the code compiles correctly. PFD is integrated into the Windows 7 build environments in the Windows Driver Kit (WDK) as well as into Windows Automated Code Review (known as OACR). PFD supports a large vocabulary of annotations beyond those supported for generic PREfast, including annotations for IRQLs, resource-object leaks, memory leaks, and stricter type checking.

PREfast for Drivers examines each function in the code independently, looking for common driver errors and unwise coding practices. PFD runs quickly, even on larger drivers, and generates a report that identifies the line of driver code with the suspected error.

PREfast for Drivers runs on Windows XP and later versions of Windows and is designed to analyze code written for x86-based and x64-based platforms. It can analyze C and C++ source files for drivers in any driver model, including managed code.

You should use PREfast for Drivers in conjunction with Driver Verifier, Static Driver Verifier, and the checked build of Windows to ensure that your driver code is safe and reliable.

PREfast for Drivers is provided in the Windows Driver Kit (WDK).

What’s New for PFD in Windows 7

PFD now supports a broader range of expressions for analysis, such as const, member names, and, ‘side effect–free’ C expressions.

PFD now has better annotation error checking.

PFD now has improved defect detection, including “banned API” checking.

PFD now generates warnings that help you prepare to analyze a driver with Static Driver Verifier (SDV). SDV requires drivers to have declarations that define the role of the driver-supplied callback functions. PFD will indicate when you need to add these role type declarations to the driver code.

PFD is now integrated into the build environments and OACR in the WDK. When you build your driver using the WDK build environments, PFD runs automatically in the background and presents an easy-to-read view for any potential defects it finds.

High Quality Drivers and WDK Samples

For Windows 7, all Microsoft drivers that ship with the operating system and all WDK samples have been verified with PFD, and identified defects have been fixed. In addition, the WDK public headers are now annotated to enable PFD to better find code defects.

Because PFD annotations are now in public header files, driver writers can take advantage of these checks by simply running PFD on their drivers. Adding additional PFD annotations to your driver code will give you deeper analysis.

Windows headers for drivers now provide a comprehensive set of examples of how to annotate your functions.

General PREfast
White PaperHow to Use Function typedefs in C++ Driver Code to Improve PREƒast Results
White PaperPREƒast Step-by-Step (V8.0)
White PaperPREfast Annotations
WHDC Portal/NodalStatic Driver Verifier
OtherDeveloping Drivers with Windows Driver Foundation by Orwick and Smith
Comprehensive Guide from Microsoft Press

Static Analysis Tools - WinHEC
Microsoft Powerpoint (.ppt)Static Analysis and Verification of Drivers [WinHEC 2007; 8.6 MB]
Microsoft Powerpoint (.ppt)Static Analysis Tools: PREƒast for Drivers [WinHEC 2007; 1.2 MB]
Microsoft Powerpoint (.ppt)Using Static Analysis Tools When Developing Drivers [WinHEC 2008; 1.5 MB]

Static Tools for Driver Development - WHDC Labs
DownloadablePREƒast for Drivers: WHDC Lab [388 KB]
DownloadableStatic Driver Verifier for KMDF Drivers: WHDC Lab [242 KB]
DownloadableStatic Driver Verifier for WDM Drivers: WHDC Lab [366 KB]


Looking for help with your personal computer?