Showing error 74

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: 59876
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 59846    }
 59847  } else {
 59848
 59849  }
 59850#line 848
 59851  if (local == 0) {
 59852#line 848
 59853    if (remote == 0) {
 59854      {
 59855#line 848
 59856      __cil_tmp73 = mdev->state;
 59857#line 848
 59858      tmp___7 = is_susp(__cil_tmp73);
 59859      }
 59860#line 848
 59861      if (tmp___7 == 0) {
 59862        {
 59863#line 849
 59864        tmp___6 = ___ratelimit(& drbd_ratelimit_state, "drbd_make_request_common");
 59865        }
 59866#line 849
 59867        if (tmp___6 != 0) {
 59868          {
 59869#line 850
 59870          __cil_tmp74 = mdev->vdisk;
 59871#line 850
 59872          __cil_tmp75 = & __cil_tmp74->part0.__dev;
 59873#line 850
 59874          __cil_tmp76 = (struct device  const  *)__cil_tmp75;
 59875#line 850
 59876          dev_err(__cil_tmp76, "IO ERROR: neither local nor remote disk\n");
 59877          }
 59878        } else {
 59879
 59880        }
 59881#line 851
 59882        goto fail_free_complete;
 59883      } else {
 59884
 59885      }
 59886    } else {
Show full sources
↑