Showing error 171

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 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

 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      }
Show full sources
↑