Showing error 631

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

Source: 

3498        goto while_break___0;
3499      }
3500      {
3501#line 410
3502      __cil_tmp96 = (unsigned int )sdev;
3503#line 410
3504      nchans = comedi_get_n_channels(d, __cil_tmp96);
3505      }
3506#line 411
3507      if (nchans <= 0) {
3508        {
3509#line 412
3510        printk("<3>comedi_bond: INTERNAL ERROR: comedi_get_n_channels() returned %d on minor %u subdev %d!\n",
3511               nchans, minor, sdev);
3512        }
3513#line 415
3514        return (0);
3515      } else {
3516
3517      }
3518      {
3519#line 417
3520      tmp___1 = kmalloc(32UL, 208U);
3521#line 417
3522      bdev = (struct BondedDevice *)tmp___1;
3523      }
3524#line 418
3525      if (! bdev) {
3526        {
3527#line 419
3528        printk("<3>comedi_bond: INTERNAL ERROR: Out of memory.\n");
3529        }
3530#line 420
3531        return (0);
3532      } else {
3533
3534      }
3535#line 422
3536      *((struct comedi_device **)bdev) = d;
3537#line 423
3538      __cil_tmp97 = (unsigned long )bdev;
Show full sources
↑