Showing error 633

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

Source: 

3905#line 456
3906      strncat(__cil_tmp241, __cil_tmp245, __cil_tmp246);
3907      }
3908    }
3909    while_break___0: /* CIL Label */ ;
3910    }
3911#line 377
3912    i = i + 1;
3913  }
3914  while_break: /* CIL Label */ ;
3915  }
3916  {
3917#line 462
3918  __cil_tmp247 = (unsigned long )dev;
3919#line 462
3920  __cil_tmp248 = __cil_tmp247 + 16;
3921#line 462
3922  __cil_tmp249 = *((void **)__cil_tmp248);
3923#line 462
3924  __cil_tmp250 = (struct Private *)__cil_tmp249;
3925#line 462
3926  __cil_tmp251 = (unsigned long )__cil_tmp250;
3927#line 462
3928  __cil_tmp252 = __cil_tmp251 + 2320;
3929#line 462
3930  __cil_tmp253 = *((unsigned int *)__cil_tmp252);
3931#line 462
3932  if (! __cil_tmp253) {
3933    {
3934#line 463
3935    printk("<3>comedi_bond: INTERNAL ERROR: No channels found!\n");
3936    }
3937#line 464
3938    return (0);
3939  } else {
3940
3941  }
3942  }
3943#line 467
3944  return (1);
3945}
Show full sources
↑