Showing error 334

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 11883
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

11853#line 787
11854      printk("<c>\n");
11855      }
11856    } else {
11857
11858    }
11859    }
11860#line 788
11861    if (ret < 0) {
11862#line 789
11863      goto err;
11864    } else {
11865
11866    }
11867#line 711
11868    i = i + 1;
11869  }
11870  while_break: /* CIL Label */ ;
11871  }
11872  err: 
11873  {
11874#line 792
11875  __cil_tmp233 = (struct mutex *)st;
11876#line 792
11877  mutex_unlock(__cil_tmp233);
11878  }
11879#line 794
11880  if (ret < 0) {
11881    {
11882#line 795
11883    printk("<6>az6007: %s ERROR: %i\n", "az6007_i2c_xfer", ret);
11884    }
11885#line 796
11886    return (ret);
11887  } else {
11888
11889  }
11890#line 798
11891  return (num);
11892}
11893}
Show full sources
↑