Showing error 627

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

Source: 

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
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;
Show full sources
↑