bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--infiniband--hw-cxgb3--iw_cxgb3.ko-main.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 430 491 4196 38098
Removed infinite loop in abort_rpl
Removed infinite loop in peer_close
Removed infinite loop in peer_abort
Removed infinite loop in close_con_rpl
Removed infinite loop in rx_data
Removed infinite loop in tx_ack
Removed infinite loop in iwch_modify_qp
Removed infinite loop in iwch_ep_disconnect
Removed infinite loop in __skb_put
Removed infinite loop in accept_cr
Removed infinite loop in reject_cr
Removed infinite loop in send_mpa_req
Removed infinite loop in arch_local_save_flags
Removed infinite loop in iwch_query_gid
Removed infinite loop in iwch_poll_cq
Removed infinite loop in iwch_connect
Removed infinite loop in iwch_accept_cr
Removed infinite loop in iwch_reject_cr
Removed infinite loop in send_mpa_reject
Removed infinite loop in insert_handle___0
Removed infinite loop in __cxio_tpt_op
Removed infinite loop in cxio_hal_put_resource
Removed infinite loop in insert_handle
Removed infinite loop in cxio_poll_cq
INFO: Compilation, preparation and instrumentation time: 1.35491895676
Removed calls to 'ib_dealloc_device' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'synchronize_net' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'dst_release' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'ib_dispatch_event' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function usecs_to_jiffies as symbolic
Defining function schedule_delayed_work as symbolic
Defining function idr_for_each as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function __dynamic_pr_debug as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'cxgb3_remove_tid' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 't3_l2e_free' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_cpu_idle as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 't3_l2t_send_event' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'cxgb3_insert_tid' (function is undefined)
Defining function printk as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function skb_put as symbolic
Defining function cxgb3_ofld_send as symbolic
Defining function t3_l2t_send_slow as symbolic
Defining function __alloc_skb as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function idr_find as symbolic
Defining function skb_pull as symbolic
Defining function t3_l2t_get as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function ip_route_output_flow as symbolic
Defining function cxgb3_free_atid as symbolic
Defining function skb_push as symbolic
Defining function sprintf as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Defining function queue_work as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'ib_unregister_device' (function is undefined)
Removed calls to 'gen_pool_destroy' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__kfifo_free' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function ib_alloc_device as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function strlcpy as symbolic
Removed calls to 'in_dev_finish_destroy' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'ib_umem_release' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'cxgb3_free_stid' (function is undefined)
Defining function ib_register_device as symbolic
Defining function device_create_file as symbolic
Defining function autoremove_wake_function as symbolic
Defining function cxgb3_alloc_stid as symbolic
Defining function cxgb3_alloc_atid as symbolic
Defining function __ip_dev_find as symbolic
Defining function gen_pool_alloc as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'gen_pool_free' (function is undefined)
Defining function __kfifo_in as symbolic
Defining function __kfifo_out as symbolic
Defining function idr_pre_get as symbolic
Defining function idr_get_new_above as symbolic
Defining function ib_umem_get as symbolic
Defining function __get_free_pages as symbolic
Defining function _copy_to_user as symbolic
Defining function __phys_addr as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function remap_pfn_range as symbolic
Defining function strsep as symbolic
Defining function sscanf as symbolic
Defining function dev_get_by_name as symbolic
Defining function dev2t3cdev as symbolic
Defining function gen_pool_create as symbolic
Defining function gen_pool_add_virt as symbolic
Defining function __kfifo_alloc as symbolic
Defining function prandom_u32 as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'dev_kfree_skb_irq' (function is undefined)
Removed calls to 'cxgb3_unregister_client' (function is undefined)
Removed calls to 'cxgb3_register_client' (function is undefined)
Removed calls to 't3_register_cpl_handler' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.3946659565
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 625 370 2031 30177
INFO: Starting verification
KLEE: WARNING ONCE: function "iwch_ep_redirect" has inline asm
KLEE: WARNING ONCE: function "enable_qp_db" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "l2t_release" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "abort_rpl" has inline asm
KLEE: WARNING ONCE: function "peer_close" has inline asm
KLEE: WARNING ONCE: function "peer_abort" has inline asm
KLEE: WARNING ONCE: function "close_con_rpl" has inline asm
KLEE: WARNING ONCE: function "rx_data" has inline asm
KLEE: WARNING ONCE: function "act_establish" has inline asm
KLEE: WARNING ONCE: function "pass_accept_req" has inline asm
KLEE: WARNING ONCE: function "tx_ack" has inline asm
KLEE: WARNING ONCE: function "iwch_modify_qp" has inline asm
KLEE: WARNING ONCE: function "get_skb" has inline asm
KLEE: WARNING ONCE: function "cxio_rdma_init" has inline asm
KLEE: WARNING ONCE: function "flush_qp" has inline asm
KLEE: WARNING ONCE: function "iwch_ep_disconnect" has inline asm
KLEE: WARNING ONCE: function "start_ep_timer" has inline asm
KLEE: WARNING ONCE: function "release_ep_resources" has inline asm
KLEE: WARNING ONCE: function "sched" has inline asm
KLEE: WARNING ONCE: function "cxio_hal_destroy_ctrl_qp" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "cxio_rdev_open" has inline asm
KLEE: WARNING ONCE: function "iwch_query_port" has inline asm
KLEE: WARNING ONCE: function "iwch_query_gid" has inline asm
KLEE: WARNING ONCE: function "iwch_create_qp" has inline asm
KLEE: WARNING ONCE: function "iwch_destroy_qp" has inline asm
KLEE: WARNING ONCE: function "iwch_create_cq" has inline asm
KLEE: WARNING ONCE: function "iwch_destroy_cq" has inline asm
KLEE: WARNING ONCE: function "iwch_poll_cq" has inline asm
KLEE: WARNING ONCE: function "iwch_reg_user_mr" has inline asm
KLEE: WARNING ONCE: function "iwch_bind_mw" has inline asm
KLEE: WARNING ONCE: function "iwch_arm_cq" has inline asm
KLEE: WARNING ONCE: function "iwch_post_send" has inline asm
KLEE: WARNING ONCE: function "iwch_post_receive" has inline asm
KLEE: WARNING ONCE: function "iwch_connect" has inline asm
KLEE: WARNING ONCE: function "iwch_accept_cr" has inline asm
KLEE: WARNING ONCE: function "iwch_reject_cr" has inline asm
KLEE: WARNING ONCE: function "iwch_create_listen" has inline asm
KLEE: WARNING ONCE: function "iwch_destroy_listen" has inline asm
KLEE: WARNING ONCE: function "iwch_qp_add_ref" has inline asm
KLEE: WARNING ONCE: function "iwch_qp_rem_ref" has inline asm
KLEE: WARNING ONCE: function "__cxio_tpt_op" has inline asm
KLEE: WARNING ONCE: function "insert_handle___0" has inline asm
KLEE: WARNING ONCE: function "cxio_hal_ctrl_qp_write_mem" has inline asm
KLEE: WARNING ONCE: function "cxio_hal_put_resource" has inline asm
KLEE: WARNING ONCE: function "cxio_write_pbl" has inline asm
KLEE: WARNING ONCE: function "iwch_finish_mem_reg" has inline asm
KLEE: WARNING ONCE: function "cxio_poll_cq" has inline asm
KLEE: WARNING ONCE: function "iwch_ev_dispatch" has inline asm
KLEE: WARNING ONCE: function "post_qp_event" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 5822 states (over memory cap)
KLEE: WARNING: killing 7802 states (over memory cap)
KLEE: WARNING: killing 8221 states (over memory cap)
KLEE: WARNING: killing 8472 states (over memory cap)
KLEE: WARNING: killing 8500 states (over memory cap)
KLEE: WARNING: killing 8638 states (over memory cap)
KLEE: WARNING: killing 9823 states (over memory cap)
KLEE: WARNING: killing 9902 states (over memory cap)
KLEE: WARNING: killing 10201 states (over memory cap)
KLEE: WARNING: killing 5511 states (over memory cap)
KLEE: WARNING: killing 10151 states (over memory cap)
KLEE: WARNING: killing 5593 states (over memory cap)
KLEE: WARNING: killing 10321 states (over memory cap)
KLEE: WARNING: killing 5567 states (over memory cap)
KLEE: WARNING: killing 5505 states (over memory cap)
KLEE: WARNING: killing 5388 states (over memory cap)
KLEE: WARNING: killing 5379 states (over memory cap)
KLEE: WARNING: killing 5425 states (over memory cap)
KLEE: WARNING: killing 10478 states (over memory cap)
KLEE: WARNING: killing 5718 states (over memory cap)
KLEE: WARNING: killing 5445 states (over memory cap)
KLEE: WARNING: killing 5540 states (over memory cap)
KLEE: WARNING: killing 5693 states (over memory cap)
KLEE: WARNING: killing 5471 states (over memory cap)
KLEE: WARNING: killing 5408 states (over memory cap)
KLEE: WARNING: killing 5558 states (over memory cap)
KLEE: WARNING: killing 5496 states (over memory cap)
KLEE: WARNING: killing 5700 states (over memory cap)
KLEE: WARNING: killing 5745 states (over memory cap)
KLEE: WARNING: killing 5739 states (over memory cap)
KLEE: WARNING: killing 5730 states (over memory cap)
KLEE: WARNING: killing 5618 states (over memory cap)
KLEE: WARNING: killing 5712 states (over memory cap)
KLEE: WARNING: killing 5703 states (over memory cap)
KLEE: WARNING: killing 5697 states (over memory cap)
KLEE: WARNING: killing 5637 states (over memory cap)
KLEE: WARNING: killing 5680 states (over memory cap)
KLEE: WARNING: killing 5724 states (over memory cap)
KLEE: WARNING: killing 5717 states (over memory cap)
KLEE: WARNING: killing 5605 states (over memory cap)
KLEE: WARNING: killing 5699 states (over memory cap)
KLEE: WARNING: killing 5639 states (over memory cap)
KLEE: WARNING: killing 5633 states (over memory cap)
KLEE: WARNING: killing 5674 states (over memory cap)
KLEE: WARNING: killing 5615 states (over memory cap)
KLEE: WARNING: killing 5761 states (over memory cap)
KLEE: WARNING: killing 5753 states (over memory cap)
KLEE: WARNING: killing 5748 states (over memory cap)
KLEE: WARNING: killing 5840 states (over memory cap)
KLEE: WARNING: killing 5732 states (over memory cap)
KLEE: WARNING: killing 5774 states (over memory cap)
KLEE: WARNING: killing 5564 states (over memory cap)
KLEE: WARNING: killing 5708 states (over memory cap)
KLEE: WARNING: killing 5753 states (over memory cap)
KLEE: WARNING: killing 5949 states (over memory cap)
KLEE: WARNING: killing 5637 states (over memory cap)
KLEE: WARNING: killing 5678 states (over memory cap)
KLEE: WARNING: killing 5622 states (over memory cap)
KLEE: WARNING: killing 5666 states (over memory cap)
KLEE: WARNING: killing 5809 states (over memory cap)
KLEE: WARNING: killing 5702 states (over memory cap)
KLEE: WARNING: killing 5694 states (over memory cap)
KLEE: WARNING: killing 5638 states (over memory cap)
KLEE: WARNING: killing 5981 states (over memory cap)
KLEE: WARNING: killing 5726 states (over memory cap)
KLEE: WARNING: killing 5818 states (over memory cap)
KLEE: WARNING: killing 5712 states (over memory cap)
KLEE: WARNING: killing 5654 states (over memory cap)
KLEE: WARNING: killing 5694 states (over memory cap)
KLEE: WARNING: killing 5788 states (over memory cap)
KLEE: WARNING: killing 5831 states (over memory cap)
KLEE: WARNING: killing 5726 states (over memory cap)
KLEE: WARNING: killing 5715 states (over memory cap)
KLEE: WARNING: killing 5611 states (over memory cap)
KLEE: WARNING: killing 5704 states (over memory cap)
KLEE: WARNING: killing 5795 states (over memory cap)
KLEE: WARNING: killing 5790 states (over memory cap)
KLEE: WARNING: killing 5783 states (over memory cap)
KLEE: WARNING: killing 5780 states (over memory cap)
KLEE: WARNING: killing 5722 states (over memory cap)
KLEE: WARNING: killing 5715 states (over memory cap)
KLEE: WARNING: killing 5560 states (over memory cap)
KLEE: WARNING: killing 5752 states (over memory cap)
KLEE: WARNING: killing 5745 states (over memory cap)
KLEE: WARNING: killing 5884 states (over memory cap)
KLEE: WARNING: killing 5780 states (over memory cap)
KLEE: WARNING: killing 5773 states (over memory cap)
KLEE: WARNING: killing 5767 states (over memory cap)
KLEE: WARNING: killing 5762 states (over memory cap)
KLEE: WARNING: killing 5756 states (over memory cap)
KLEE: WARNING: killing 5699 states (over memory cap)
KLEE: WARNING: killing 5791 states (over memory cap)
KLEE: WARNING: killing 5640 states (over memory cap)
KLEE: WARNING: killing 5628 states (over memory cap)
KLEE: WARNING: killing 5720 states (over memory cap)
KLEE: WARNING: killing 5811 states (over memory cap)
KLEE: WARNING: killing 5711 states (over memory cap)
KLEE: WARNING: killing 5752 states (over memory cap)
KLEE: WARNING: killing 5743 states (over memory cap)
KLEE: WARNING: killing 5739 states (over memory cap)
KLEE: WARNING: killing 5538 states (over memory cap)
KLEE: WARNING: killing 5678 states (over memory cap)
KLEE: WARNING: killing 5814 states (over memory cap)
KLEE: WARNING: killing 5810 states (over memory cap)
KLEE: WARNING: killing 5901 states (over memory cap)
KLEE: WARNING: killing 5608 states (over memory cap)
KLEE: WARNING: killing 5792 states (over memory cap)
KLEE: WARNING: killing 5691 states (over memory cap)
KLEE: WARNING: killing 5828 states (over memory cap)
KLEE: WARNING: killing 5823 states (over memory cap)
KLEE: WARNING: killing 5912 states (over memory cap)
KLEE: WARNING: killing 5765 states (over memory cap)
KLEE: WARNING: killing 5566 states (over memory cap)
KLEE: WARNING: killing 5555 states (over memory cap)
KLEE: WARNING: killing 5644 states (over memory cap)
KLEE: WARNING: killing 5782 states (over memory cap)
KLEE: WARNING: killing 5726 states (over memory cap)
KLEE: WARNING: killing 5814 states (over memory cap)
KLEE: WARNING: killing 5715 states (over memory cap)
KLEE: WARNING: killing 5615 states (over memory cap)
KLEE: WARNING: killing 5654 states (over memory cap)
KLEE: WARNING: killing 5789 states (over memory cap)
KLEE: WARNING: killing 5784 states (over memory cap)
KLEE: WARNING: killing 5779 states (over memory cap)
KLEE: WARNING: killing 5774 states (over memory cap)
KLEE: WARNING: killing 5720 states (over memory cap)
KLEE: WARNING: killing 5805 states (over memory cap)
KLEE: WARNING: killing 5755 states (over memory cap)
KLEE: WARNING: killing 5841 states (over memory cap)
KLEE: WARNING: killing 5698 states (over memory cap)
KLEE: WARNING: killing 5785 states (over memory cap)
KLEE: WARNING: killing 5690 states (over memory cap)
KLEE: WARNING: killing 5823 states (over memory cap)
KLEE: WARNING: killing 5725 states (over memory cap)
KLEE: WARNING: killing 5668 states (over memory cap)
KLEE: WARNING: killing 5615 states (over memory cap)
KLEE: WARNING: killing 5843 states (over memory cap)
KLEE: WARNING: killing 5652 states (over memory cap)
KLEE: WARNING: killing 5737 states (over memory cap)
KLEE: WARNING: killing 5684 states (over memory cap)
KLEE: WARNING: killing 5630 states (over memory cap)
KLEE: WARNING: killing 5719 states (over memory cap)
KLEE: WARNING: killing 5806 states (over memory cap)
KLEE: WARNING: killing 5657 states (over memory cap)
KLEE: WARNING: killing 5791 states (over memory cap)
KLEE: WARNING: killing 5829 states (over memory cap)
KLEE: WARNING: killing 5641 states (over memory cap)
KLEE: WARNING: killing 5772 states (over memory cap)
KLEE: WARNING: killing 5675 states (over memory cap)
KLEE: WARNING: killing 5808 states (over memory cap)
KLEE: WARNING: killing 5660 states (over memory cap)
KLEE: WARNING: killing 5795 states (over memory cap)
KLEE: WARNING: killing 5697 states (over memory cap)
KLEE: WARNING: killing 5691 states (over memory cap)
KLEE: WARNING: killing 5820 states (over memory cap)
KLEE: WARNING: killing 5722 states (over memory cap)
KLEE: WARNING: killing 5670 states (over memory cap)
KLEE: WARNING: killing 5758 states (over memory cap)
KLEE: WARNING: killing 5751 states (over memory cap)
KLEE: WARNING: killing 5699 states (over memory cap)
KLEE: WARNING: killing 5736 states (over memory cap)
KLEE: WARNING: killing 5778 states (over memory cap)
KLEE: WARNING: killing 5773 states (over memory cap)
KLEE: WARNING: killing 5629 states (over memory cap)
KLEE: WARNING: killing 5806 states (over memory cap)
KLEE: WARNING: killing 5798 states (over memory cap)
KLEE: WARNING: killing 5612 states (over memory cap)
KLEE: WARNING: killing 5651 states (over memory cap)
KLEE: WARNING: killing 5601 states (over memory cap)
KLEE: WARNING: killing 5681 states (over memory cap)
KLEE: WARNING: killing 5675 states (over memory cap)
KLEE: WARNING: killing 5807 states (over memory cap)
KLEE: WARNING: killing 5802 states (over memory cap)
KLEE: WARNING: killing 5750 states (over memory cap)
KLEE: WARNING: killing 5697 states (over memory cap)
KLEE: WARNING: killing 5738 states (over memory cap)
KLEE: WARNING: killing 5775 states (over memory cap)
KLEE: WARNING: killing 5680 states (over memory cap)
KLEE: WARNING: killing 5671 states (over memory cap)
KLEE: WARNING: killing 5713 states (over memory cap)
KLEE: WARNING: killing 5794 states (over memory cap)
KLEE: WARNING: killing 5569 states (over memory cap)
KLEE: WARNING: killing 5694 states (over memory cap)
KLEE: WARNING: killing 5867 states (over memory cap)
KLEE: WARNING: killing 5679 states (over memory cap)
KLEE: WARNING: killing 5852 states (over memory cap)
KLEE: WARNING: killing 5758 states (over memory cap)
