Linux Driver Verification

Blast fails with exception on the orginal driver drivers/net/wireless/wl12xx/wl12xx.ko

The corresponding code fragments which cause exceptions of that kind are shown below.
If line in items 1-3 are commented, then the result is unsafe, and Exception otherwise.

Command line:
LDV_DEBUG=100 BLAST_EXP_NOALIAS=1 RCV_TIMELIMIT=900 RCV_MEMLIMIT=1800000 BLAST_SOLVER=yices BLAST_OPTIONS="-devdebug" ldv-manager tag=current envs=linux-2.6.31.6.tar.bz2 drivers=wl12xx.ko.tar.bz2 "rule_models=32_7"
Extracted driver with commented line is attached.

1. ZZZ: Exception: Failure("sanity check: mem_temp recycled? ((mem_conf@wl1251_mem_cfg).header).len")
in wl1251.c

static int wl1251_mem_cfg(struct wl12xx *wl)
       //mem_conf.header.len -=
       //      (MAX_TX_QUEUE_CONFIGS - mem_conf.mem_config.num_tx_queues) *
       //      sizeof(struct wl1251_acx_tx_queue_config);

2. ZZZ: Exception: Failure(""sanity check: mem_temp recycled? mem_size@wl12xx_set_partition")
in spi.c

void wl12xx_set_partition(struct wl12xx *wl,
             u32 mem_start, u32 mem_size,
             u32 reg_start, u32 reg_size)
...
//mem_size = HW_ACCESS_MEMORY_MAX_RANGE - reg_size;

3. ZZZ: Exception: Failure("sanity check: mem_temp recycled? mem_blocks@wl12xx_tx_frag_block_num")
in tx.c

static void wl12xx_tx_frag_block_num(struct tx_double_buffer_desc *tx_hdr)
...
       //mem_blocks_per_frag =
       //    ((frag_threshold + MAX_MPDU_HEADER_AND_SECURITY) /
       //     HW_BLOCK_SIZE) + 1;

       //mem_blocks = num_mpdus * mem_blocks_per_frag;

...
   //mem_blocks += (payload_len / HW_BLOCK_SIZE) + 1;

   //if (num_mpdus > 1)
       //mem_blocks += min(num_mpdus, mem_blocks_per_frag);