Showing error 31

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ntdrivers/kbfiltr.BUG.i.cil.c
Line in file: 1637
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

1607NTSTATUS KbFilter_InternIoCtl(PDEVICE_OBJECT DeviceObject , PIRP Irp ) ;
1608extern NTSTATUS KbFilter_IoCtl(PDEVICE_OBJECT DeviceObject , PIRP Irp ) ;
1609NTSTATUS KbFilter_PnP(PDEVICE_OBJECT DeviceObject , PIRP Irp ) ;
1610NTSTATUS KbFilter_Power(PDEVICE_OBJECT DeviceObject , PIRP Irp ) ;
1611NTSTATUS KbFilter_InitializationRoutine(PDEVICE_OBJECT DeviceObject , PVOID SynchFuncContext ,
1612                                        NTSTATUS (*ReadPort)(PVOID Context , PUCHAR Value ,
1613                                                             BOOLEAN WaitForACK ) ,
1614                                        NTSTATUS (*WritePort)(PVOID Context , UCHAR Value ,
1615                                                              BOOLEAN WaitForACK ) ,
1616                                        PBOOLEAN TurnTranslationOn ) ;
1617BOOLEAN KbFilter_IsrHook(PDEVICE_OBJECT DeviceObject , PKEYBOARD_INPUT_DATA CurrentInput ,
1618                         POUTPUT_PACKET CurrentOutput , UCHAR StatusByte , PUCHAR DataByte ,
1619                         PBOOLEAN ContinueProcessing , PKEYBOARD_SCAN_STATE ScanState ) ;
1620void KbFilter_ServiceCallback(PDEVICE_OBJECT DeviceObject , PKEYBOARD_INPUT_DATA InputDataStart ,
1621                              PKEYBOARD_INPUT_DATA InputDataEnd , PULONG InputDataConsumed ) ;
1622void KbFilter_Unload(PDRIVER_OBJECT Driver ) ;
1623NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject , PUNICODE_STRING RegistryPath ) ;
1624#pragma alloc_text(INIT,DriverEntry)
1625#pragma alloc_text(PAGE,KbFilter_AddDevice)
1626#pragma alloc_text(PAGE,KbFilter_CreateClose)
1627#pragma alloc_text(PAGE,KbFilter_IoCtl)
1628#pragma alloc_text(PAGE,KbFilter_InternIoCtl)
1629#pragma alloc_text(PAGE,KbFilter_Unload)
1630#pragma alloc_text(PAGE,KbFilter_DispatchPassThrough)
1631#pragma alloc_text(PAGE,KbFilter_PnP)
1632#pragma alloc_text(PAGE,KbFilter_Power)
1633void errorFn(void) 
1634{ 
1635
1636  {
1637  ERROR: 
1638  goto ERROR;
1639}
1640}
1641int s  ;
1642int UNLOADED  ;
1643int NP  ;
1644int DC  ;
1645int SKIP1  ;
1646int SKIP2  ;
1647int MPR1  ;
Show full sources