Showing error 1560

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

Source: 

   3extern long __VERIFIER_nondet_long(void);
   4extern void *__VERIFIER_nondet_pointer(void);
   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 myStatus  ;
  23int routine  ;
  24int pirp  ;
  25int Executive ;
  26int KernelMode ;
  27
  28void errorFn(void) 
  29{ 
  30
  31  {
  32  goto ERROR;
  33  ERROR: 
  34#line 58
  35  return;
  36}
  37}
  38#line 61 "diskperf_simpl1.cil.c"
  39void _BLAST_init(void) 
  40{ 
  41
  42  {
  43#line 65
Show full sources
↑