Showing error 1220

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

Source: 

3156  __cil_tmp71 = *((int *)__cil_tmp70);
3157#line 402
3158  if (__cil_tmp71 == minor) {
3159    {
3160#line 403
3161    printk("<3>comedi_bond: INTERNAL ERROR: Cannot bond this driver to itself!\n");
3162    }
3163#line 404
3164    return (0);
3165  } else {
3166
3167  }
3168  }
3169  {
3170#line 406
3171  __cil_tmp72 = (struct comedi_device *)0;
3172#line 406
3173  __cil_tmp73 = (unsigned long )__cil_tmp72;
3174#line 406
3175  __cil_tmp74 = minor * 8UL;
3176#line 406
3177  __cil_tmp75 = (unsigned long )(devs_opened) + __cil_tmp74;
3178#line 406
3179  __cil_tmp76 = *((struct comedi_device **)__cil_tmp75);
3180#line 406
3181  __cil_tmp77 = (unsigned long )__cil_tmp76;
3182#line 406
3183  if (__cil_tmp77 != __cil_tmp73) {
3184    {
3185#line 407
3186    printk("<3>comedi_bond: INTERNAL ERROR: Minor %d specified more than once!\n",
3187           minor);
3188    }
3189#line 408
3190    return (0);
3191  } else {
3192
3193  }
3194  }
3195  {
3196#line 411
Show full sources
↑