Showing error 1224

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

Source: 

3500#line 452
3501  __cil_tmp178 = __cil_tmp177 + 256;
3502#line 452
3503  *((struct BondedDevice ***)__cil_tmp178) = (struct BondedDevice **)tmp___4;
3504  }
3505  {
3506#line 455
3507  __cil_tmp179 = (struct BondedDevice **)0;
3508#line 455
3509  __cil_tmp180 = (unsigned long )__cil_tmp179;
3510#line 455
3511  __cil_tmp181 = (unsigned long )dev;
3512#line 455
3513  __cil_tmp182 = __cil_tmp181 + 16;
3514#line 455
3515  __cil_tmp183 = *((void **)__cil_tmp182);
3516#line 455
3517  __cil_tmp184 = (struct Private *)__cil_tmp183;
3518#line 455
3519  __cil_tmp185 = (unsigned long )__cil_tmp184;
3520#line 455
3521  __cil_tmp186 = __cil_tmp185 + 256;
3522#line 455
3523  __cil_tmp187 = *((struct BondedDevice ***)__cil_tmp186);
3524#line 455
3525  __cil_tmp188 = (unsigned long )__cil_tmp187;
3526#line 455
3527  if (__cil_tmp188 == __cil_tmp180) {
3528    {
3529#line 456
3530    printk("<3>comedi_bond: INTERNAL ERROR: Could not allocate memory. Out of memory?");
3531    }
3532#line 458
3533    return (0);
3534  } else {
3535
3536  }
3537  }
3538  {
3539#line 461
3540  __cil_tmp189 = (unsigned long )dev;
Show full sources
↑