Showing error 1223

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

Source: 

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);
3262#line 431
3263  bdev = (struct BondedDevice *)tmp___1;
3264  }
3265  {
3266#line 432
3267  __cil_tmp88 = (struct BondedDevice *)0;
3268#line 432
3269  __cil_tmp89 = (unsigned long )__cil_tmp88;
3270#line 432
3271  __cil_tmp90 = (unsigned long )bdev;
3272#line 432
3273  if (__cil_tmp90 == __cil_tmp89) {
3274    {
3275#line 433
3276    printk("<3>comedi_bond: INTERNAL ERROR: Out of memory.\n");
3277    }
3278#line 434
3279    return (0);
3280  } else {
3281
3282  }
3283  }
3284#line 436
3285  *((struct comedi_device **)bdev) = d;
3286#line 437
Show full sources
↑