Showing error 628

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: 3425
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

3395
3396    }
3397    {
3398#line 388
3399    __cil_tmp77 = (unsigned long )dev;
3400#line 388
3401    __cil_tmp78 = __cil_tmp77 + 32;
3402#line 388
3403    __cil_tmp79 = *((int *)__cil_tmp78);
3404#line 388
3405    if (minor == __cil_tmp79) {
3406      {
3407#line 389
3408      printk("<3>comedi_bond: INTERNAL ERROR: Cannot bond this driver to itself!\n");
3409      }
3410#line 390
3411      return (0);
3412    } else {
3413
3414    }
3415    }
3416    {
3417#line 392
3418    __cil_tmp80 = minor * 8UL;
3419#line 392
3420    __cil_tmp81 = (unsigned long )(devs_opened) + __cil_tmp80;
3421#line 392
3422    if (*((struct comedi_device **)__cil_tmp81)) {
3423      {
3424#line 393
3425      printk("<3>comedi_bond: INTERNAL ERROR: Minor %d specified more than once!\n",
3426             minor);
3427      }
3428#line 394
3429      return (0);
3430    } else {
3431
3432    }
3433    }
3434    {
3435#line 397
Show full sources
↑