Showing error 626

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

Source: 

3360    *((char *)__cil_tmp71) = (char )'\000';
3361#line 379
3362    __cil_tmp72 = i * 4UL;
3363#line 379
3364    __cil_tmp73 = 20 + __cil_tmp72;
3365#line 379
3366    __cil_tmp74 = (unsigned long )it;
3367#line 379
3368    __cil_tmp75 = __cil_tmp74 + __cil_tmp73;
3369#line 379
3370    minor = *((int *)__cil_tmp75);
3371#line 381
3372    sdev = -1;
3373#line 382
3374    __cil_tmp76 = (void *)0;
3375#line 382
3376    bdev = (struct BondedDevice *)__cil_tmp76;
3377#line 384
3378    if (minor < 0) {
3379      {
3380#line 385
3381      printk("<3>comedi_bond: INTERNAL ERROR: Minor %d is invalid!\n", minor);
3382      }
3383#line 386
3384      return (0);
3385    } else
3386#line 384
3387    if (minor >= 48) {
3388      {
3389#line 385
3390      printk("<3>comedi_bond: INTERNAL ERROR: Minor %d is invalid!\n", minor);
3391      }
3392#line 386
3393      return (0);
3394    } else {
3395
3396    }
3397    {
3398#line 388
3399    __cil_tmp77 = (unsigned long )dev;
3400#line 388
Show full sources
↑