Showing error 1555

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_unsafe.i.cil.c
Line in file: 1641
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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