/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    AliasWithinTimerDpc

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    This property is satisfied if __sdv_retrieve_request is present, 
    and is called while within a deferred processing routine.

Help Link:

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

--*/




#include "slic_base.h"

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

[fun_WDF_TIMER_1
,fun_WDF_TIMER_2
,fun_WDF_TIMER_3
,fun_WDF_TIMER_4
,fun_WDF_TIMER_5
,fun_WDF_TIMER_6
,fun_WDF_DPC_1
,fun_WDF_DPC_2
,fun_WDF_DPC_3
,fun_WDF_DPC_4
,fun_WDF_DPC_5
,fun_WDF_DPC_6
,fun_WDF_DPC_7
,fun_WDF_INTERRUPT_DPC
,fun_WDF_INTERRUPT_ENABLE
,fun_WDF_INTERRUPT_DISABLE
,fun_WDF_WORKITEM_1
,fun_WDF_WORKITEM_2
,fun_WDF_WORKITEM_3
,fun_WDF_WORKITEM_4
,fun_WDF_WORKITEM_5
,fun_WDF_WORKITEM_6
].entry
{
         s = INDEFR;               
}
[fun_WDF_TIMER_1
,fun_WDF_TIMER_2
,fun_WDF_TIMER_3
,fun_WDF_TIMER_4
,fun_WDF_TIMER_5
,fun_WDF_TIMER_6
,fun_WDF_DPC_1
,fun_WDF_DPC_2
,fun_WDF_DPC_3
,fun_WDF_DPC_4
,fun_WDF_DPC_5
,fun_WDF_DPC_6
,fun_WDF_DPC_7
,fun_WDF_INTERRUPT_DPC
,fun_WDF_INTERRUPT_ENABLE
,fun_WDF_INTERRUPT_DISABLE
,fun_WDF_WORKITEM_1
,fun_WDF_WORKITEM_2
,fun_WDF_WORKITEM_3
,fun_WDF_WORKITEM_4
,fun_WDF_WORKITEM_5
,fun_WDF_WORKITEM_6
].exit
{
          s = INIT;
}
sdv_retrieve_request.entry
{
   if (s == INDEFR) {
     abort "The property is satisfied as sdv_retrieve_request is called within a deferred processing routine: Dpc, Dpc for Isr, Timer Dpc, Workitem.";
   }
}

