/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    PdoInitFreeDeviceCreateType2

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=507120

--*/

   


#include "slic_base.h"

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

watch sdv_WdfPdoInitAllocate.exit.$return;


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

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





 
