Showing error 1222

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


Source:

3221  __cil_tmp84 = (struct comedi_device *)0;
3222#line 416
3223  __cil_tmp85 = (unsigned long )__cil_tmp84;
3224#line 416
3225  __cil_tmp86 = (unsigned long )d;
3226#line 416
3227  if (__cil_tmp86 == __cil_tmp85) {
3228    {
3229#line 417
3230    printk("<3>comedi_bond: INTERNAL ERROR: Minor %u could not be opened\n", minor);
3231    }
3232#line 418
3233    return (0);
3234  } else {
3235
3236  }
3237  }
3238#line 422
3239  goto ldv_19417;
3240  ldv_19416: 
3241  {
3242#line 424
3243  __cil_tmp87 = (unsigned int )sdev;
3244#line 424
3245  nchans = comedi_get_n_channels(d, __cil_tmp87);
3246  }
3247#line 425
3248  if (nchans <= 0) {
3249    {
3250#line 426
3251    printk("<3>comedi_bond: INTERNAL ERROR: comedi_get_n_channels() returned %d on minor %u subdev %d!\n",
3252           nchans, minor, sdev);
3253    }
3254#line 429
3255    return (0);
3256  } else {
3257
3258  }
3259  {
3260#line 431
3261  tmp___1 = kmalloc(32UL, 208U);
Show full sources