Showing error 168

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-safe.cil.out.i.pp.cil.c
Line in file: 59976
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

 59946#line 890
 59947      if (send_oos == 0) {
 59948        {
 59949#line 891
 59950        __cil_tmp98 = mdev->vdisk;
 59951#line 891
 59952        __cil_tmp99 = & __cil_tmp98->part0.__dev;
 59953#line 891
 59954        __cil_tmp100 = (struct device  const  *)__cil_tmp99;
 59955#line 891
 59956        dev_warn(__cil_tmp100, "lost connection while grabbing the req_lock!\n");
 59957        }
 59958      } else {
 59959
 59960      }
 59961    } else {
 59962
 59963    }
 59964#line 892
 59965    if (local == 0) {
 59966#line 892
 59967      if (remote == 0) {
 59968        {
 59969#line 893
 59970        __cil_tmp101 = mdev->vdisk;
 59971#line 893
 59972        __cil_tmp102 = & __cil_tmp101->part0.__dev;
 59973#line 893
 59974        __cil_tmp103 = (struct device  const  *)__cil_tmp102;
 59975#line 893
 59976        dev_err(__cil_tmp103, "IO ERROR: neither local nor remote disk\n");
 59977#line 894
 59978        __cil_tmp104 = & mdev->req_lock;
 59979#line 894
 59980        spin_unlock_irq(__cil_tmp104);
 59981        }
 59982#line 895
 59983        goto fail_free_complete;
 59984      } else {
 59985
 59986      }
Show full sources
↑