Showing error 38

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.cil.c
Line in file: 31
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

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