/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    InitFreeDeviceCreateType2

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

	A driver shouldn't call WdfDeviceCreate after it calls WdfDeviceInitFree.

	
	Rule diagnostics:
	"A driver shouldn't call WdfDeviceCreate after it calls WdfDeviceInitFree."
 
    Related rules: 
	InitFreeDeviceCallback, InitFreeDeviceCreate, InitFreeDeviceCreateType2, PdoInitFreeDeviceCreateType2, 
	InitFreeDeviceCreateType4, PdoInitFreeDeviceCallback, PdoInitFreeDeviceCreate, PdoInitFreeDeviceCreateType4, 
	and InitFreeDevice.

Help Link:

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

--*/




#include "slic_base.h"

state{
     enum {FREENOTCALLED,FREECALLED} s = FREENOTCALLED;
} 

watch sdv_WdfControlDeviceInitAllocate.exit.$return;



[sdv_WdfDeviceInitFree].entry[guard $1]
{
	
    s=FREECALLED;
		
}

[sdv_WdfDeviceCreate].exit[guard *$1]
{	
    if (s==FREECALLED) 
    { 
     abort "A driver shouldn't call WdfDeviceCreate after it calls WdfDeviceInitFree.";
    }
	else
	{
		halt;
	}
}





 
