Showing error 1565

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

Source: 

733      switch_3_default: ;
734#line 584
735      return (-1073741823);
736    } else {
737
738    }
739  }
740}
741}
742#line 592 "kbfiltr_simpl1.cil.c"
743int KbFilter_Complete(int DeviceObject , int Irp , int Context ) 
744{ int event ;
745
746  {
747  {
748#line 597
749  event = Context;
750#line 598
751  KeSetEvent(event, 0, 0);
752  }
753#line 600
754  return (-1073741802);
755}
756}
757
758void errorFn(void) 
759{ 
760
761  {
762  goto ERROR;
763  ERROR: 
764#line 23
765  return;
766}
767}
Show full sources
↑