Share on Facebook Tweet on Twitter Share on LinkedIn Share by email

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

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, and install into the default
C:\WinDDK\SDVRP. (You don't need to install WDK too.)

Once you've done this, unzip the 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:\> 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 format, etc).