Showing error 36

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/diskperf_simpl1.cil.c
Line in file: 28
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 myStatus  ;
  18int routine  ;
  19int pirp  ;
  20int Executive ;
  21int KernelMode ;
  22
  23void errorFn(void) 
  24{ 
  25
  26  {
  27  goto ERROR;
  28  ERROR: 
  29#line 58
  30  return;
  31}
  32}
  33#line 61 "diskperf_simpl1.cil.c"
  34void _BLAST_init(void) 
  35{ 
  36
  37  {
  38#line 65
Show full sources
↑