Showing error 41

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

Source: 

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