/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    QueuedSpinLockRelease

Domain:

    storport

Rule ID:

    Not Applicable

Description:

    This rule verifies that the driver does not call KeReleaseInStackQueuedSpinLock 
    without first acquiring the lock via KeAcquireInStackQueuedSpinLock.

Help Link:

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

--*/


#include "ntddk_slic.h"

state {
	enum {unlocked, locked} s = unlocked;
	int *pointer = 0;
}

KeReleaseInStackQueuedSpinLock.exit
{
	if ( (s == unlocked) && (pointer != $1) ) {
		abort "The driver is calling $fname without first acquiring the queued spinlock.";
	} else {
		halt;
	}
}

KeAcquireInStackQueuedSpinLock.exit
{   
	s = locked;
	pointer = $2;
}
