| 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/floppy_simpl4_BUG.cil.c |
| Line in file: | 2156 |
| Project: | SV-COMP 2012 |
| Tools: |
Manual Work
|
| Entered: | 2012-11-19 13:47:39 UTC |
2126 } else { 2127#line 1515 2128 Irp__IoStatus__Status = 259; 2129#line 1516 2130 myStatus = 259; 2131#line 1517 2132 //Irp__Tail__Overlay__CurrentStackLocation__Control |= 1; 2133#line 1518 2134 if (pended == 0) { 2135#line 1519 2136 pended = 1; 2137 } else { 2138 { 2139#line 1522 2140 errorFn(); 2141 } 2142 } 2143#line 1525 2144 ntStatus = 259; 2145 } 2146#line 1527 2147 return (ntStatus); 2148} 2149} 2150 2151void errorFn(void) 2152{ 2153 2154 { 2155 goto ERROR; 2156 ERROR: 2157#line 53 2158 return; 2159} 2160}