/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    AliasWithinDispatch

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    This property is satisfied if __sdv_save_request 
    is called while within one of the Io Queue callback routines:
    EvtIoRead, EvtIoWrite, EvtIoDeviceControl, EvtIoInternalDeviceControl.


Help Link:

    https://go.microsoft.com/fwlink/?LinkId=507476

--*/



#include "slic_base.h"

state{
     enum {INIT, INDISP} s = INIT;
}
                   

[fun_WDF_IO_QUEUE_IO_DEVICE_CONTROL
,fun_WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL
,fun_WDF_IO_QUEUE_IO_READ
,fun_WDF_IO_QUEUE_IO_WRITE
,fun_WDF_IO_QUEUE_IO_DEFAULT
].entry
{
          s = INDISP;               
}
[fun_WDF_IO_QUEUE_IO_DEVICE_CONTROL
,fun_WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL
,fun_WDF_IO_QUEUE_IO_READ
,fun_WDF_IO_QUEUE_IO_WRITE
,fun_WDF_IO_QUEUE_IO_DEFAULT
].exit
{
         s = INIT;
}
sdv_save_request.entry
{
   if (s == INDISP) {
     abort "The property is satisfied as __sdv_save_request is called within one of the Io Queue callback routines: EvtIoRead, EvtIoWrite, EvtIoDeviceControl, EvtIoInternalDeviceControl.";
   }
}


