SLAyer is an automatic, separation-logic-based memory safety checker. It checks that its input C code doesn't deference dangling pointers, do double frees, nor leak memory.
Note By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license. Read the license.
There are two pre-requisites for using the tool:
1. The Visual Studio 2010 C compiler (cl.exe) is used to compile the C
2. The Static Driver Verifier Research Platform (SDVRP) is used to translate
cl.exe's output object to an internal abstract syntax tree. Download SDVRP
from http://research.microsoft.com/slam/, and install into the default
C:\WinDDK\SDVRP. (You don't need to install WDK too.)
Once you've done this, unzip the SLAyer.zip archive into C:\SLAyer on your
Using the tool
The release comes with a set of test programs. 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
C:\> slayer cleanup_isochresourcedata_remove_head_list.c
On exit, SLAyer prints a "RESULT: SAFE" message, and leaves several output
files (the program's internal representation in dot format, a counter-example
in defect.tt format, etc).