Showing error 1549

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

Source: 

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