Showing error 1221

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

Source: 

3200#line 412
3201  __cil_tmp79 = 17UL * 1UL;
3202#line 412
3203  __cil_tmp80 = (unsigned long )(file) + __cil_tmp79;
3204#line 412
3205  *((char *)__cil_tmp80) = (char)0;
3206#line 414
3207  __cil_tmp81 = (char const   *)(& file);
3208#line 414
3209  tmp___0 = comedi_open(__cil_tmp81);
3210#line 414
3211  __cil_tmp82 = minor * 8UL;
3212#line 414
3213  __cil_tmp83 = (unsigned long )(devs_opened) + __cil_tmp82;
3214#line 414
3215  *((struct comedi_device **)__cil_tmp83) = tmp___0;
3216#line 414
3217  d = tmp___0;
3218  }
3219  {
3220#line 416
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:
Show full sources
↑