User: | Jiri Slaby |
Error type: | Reachable Error Location |
Error type description: | A specified error location is reachable in some program path |
File location: | ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko_unsafe.cil.out.i.pp.cil.c |
Line in file: | 60088 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
60058#line 890 60059 if (send_oos == 0) { 60060 { 60061#line 891 60062 __cil_tmp98 = mdev->vdisk; 60063#line 891 60064 __cil_tmp99 = & __cil_tmp98->part0.__dev; 60065#line 891 60066 __cil_tmp100 = (struct device const *)__cil_tmp99; 60067#line 891 60068 dev_warn(__cil_tmp100, "lost connection while grabbing the req_lock!\n"); 60069 } 60070 } else { 60071 60072 } 60073 } else { 60074 60075 } 60076#line 892 60077 if (local == 0) { 60078#line 892 60079 if (remote == 0) { 60080 { 60081#line 893 60082 __cil_tmp101 = mdev->vdisk; 60083#line 893 60084 __cil_tmp102 = & __cil_tmp101->part0.__dev; 60085#line 893 60086 __cil_tmp103 = (struct device const *)__cil_tmp102; 60087#line 893 60088 dev_err(__cil_tmp103, "IO ERROR: neither local nor remote disk\n"); 60089#line 894 60090 __cil_tmp104 = & mdev->req_lock; 60091#line 894 60092 spin_unlock_irq(__cil_tmp104); 60093 } 60094#line 895 60095 goto fail_free_complete; 60096 } else { 60097 60098 }