Showing error 35

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

Source: 

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