Showing error 632

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

Source: 

3748#line 438
3749      __cil_tmp182 = *((void **)__cil_tmp181);
3750#line 438
3751      __cil_tmp183 = (struct Private *)__cil_tmp182;
3752#line 438
3753      __cil_tmp184 = (unsigned long )__cil_tmp183;
3754#line 438
3755      __cil_tmp185 = __cil_tmp184 + 256;
3756#line 438
3757      *((struct BondedDevice ***)__cil_tmp185) = (struct BondedDevice **)tmp___4;
3758      }
3759      {
3760#line 441
3761      __cil_tmp186 = (unsigned long )dev;
3762#line 441
3763      __cil_tmp187 = __cil_tmp186 + 16;
3764#line 441
3765      __cil_tmp188 = *((void **)__cil_tmp187);
3766#line 441
3767      __cil_tmp189 = (struct Private *)__cil_tmp188;
3768#line 441
3769      __cil_tmp190 = (unsigned long )__cil_tmp189;
3770#line 441
3771      __cil_tmp191 = __cil_tmp190 + 256;
3772#line 441
3773      __cil_tmp192 = *((struct BondedDevice ***)__cil_tmp191);
3774#line 441
3775      if (! __cil_tmp192) {
3776        {
3777#line 442
3778        printk("<3>comedi_bond: INTERNAL ERROR: Could not allocate memory. Out of memory?");
3779        }
3780#line 444
3781        return (0);
3782      } else {
3783
3784      }
3785      }
3786      {
3787#line 447
3788      __cil_tmp193 = (unsigned long )dev;
Show full sources
↑