Some PreFAST and Static Driver Verifier Notes
I just spent most of the day working with the new builds of PreFAST and Static Driver Verifier. PreFAST keeps getting better with each release; I found a few more issues with the 5112 WDK PreFAST than previous versions (mostly having to do with improved decorations of callback functions and better obsolete API checking). It's still my favorite static analysis tool... PC-Lint is great, and I'll continue to use it, but PreFAST is much more driver-oriented and tends to catch more of the types of mistakes I make these days than Lint does. Maybe the folks at Gimpel have finally got me trained. :-)
Static Driver Verifier is, well, SLOW. I ran it against one of my production drivers, and it did manage to find a bug (a double-completion, through an unlikely but not impossible code path), that I suspect was introduced fairly recently by another coder. Highly recommended as well - zero false positives, one true positive. If you haven't tried it yet, check out your WDF kits from WinHEC or Driver DevCon, if you were there. If you weren't there, consider signing up for the WDF beta; Static Driver Verifier is only in the WDF kit at this point, as far as I know.
In pondering the importance of static analysis tools, I think the double-completion case from today is important to consider. Any project of reasonable size will have more than one programmer on it, either during development or down the road, and issues like the one that popped up today are just bound to happen. Maintaining existing code is really hard to do well - just think of how much state you have in your head during initial code construction. You'll never manage to get that state re-built two years later when hunting down a bluescreen for a day or two, and unless the maintenance coders are out of sight, they aren't going to amass that much state either.
That's where static tools like PreFAST and Static Driver Verifier come into play. If someone manages to put an IoCompleteRequest() in a perfectly reasonable (but incorrect) place, they'll catch it. Add that to a checked OS and full driver verifier, and you have an exceedingly high chance of catching bugs introduced as a result of this lack of state.