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_simpl2_BUG.cil.c |
Line in file: | 1320 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
1290 { 1291#line 941 1292#line 941 1293 if (status < 0) { 1294 { 1295#line 943 1296 Irp__IoStatus__Status = status; 1297#line 944 1298 myStatus = status; 1299#line 945 1300 IofCompleteRequest(Irp, 0); 1301 } 1302#line 947 1303 return (status); 1304 } 1305 } 1306 { 1307#line 952 1308 tmp = KbFilter_DispatchPassThrough(DeviceObject, Irp); 1309 } 1310#line 954 1311 return (tmp); 1312} 1313} 1314 1315void errorFn(void) 1316{ 1317 1318 { 1319 goto ERROR; 1320 ERROR: 1321#line 29 1322 return; 1323} 1324}