Showing error 25

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


Source:

2805                                                                        ACCESS_MASK DesiredAccess ,
2806                                                                        PHANDLE DevInstRegKey ) ;
2807  NTSTATUS IoRegisterDeviceInterface(PDEVICE_OBJECT PhysicalDeviceObject ,
2808                                                                                                   GUID const   *InterfaceClassGuid ,
2809                                                                                                   PUNICODE_STRING ReferenceString ,
2810                                                                                                   PUNICODE_STRING SymbolicLinkName ) ;
2811  NTSTATUS IoSetDeviceInterfaceState(PUNICODE_STRING SymbolicLinkName ,
2812                                                                   BOOLEAN Enable ) ;
2813#pragma warning(disable:4200)
2814#pragma warning(default:4200)
2815  NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject ,
2816                                                      PIRP Irp ) ;
2817  void PoStartNextPowerIrp(PIRP Irp ) ;
2818  NTSTATUS ObReferenceObjectByHandle(HANDLE Handle ,
2819                                                                   ACCESS_MASK DesiredAccess ,
2820                                                                   POBJECT_TYPE ObjectType ,
2821                                                                   KPROCESSOR_MODE AccessMode ,
2822                                                                   PVOID *Object ,
2823                                                                   POBJECT_HANDLE_INFORMATION HandleInformation ) ;
2824  void ObfDereferenceObject(PVOID Object ) ;
2825  NTSTATUS ZwClose(HANDLE Handle ) ;
2826#pragma once
2827#pragma once
2828#pragma warning(disable:4200)
2829#pragma warning(default:4200)
2830int __BLAST_NONDET  ;
2831void errorFn(void) 
2832{ 
2833
2834  {
2835  ERROR: 
2836  goto ERROR;
2837}
2838}
2839int s  ;
2840int UNLOADED  ;
2841int NP  ;
2842int DC  ;
2843int SKIP1  ;
2844int SKIP2  ;
2845int MPR1  ;
Show full sources