Showing error 167

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

Source: 

 59734    }
 59735  } else {
 59736
 59737  }
 59738#line 848
 59739  if (local == 0) {
 59740#line 848
 59741    if (remote == 0) {
 59742      {
 59743#line 848
 59744      __cil_tmp73 = mdev->state;
 59745#line 848
 59746      tmp___7 = is_susp(__cil_tmp73);
 59747      }
 59748#line 848
 59749      if (tmp___7 == 0) {
 59750        {
 59751#line 849
 59752        tmp___6 = ___ratelimit(& drbd_ratelimit_state, "drbd_make_request_common");
 59753        }
 59754#line 849
 59755        if (tmp___6 != 0) {
 59756          {
 59757#line 850
 59758          __cil_tmp74 = mdev->vdisk;
 59759#line 850
 59760          __cil_tmp75 = & __cil_tmp74->part0.__dev;
 59761#line 850
 59762          __cil_tmp76 = (struct device  const  *)__cil_tmp75;
 59763#line 850
 59764          dev_err(__cil_tmp76, "IO ERROR: neither local nor remote disk\n");
 59765          }
 59766        } else {
 59767
 59768        }
 59769#line 851
 59770        goto fail_free_complete;
 59771      } else {
 59772
 59773      }
 59774    } else {
Show full sources
↑