15974#line 1267
15975 __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
15976#line 1267
15977 __cil_tmp64 = *((struct mwifiex_pcie_buf_desc **)__cil_tmp63);
15978#line 1267
15979 __cil_tmp65 = (unsigned long )__cil_tmp64;
15980#line 1267
15981 __cil_tmp66 = __cil_tmp65 + 10;
15982#line 1267
15983 *((u16 *)__cil_tmp66) = (u16 )0U;
15984#line 1268
15985 skb = (struct sk_buff *)0;
15986 }
15987 } else {
15988 {
15989#line 1270
15990 __cil_tmp67 = & descriptor;
15991#line 1270
15992 *((char const **)__cil_tmp67) = "mwifiex_pcie";
15993#line 1270
15994 __cil_tmp68 = (unsigned long )(& descriptor) + 8;
15995#line 1270
15996 *((char const **)__cil_tmp68) = "mwifiex_pcie_event_complete";
15997#line 1270
15998 __cil_tmp69 = (unsigned long )(& descriptor) + 16;
15999#line 1270
16000 *((char const **)__cil_tmp69) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14373/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/mwifiex/pcie.c.p";
16001#line 1270
16002 __cil_tmp70 = (unsigned long )(& descriptor) + 24;
16003#line 1270
16004 *((char const **)__cil_tmp70) = "info: ERROR: buf still valid at index %d, <%p, %p>\n";
16005#line 1270
16006 __cil_tmp71 = (unsigned long )(& descriptor) + 32;
16007#line 1270
16008 *((unsigned int *)__cil_tmp71) = 1272U;
16009#line 1270
16010 __cil_tmp72 = (unsigned long )(& descriptor) + 35;
16011#line 1270
16012 *((unsigned char *)__cil_tmp72) = (unsigned char)0;
16013#line 1270
16014 __cil_tmp73 = (unsigned long )(& descriptor) + 35;