SLAyer (separation Logic Analyzer) is a memory safety checker designed to verify that its input C code doesn't deference dangling pointers, do double frees, nor leak memory.
Using the tool
To run on a test, say cleanup_isochresourcedata_remove_head_list.c that mallocs and then frees a PLIST_ENTRY list, execute this in a cmd shell:
C:\> cd C:\SLAyer
C:\> cd test\kmdf\1394\cleanup_isochresourcedata_remove_head_list