Showing error 1554

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ntdrivers/floppy2_safe.i.cil.c
Line in file: 6175
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 6145  __cil_tmp101 = *mem_134;
 6146#line 835
 6147  mem_135 = (UCHAR *)__cil_tmp97;
 6148#line 835
 6149  *mem_135 = (unsigned char )__cil_tmp101;
 6150#line 836
 6151  __cil_tmp102 = (unsigned int )biosDriveMediaConstants;
 6152#line 836
 6153  __cil_tmp103 = __cil_tmp102 + 52;
 6154#line 836
 6155  __cil_tmp104 = 64 + 44;
 6156#line 836
 6157  __cil_tmp105 = (unsigned int )FdcInfo;
 6158#line 836
 6159  __cil_tmp106 = __cil_tmp105 + __cil_tmp104;
 6160#line 836
 6161  mem_136 = (ULONG *)__cil_tmp106;
 6162#line 836
 6163  __cil_tmp107 = *mem_136;
 6164#line 836
 6165  mem_137 = (UCHAR *)__cil_tmp103;
 6166#line 836
 6167  *mem_137 = (unsigned char )__cil_tmp107;
 6168#line 838
 6169  return (0L);
 6170}
 6171}
 6172#line 949
 6173void assert(int cond) {
 6174  if (!(cond)) {
 6175    ERROR: goto ERROR; 
 6176  }
 6177  return;
 6178}
 6179#line 841 "floppy.c"
 6180NTSTATUS FlQueueIrpToThread(PIRP Irp , PDISKETTE_EXTENSION DisketteExtension ) 
 6181{ NTSTATUS status ;
 6182  HANDLE threadHandle ;
 6183  PIO_STACK_LOCATION irpSp ;
 6184  OBJECT_ATTRIBUTES ObjAttributes ;
 6185  unsigned int __cil_tmp7 ;
Show full sources