Showing error 629

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

Source: 

3444    __cil_tmp85 = 18UL - 1UL;
3445#line 398
3446    __cil_tmp86 = __cil_tmp85 * 1UL;
3447#line 398
3448    __cil_tmp87 = (unsigned long )(file) + __cil_tmp86;
3449#line 398
3450    *((char *)__cil_tmp87) = (char)0;
3451#line 400
3452    __cil_tmp88 = 0 * 1UL;
3453#line 400
3454    __cil_tmp89 = (unsigned long )(file) + __cil_tmp88;
3455#line 400
3456    __cil_tmp90 = (char *)__cil_tmp89;
3457#line 400
3458    __cil_tmp91 = (char const   *)__cil_tmp90;
3459#line 400
3460    tmp___0 = comedi_open(__cil_tmp91);
3461#line 400
3462    __cil_tmp92 = minor * 8UL;
3463#line 400
3464    __cil_tmp93 = (unsigned long )(devs_opened) + __cil_tmp92;
3465#line 400
3466    *((struct comedi_device **)__cil_tmp93) = tmp___0;
3467#line 400
3468    d = tmp___0;
3469    }
3470#line 402
3471    if (! d) {
3472      {
3473#line 403
3474      printk("<3>comedi_bond: INTERNAL ERROR: Minor %u could not be opened\n", minor);
3475      }
3476#line 404
3477      return (0);
3478    } else {
3479
3480    }
3481    {
3482#line 408
3483    while (1) {
3484      while_continue___0: /* CIL Label */ ;
Show full sources
↑