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-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.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.: 421 476 4030 37601
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.21891999245
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 'ldv_handler_precall' (function is undefined)
Removed calls to 'cxgb3_register_client' (function is undefined)
Removed calls to 'cxgb3_unregister_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.32770085335
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 603 355 1957 29917
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: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:22848: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 4176 bytes on read, may be slow and/or crash: MO151[4176] allocated at global:init_net
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:20034: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:19993: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:20045: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:20045: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:19935: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:19935: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-nMQ8dz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c:19936: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
