/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    CtlDeviceFinishInitDrEntry

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    If a PnP driver creates a control device object in a callback function, 
    it must call WdfControlFinishInitializing after the device has been created
    and before exit from callback. This rule applies to the DriverEntry routine. 
    The rule is not applicable for non-PnP drivers.

    If a PnP driver calls WdfDeviceCreate for a control device object and the call 
    returns status STATUS_SUCCESS, the rule checks that WdfControlFinishInitializing is called before
    exit from the DriverEntry routine , unless the WDFObjectDelete method
    was called before (this usually happens when there is an error
    during an initialization phase for the control device).

    Rule diagnostics:
    "WdfControlFinishInitializing must be called after the control device has been created and 
    before it can be used and have I/O sent to it."


Help Link:

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

--*/




#include "slic_base.h"

state{
     enum {INIT, FINISHCALLED} s = INIT;
     enum {INIT1, INITCALLED, CREATECALLED} u = INIT1;
     int t = 0;
}

watch sdv_WdfControlDeviceInitAllocate.exit.$return;

sdv_WdfControlDeviceInitAllocate.exit[guard $return]
{
     u = INITCALLED;
}
sdv_WdfDeviceCreate.exit[guard *$1]
{
  if ((u == INITCALLED)&&($return == STATUS_SUCCESS)) {
     u = CREATECALLED;
     t = *$3;               
   }
}
sdv_WdfControlFinishInitializing.entry
{
  if ((u == CREATECALLED)&&(t == $1)) {
     s = FINISHCALLED;    
  }
}
sdv_WdfObjectDelete.entry
{
  if ($1 == t) {
	halt;
  }
}
select one {
  case fun_WDF_DRIVER_DEVICE_ADD:
      [fun_DriverEntry].exit
      {
          if ((u == CREATECALLED)&&(s != FINISHCALLED))
		  {
             abort "WdfControlFinishInitializing must be called after the control device has been created and before it can be used and have I/O sent to it.";
          }
		  
      }
 }



   
