Showing error 917

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/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 11799
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

11769#line 802
11770  if (ret < 0) {
11771#line 803
11772    goto err;
11773  } else {
11774
11775  }
11776#line 725
11777  i = i + 1;
11778  ldv_39135: ;
11779#line 725
11780  if (i < num) {
11781#line 726
11782    goto ldv_39134;
11783  } else {
11784#line 728
11785    goto ldv_39136;
11786  }
11787  ldv_39136: ;
11788  err: 
11789  {
11790#line 806
11791  __cil_tmp282 = (struct mutex *)st;
11792#line 806
11793  mutex_unlock(__cil_tmp282);
11794  }
11795#line 808
11796  if (ret < 0) {
11797    {
11798#line 809
11799    printk("<6>az6007: %s ERROR: %i\n", "az6007_i2c_xfer", ret);
11800    }
11801#line 810
11802    return (ret);
11803  } else {
11804
11805  }
11806#line 812
11807  return (num);
11808}
11809}
Show full sources
↑