Installation Instructions

There are two pre-requisites for using the tool:

1. The Visual Studio 2010 C compiler (cl.exe) is used to compile the C
programs.

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
machine.

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:\> setup.cmd
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).