/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    MarkIrpPending2

Domain:

    wdm

Rule ID:

    Not Applicable

Description:

    This rule specifies that if a dispatch routine returns
    STATUS_PENDING it has called IoMarkIrpPending or passed the
    IRP to the lower driver.  See MarkIrpPending for a
    complimentary specification.

Help Link:

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

--*/


#include "slic_base.h"

state {
} with guard(sdv_main,sdv_irp) 

[SDV_RunDispatchFunction].exit [guard $2]
{
    if ($return == STATUS_PENDING) {
       abort "The dispatch routine has not marked the incoming IRP with IoMarkIrpPending, but it is returning STATUS_PENDING.";
    }
    else
    {
       halt;
    }
}

[RemoveHeadList,sdv_containing_record].entry
{
    halt;
}

[KeWaitForSingleObject].entry
{
    halt;
}




[PoCallDriver,IoCallDriver].exit[guard $2] 
{
    halt;
}

IoMarkIrpPending.entry[guard $1]
{        
    halt;
}
