Showing error 1225

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--staging--comedi--drivers--comedi_bond.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3709
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

3679      } else {
3680#line 394
3681        goto ldv_19421;
3682      }
3683      }
3684    }
3685  } else {
3686#line 394
3687    goto ldv_19421;
3688  }
3689  ldv_19421: ;
3690  {
3691#line 476
3692  __cil_tmp238 = (unsigned long )dev;
3693#line 476
3694  __cil_tmp239 = __cil_tmp238 + 16;
3695#line 476
3696  __cil_tmp240 = *((void **)__cil_tmp239);
3697#line 476
3698  __cil_tmp241 = (struct Private *)__cil_tmp240;
3699#line 476
3700  __cil_tmp242 = (unsigned long )__cil_tmp241;
3701#line 476
3702  __cil_tmp243 = __cil_tmp242 + 2320;
3703#line 476
3704  __cil_tmp244 = *((unsigned int *)__cil_tmp243);
3705#line 476
3706  if (__cil_tmp244 == 0U) {
3707    {
3708#line 477
3709    printk("<3>comedi_bond: INTERNAL ERROR: No channels found!\n");
3710    }
3711#line 478
3712    return (0);
3713  } else {
3714
3715  }
3716  }
3717#line 481
3718  return (1);
3719}
Show full sources
↑