Showing error 1151

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

Source: 

16016    __cil_tmp74 = *((unsigned char *)__cil_tmp73);
16017#line 1270
16018    __cil_tmp75 = (long )__cil_tmp74;
16019#line 1270
16020    __cil_tmp76 = __cil_tmp75 & 1L;
16021#line 1270
16022    tmp___0 = __builtin_expect(__cil_tmp76, 0L);
16023    }
16024#line 1270
16025    if (tmp___0 != 0L) {
16026      {
16027#line 1270
16028      __cil_tmp77 = (unsigned long )adapter;
16029#line 1270
16030      __cil_tmp78 = __cil_tmp77 + 72;
16031#line 1270
16032      __cil_tmp79 = *((struct device **)__cil_tmp78);
16033#line 1270
16034      __cil_tmp80 = (struct device  const  *)__cil_tmp79;
16035#line 1270
16036      __cil_tmp81 = rdptr * 8UL;
16037#line 1270
16038      __cil_tmp82 = 1168 + __cil_tmp81;
16039#line 1270
16040      __cil_tmp83 = (unsigned long )card;
16041#line 1270
16042      __cil_tmp84 = __cil_tmp83 + __cil_tmp82;
16043#line 1270
16044      __cil_tmp85 = *((struct sk_buff **)__cil_tmp84);
16045#line 1270
16046      __dynamic_dev_dbg(& descriptor, __cil_tmp80, "info: ERROR: buf still valid at index %d, <%p, %p>\n",
16047                        rdptr, __cil_tmp85, skb);
16048      }
16049    } else {
16050
16051    }
16052  }
16053  }
16054#line 1275
16055  __cil_tmp86 = (unsigned long )card;
16056#line 1275
Show full sources
↑