/*++
    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    IrqlReturn

Domain:

    Wdm

Rule ID:

    0x0002001D

Description:

    This rule specifies that dispatch routines must return at the
    exact same IRQL level at which they were called.
    
Help Link:

    https://go.microsoft.com/fwlink/?LinkId=216046
*/


#include "slic_base.h"

/* Records the IRQL at the start of a dispatch routine: */
state {
    int start_irql = 0;
}

/* Latch the IRQL at dispatch start: */
[SDV_RunDispatchFunction].entry
{
    start_irql = sdv_irql_current;
}

/* Make sure that the IRQL has been restored: */
[SDV_RunDispatchFunction].exit
{
    if (start_irql != sdv_irql_current) {
        abort "The dispatch routine does not return at the same IRQL level at which it was called";
    }
}
