Showing error 630

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

Source: 

3480    }
3481    {
3482#line 408
3483    while (1) {
3484      while_continue___0: /* CIL Label */ ;
3485      {
3486#line 408
3487      __cil_tmp94 = sdev + 1;
3488#line 408
3489      __cil_tmp95 = (unsigned int )__cil_tmp94;
3490#line 408
3491      sdev = comedi_find_subdevice_by_type(d, 5, __cil_tmp95);
3492      }
3493#line 408
3494      if (sdev > -1) {
3495
3496      } else {
3497#line 408
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);
Show full sources
↑