/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    InitFreeDeviceCreateType4

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

	The driver must call WdfDeviceInitFree if an error occurs when calling WdfDeviceCreate.

	If your driver encounters an error while calling WdfDeviceCreate 
	and if the driver received the WDFDEVICE_INIT structure from a call to WdfControlDeviceInitAllocate, 
	the driver must call WdfDeviceInitFree. 
	
	Rule diagnostics:
	"A driver must call WdfDeviceInitFree if an error occurs in WdfDriverCreate when allocating a WDFDEVICE_INIT stucture via WdfControlDeviceInitAllocate."
 
	Related rules: 
	InitFreeDeviceCallback,InitFreeDeviceCreate,InitFreeDeviceCreateType2,PdoInitFreeDeviceCreateType2,
	InitFreeDeviceCreateType4,PdoInitFreeDeviceCallback,PdoInitFreeDeviceCreate,PdoInitFreeDeviceCreateType4 
	and InitFreeDevice.

Help Link:

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

--*/







#include "slic_base.h"

state{
     enum {ALLOCATENOTCALLED, ALLOCATECALLED} s = ALLOCATENOTCALLED;
	 enum {FREENOTREQUIRED,FREEREQUIRED,FREECALLED} s1 = FREENOTREQUIRED;
} 


watch sdv_WdfControlDeviceInitAllocate.exit.$return;

[sdv_WdfControlDeviceInitAllocate].exit [guard || null $return]
{
    if (($return != 0)) 
    { 
     s= ALLOCATECALLED;      
    }
}
[sdv_WdfDeviceInitFree].entry[guard || null $1]
{
    if (s1==FREEREQUIRED)
    {
     s1=FREECALLED;
    }
    else if($1==0) 
    {
     abort "$fname cannot be called with a PWDFDEVICE_INIT==null.";
    }
}

sdv_WdfDeviceCreate.entry[guard || null *$1]
{
     if(*$1==0) 
     {
      abort "$fname cannot be called with a PWDFDEVICE_INIT==null.";
     }	
}


sdv_WdfDeviceCreate.exit[guard || null *$1]
{	
     if((s==ALLOCATECALLED)&&(!NT_SUCCESS($return)))
     {
      s1=FREEREQUIRED;
     }
}


select one 
{
  case fun_DriverEntry:
      [fun_DriverEntry].exit
      {
        if (s1==FREEREQUIRED) 
	{
	 abort "A driver must call WdfDeviceInitFree if an error occurs in WdfDeviceCreate when allocating a WDFDEVICE_INIT stucture via WdfControlDeviceInitAllocate.";
        }
      }    
} 
