Showing error 1561

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

Source: 

   7int FloppyThread  ;
   8int KernelMode  ;
   9int Suspended  ;
  10int Executive  ;
  11int DiskController  ;
  12int FloppyDiskPeripheral  ;
  13int FlConfigCallBack  ;
  14int MaximumInterfaceType  ;
  15int MOUNTDEV_MOUNTED_DEVICE_GUID  ;
  16int myStatus  ;
  17int s  ;
  18int UNLOADED  ;
  19int NP  ;
  20int DC  ;
  21int SKIP1  ;
  22int SKIP2  ;
  23int MPR1  ;
  24int MPR3  ;
  25int IPC  ;
  26int pended  ;
  27int compRegistered  ;
  28int lowerDriverReturn  ;
  29int setEventCalled  ;
  30int customIrp  ;
  31
  32void errorFn(void) 
  33{ 
  34
  35  {
  36  goto ERROR;
  37  ERROR: 
  38  return;
  39}
  40}
  41
  42void _BLAST_init(void) 
  43{ 
  44
  45  {
  46#line 73
  47  UNLOADED = 0;
Show full sources
↑