Showing error 1559

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c
Line in file: 35
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

   5void IofCompleteRequest(int Irp , int PriorityBoost ) ;
   6int __VERIFIER_nondet_int()  ;
   7int s  ;
   8int UNLOADED  ;
   9int NP  ;
  10int DC  ;
  11int SKIP1  ;
  12int SKIP2  ;
  13int MPR1  ;
  14int MPR3  ;
  15int IPC  ;
  16int pended  ;
  17int compFptr  ;
  18int compRegistered  ;
  19int lowerDriverReturn  ;
  20int setEventCalled  ;
  21int customIrp  ;
  22int routine  ;
  23int myStatus  ;
  24int pirp  ;
  25int Executive ;
  26int Suspended ;
  27int KernelMode ;
  28int DeviceUsageTypePaging ;
  29
  30void errorFn(void) 
  31{ 
  32
  33  {
  34  goto ERROR;
  35  ERROR: 
  36#line 60
  37  return;
  38}
  39}
  40#line 63 "cdaudio_simpl1.cil.c"
  41void _BLAST_init(void) 
  42{ 
  43
  44  {
  45#line 67
Show full sources
↑