Showing error 561

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--net--wireless--mwifiex--mwifiex_pcie.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 16213
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

16183        __cil_tmp62 = ! __cil_tmp61;
16184#line 1256
16185        __cil_tmp63 = ! __cil_tmp62;
16186#line 1256
16187        __cil_tmp64 = (long )__cil_tmp63;
16188#line 1256
16189        tmp___8 = __builtin_expect(__cil_tmp64, 0L);
16190        }
16191#line 1256
16192        if (tmp___8) {
16193          {
16194#line 1256
16195          __cil_tmp65 = (unsigned long )adapter;
16196#line 1256
16197          __cil_tmp66 = __cil_tmp65 + 72;
16198#line 1256
16199          __cil_tmp67 = *((struct device **)__cil_tmp66);
16200#line 1256
16201          __cil_tmp68 = (struct device  const  *)__cil_tmp67;
16202#line 1256
16203          __cil_tmp69 = rdptr * 8UL;
16204#line 1256
16205          __cil_tmp70 = 1168 + __cil_tmp69;
16206#line 1256
16207          __cil_tmp71 = (unsigned long )card;
16208#line 1256
16209          __cil_tmp72 = __cil_tmp71 + __cil_tmp70;
16210#line 1256
16211          __cil_tmp73 = *((struct sk_buff **)__cil_tmp72);
16212#line 1256
16213          __dynamic_dev_dbg(& descriptor___27, __cil_tmp68, "info: ERROR: buf still valid at index %d, <%p, %p>\n",
16214                            rdptr, __cil_tmp73, skb);
16215          }
16216        } else {
16217
16218        }
16219#line 1256
16220        goto while_break___0;
16221      }
16222      while_break___0: /* CIL Label */ ;
16223      }
Show full sources
↑