Showing error 1217

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

Source: 

3104#line 392
3105  __cil_tmp61 = 16 * 1UL;
3106#line 392
3107  __cil_tmp62 = (unsigned long )(file) + __cil_tmp61;
3108#line 392
3109  *((char *)__cil_tmp62) = (char )'X';
3110#line 392
3111  __cil_tmp63 = 17 * 1UL;
3112#line 392
3113  __cil_tmp64 = (unsigned long )(file) + __cil_tmp63;
3114#line 392
3115  *((char *)__cil_tmp64) = (char )'\000';
3116#line 393
3117  __cil_tmp65 = i * 4UL;
3118#line 393
3119  __cil_tmp66 = 20 + __cil_tmp65;
3120#line 393
3121  __cil_tmp67 = (unsigned long )it;
3122#line 393
3123  __cil_tmp68 = __cil_tmp67 + __cil_tmp66;
3124#line 393
3125  minor = *((int *)__cil_tmp68);
3126#line 395
3127  sdev = -1;
3128#line 396
3129  bdev = (struct BondedDevice *)0;
3130#line 398
3131  if (minor < 0) {
3132    {
3133#line 399
3134    printk("<3>comedi_bond: INTERNAL ERROR: Minor %d is invalid!\n", minor);
3135    }
3136#line 400
3137    return (0);
3138  } else
3139#line 398
3140  if (minor > 47) {
3141    {
3142#line 399
3143    printk("<3>comedi_bond: INTERNAL ERROR: Minor %d is invalid!\n", minor);
3144    }
Show full sources
↑