bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.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.: 405 802 6807 48468
Removed infinite loop in mlx4_en_is_ring_empty
Removed infinite loop in dma_unmap_page___0
Removed infinite loop in napi_enable
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in dma_map_page___0
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dql_queued
Removed infinite loop in dma_map_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.91915798187
Defining function ethtool_op_get_link as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mlx4_free_cmd_mailbox' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function mlx4_SET_PORT_general as symbolic
Removed calls to 'bitmap_clear' (function is undefined)
Removed calls to 'bitmap_set' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function printk as symbolic
Defining function mlx4_alloc_cmd_mailbox as symbolic
Defining function __mlx4_cmd as symbolic
Defining function mlx4_SET_PORT_SCHEDULER as symbolic
Defining function mlx4_SET_PORT_PRIO2TC as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'mlx4_uar_free' (function is undefined)
Removed calls to 'mlx4_pd_free' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'mlx4_free_hwq_res' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Defining function mlx4_mr_free as symbolic
Defining function unregister_netdevice_notifier as symbolic
Removed calls to '_raw_write_unlock_irqrestore' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function _raw_write_lock_irqsave as symbolic
Defining function timecounter_read as symbolic
Defining function ptp_clock_unregister as symbolic
Removed calls to 'mlx4_bf_free' (function is undefined)
Removed calls to 'mlx4_qp_remove' (function is undefined)
Removed calls to 'mlx4_qp_free' (function is undefined)
Removed calls to 'mlx4_qp_release_range' (function is undefined)
Removed calls to 'kvfree' (function is undefined)
Removed calls to 'mlx4_release_eq' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function mlx4_flow_detach as symbolic
Defining function cancel_work_sync as symbolic
Defining function mlx4_is_eq_vector_valid as symbolic
Defining function cancel_delayed_work as symbolic
Defining function mlx4_pd_alloc as symbolic
Defining function mlx4_uar_alloc as symbolic
Defining function mlx4_mr_alloc as symbolic
Defining function mlx4_mr_enable as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to 'timecounter_init' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
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 'netdev_rss_key_fill' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function register_netdevice_notifier as symbolic
Defining function netdev_master_upper_dev_get as symbolic
Defining function mlx4_bond as symbolic
Defining function mlx4_port_map_set as symbolic
Defining function mlx4_unbond as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function netif_set_real_num_tx_queues as symbolic
Defining function netif_set_real_num_rx_queues as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'mlx4_unregister_mac' (function is undefined)
Removed calls to 'kfree_call_rcu' (function is undefined)
Defining function mlx4_alloc_hwq_res as symbolic
Defining function mlx4_SET_PORT_VXLAN as symbolic
Defining function mlx4_INIT_PORT as symbolic
Defining function register_netdev as symbolic
Defining function __cpu_to_node as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function mlx4_get_cpu_rmap as symbolic
Defining function vmalloc_node as symbolic
Defining function vmalloc as symbolic
Defining function __phys_addr as symbolic
Defining function __kmalloc_node as symbolic
Defining function mlx4_qp_reserve_range as symbolic
Defining function mlx4_qp_alloc as symbolic
Defining function mlx4_bf_alloc as symbolic
Defining function cpumask_local_spread as symbolic
Defining function __bitmap_weight as symbolic
Defining function mlx4_config_vxlan_port as symbolic
Removed calls to 'synchronize_sched' (function is undefined)
Defining function mlx4_register_mac as symbolic
Defining function __mlx4_replace_mac as symbolic
Defining function mlx4_tunnel_steer_add as symbolic
Defining function mlx4_unicast_attach as symbolic
Defining function mlx4_flow_attach as symbolic
Defining function mlx4_unicast_detach as symbolic
Defining function mlx4_cq_modify as symbolic
Defining function mlx4_get_default_counter_index as symbolic
Defining function mlx4_get_counter_stats as symbolic
Removed calls to '__local_bh_disable_ip' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'netif_tx_stop_all_queues' (function is undefined)
Removed calls to 'netif_schedule_queue' (function is undefined)
Removed calls to '__local_bh_enable_ip' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Removed calls to 'vxlan_get_rx_port' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to 'napi_hash_add' (function is undefined)
Removed calls to 'napi_disable' (function is undefined)
Removed calls to 'napi_hash_del' (function is undefined)
Removed calls to 'netif_napi_del' (function is undefined)
Removed calls to 'mlx4_cq_free' (function is undefined)
Defining function mlx4_SET_PORT_qpn_calc as symbolic
Defining function mlx4_multicast_attach as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function mlx4_qp_modify as symbolic
Defining function mlx4_qp_to_ready as symbolic
Defining function netif_set_xps_queue as symbolic
Defining function find_first_bit as symbolic
Defining function mlx4_get_base_qpn as symbolic
Defining function mlx4_assign_eq as symbolic
Defining function mlx4_eq_get_irq as symbolic
Defining function irq_to_desc as symbolic
Defining function mlx4_cq_alloc as symbolic
Removed calls to 'dql_completed' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to 'napi_complete_done' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function napi_get_frags as symbolic
Removed calls to '_raw_read_unlock_irqrestore' (function is undefined)
Defining function napi_gro_frags as symbolic
Defining function eth_type_trans as symbolic
Defining function napi_gro_receive as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function alloc_pages_current as symbolic
Defining function netif_receive_skb_sk as symbolic
Defining function eth_get_headlen as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function _raw_read_lock_irqsave as symbolic
Defining function timecounter_cyc2time as symbolic
Defining function csum_partial as symbolic
Defining function rcu_is_watching as symbolic
Removed calls to 'skb_tstamp_tx' (function is undefined)
Removed calls to '__napi_schedule_irqoff' (function is undefined)
Defining function zalloc_cpumask_var as symbolic
Defining function mlx4_CLOSE_PORT as symbolic
Defining function mlx4_flow_steer_promisc_remove as symbolic
Defining function mlx4_unicast_promisc_remove as symbolic
Defining function mlx4_multicast_promisc_remove as symbolic
Defining function mlx4_multicast_detach as symbolic
Defining function mlx4_SET_MCAST_FLTR as symbolic
Defining function rtnl_is_locked as symbolic
Removed calls to 'dql_reset' (function is undefined)
Defining function mlx4_flow_steer_promisc_add as symbolic
Defining function mlx4_multicast_promisc_add as symbolic
Defining function kmemdup as symbolic
Defining function mlx4_unicast_promisc_add as symbolic
Defining function mlx4_get_eqs_per_port as symbolic
Defining function netif_get_num_default_rss_queues as symbolic
Defining function snprintf as symbolic
Defining function ptp_clock_register as symbolic
Defining function ktime_get_with_offset as symbolic
Defining function mlx4_read_clock as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'skb_clone_tx_timestamp' (function is undefined)
Removed calls to '__iowrite64_copy' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Defining function eth_validate_addr as symbolic
Removed calls to 'mlx4_unregister_vlan' (function is undefined)
Defining function mlx4_update_qp as symbolic
Defining function __pskb_pull_tail as symbolic
Defining function mlx4_SET_PORT_fcs_check as symbolic
Removed calls to 'netdev_features_change' (function is undefined)
Defining function rps_may_expire_flow as symbolic
Defining function mlx4_get_vf_stats as symbolic
Defining function mlx4_set_vf_link_state as symbolic
Defining function mlx4_get_vf_config as symbolic
Defining function mlx4_set_vf_spoofchk as symbolic
Defining function mlx4_set_vf_rate as symbolic
Defining function mlx4_set_vf_vlan as symbolic
Defining function mlx4_set_vf_mac as symbolic
Defining function mlx4_register_vlan as symbolic
Defining function __skb_tx_hash as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function ns_to_timespec as symbolic
Defining function mlx4_get_module_info as symbolic
Defining function ethtool_op_get_ts_info as symbolic
Defining function ptp_clock_index as symbolic
Defining function mlx4_SET_PORT_BEACON as symbolic
Defining function sprintf as symbolic
Defining function mlx4_test_interrupts as symbolic
Defining function skb_put as symbolic
Defining function mlx4_wol_read as symbolic
Defining function mlx4_wol_write as symbolic
Defining function strlcpy as symbolic
Defining function mlx4_ACCESS_PTYS_REG as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'mlx4_unregister_interface' (function is undefined)
Defining function ldv_ndo_init_14 as symbolic
Defining function ldv_ndo_uninit_14 as symbolic
Defining function ldv_ndo_init_13 as symbolic
Defining function ldv_ndo_uninit_13 as symbolic
Defining function mlx4_register_interface as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 1.9831058979
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 603 639 4126 28097
INFO: Starting verification
KLEE: WARNING ONCE: function "mlx4_en_set_ringparam" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_get_strings" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_get_ethtool_stats" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_get_rxfh" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_recover_from_oom" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_set_num_rx_rings" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_netdev_event" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_bond_work" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_calc_rx_buf" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_create_tx_ring" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_create_rx_ring" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_stop_port" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_start_port" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_activate_rx_rings" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_activate_cq" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_arm_cq" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_config_rss_steer" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_free_rx_buf" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_fill_qp_context" has inline asm
KLEE: WARNING ONCE: function "napi_schedule_irqoff" has inline asm
KLEE: WARNING ONCE: function "mlx4_alloc_pages" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_free_tx_buf" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_free_tx_desc" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_xmit" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_vlan_rx_add_vid" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_vlan_rx_kill_vid" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_netpoll" has inline asm
KLEE: WARNING ONCE: function "mlx4_SET_VLAN_FLTR" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_process_rx_cq" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "check_csum" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_poll_tx_cq" has inline asm
KLEE: WARNING ONCE: function "mlx4_en_poll_rx_cq" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_fbde82a4-ebd9-4d5d-911f-d87213306fbf/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15299 states (over memory cap)
KLEE: WARNING: killing 10523 states (over memory cap)
KLEE: WARNING: killing 10794 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31408: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10464 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31393: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:8656: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10497 states (over memory cap)
KLEE: WARNING: killing 10954 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:30843: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31226: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31694: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31618: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11402 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31361: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31540: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11379 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31465: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31393: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12314 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:8789: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12105 states (over memory cap)
KLEE: WARNING: killing 12676 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17075: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:16969: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:18254: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:30438: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12657 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:16688: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:15697: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:16855: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17120: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:15714: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17887: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17997: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17936: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:15761: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:16912: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:18058: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:14998: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:16941: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:15923: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:15870: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13384 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:31297: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13781 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:18151: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17920: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13461 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 13716 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_fbde82a4-ebd9-4d5d-911f-d87213306fbf/symbiotic/lib/libc/strcpy.c:6: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:17042: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13697 states (over memory cap)
KLEE: WARNING: killing 13613 states (over memory cap)
KLEE: WARNING: killing 13646 states (over memory cap)
KLEE: WARNING: killing 13677 states (over memory cap)
KLEE: WARNING: killing 13720 states (over memory cap)
KLEE: WARNING: killing 13575 states (over memory cap)
KLEE: WARNING: killing 13143 states (over memory cap)
KLEE: WARNING: killing 13070 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 13546 states (over memory cap)
KLEE: WARNING: killing 13233 states (over memory cap)
KLEE: WARNING: killing 13152 states (over memory cap)
KLEE: WARNING: killing 13185 states (over memory cap)
KLEE: WARNING: killing 13567 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 14097 states (over memory cap)
KLEE: WARNING: killing 14076 states (over memory cap)
KLEE: WARNING: killing 13656 states (over memory cap)
KLEE: WARNING: killing 14155 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 13717 states (over memory cap)
KLEE: WARNING: killing 13300 states (over memory cap)
KLEE: WARNING: killing 13565 states (over memory cap)
KLEE: WARNING: killing 14113 states (over memory cap)
KLEE: WARNING: killing 14094 states (over memory cap)
KLEE: WARNING: killing 13448 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:8684: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13315 states (over memory cap)
KLEE: WARNING: killing 13580 states (over memory cap)
KLEE: WARNING: killing 14131 states (over memory cap)
KLEE: WARNING: killing 14171 states (over memory cap)
KLEE: WARNING: killing 13869 states (over memory cap)
KLEE: WARNING: killing 13914 states (over memory cap)
KLEE: WARNING: killing 13269 states (over memory cap)
KLEE: WARNING: killing 13534 states (over memory cap)
KLEE: WARNING: killing 14082 states (over memory cap)
KLEE: WARNING: killing 13623 states (over memory cap)
KLEE: WARNING: killing 13884 states (over memory cap)
KLEE: WARNING: killing 13417 states (over memory cap)
KLEE: WARNING: killing 13786 states (over memory cap)
KLEE: WARNING: killing 13829 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YmGRks/linux-4.2-rc1.tar.xz-32_7a-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko-entry_point_true-unreach-call.cil.out.c:16771: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 13518 states (over memory cap)
KLEE: WARNING: killing 14003 states (over memory cap)
KLEE: WARNING: killing 13430 states (over memory cap)
KLEE: WARNING: killing 13684 states (over memory cap)
KLEE: WARNING: killing 14063 states (over memory cap)
KLEE: WARNING: killing 13879 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
KLEE: WARNING: killing 13732 states (over memory cap)
KLEE: WARNING: killing 13998 states (over memory cap)
KLEE: WARNING: killing 13707 states (over memory cap)
KLEE: WARNING: killing 13964 states (over memory cap)
KLEE: WARNING: killing 13841 states (over memory cap)
KLEE: WARNING: killing 13945 states (over memory cap)
KLEE: WARNING: killing 13762 states (over memory cap)
KLEE: WARNING: killing 13363 states (over memory cap)
KLEE: WARNING: killing 13406 states (over memory cap)
KLEE: WARNING: killing 13827 states (over memory cap)
KLEE: WARNING: killing 13595 states (over memory cap)
KLEE: WARNING: killing 13636 states (over memory cap)
KLEE: WARNING: killing 13566 states (over memory cap)
KLEE: WARNING: killing 13602 states (over memory cap)
KLEE: WARNING: killing 13862 states (over memory cap)
KLEE: WARNING: killing 13909 states (over memory cap)
KLEE: WARNING: killing 14164 states (over memory cap)
KLEE: WARNING: killing 13393 states (over memory cap)
KLEE: WARNING: killing 13601 states (over memory cap)
KLEE: WARNING: killing 13201 states (over memory cap)
KLEE: WARNING: killing 13402 states (over memory cap)
KLEE: WARNING: killing 13982 states (over memory cap)
KLEE: WARNING: killing 13701 states (over memory cap)
KLEE: WARNING: killing 14021 states (over memory cap)
KLEE: WARNING: killing 14007 states (over memory cap)
KLEE: WARNING: killing 14480 states (over memory cap)
KLEE: WARNING: killing 13814 states (over memory cap)
KLEE: WARNING: killing 13481 states (over memory cap)
KLEE: WARNING: killing 13030 states (over memory cap)
KLEE: WARNING: killing 13499 states (over memory cap)
KLEE: WARNING: killing 14125 states (over memory cap)
KLEE: WARNING: killing 13311 states (over memory cap)
KLEE: WARNING: killing 13675 states (over memory cap)
KLEE: WARNING: killing 13765 states (over memory cap)
KLEE: WARNING: killing 14137 states (over memory cap)
KLEE: WARNING: killing 13588 states (over memory cap)
KLEE: WARNING: killing 13840 states (over memory cap)
KLEE: WARNING: killing 13880 states (over memory cap)
KLEE: WARNING: killing 13704 states (over memory cap)
KLEE: WARNING: killing 13805 states (over memory cap)
KLEE: WARNING: killing 13631 states (over memory cap)
KLEE: WARNING: killing 13878 states (over memory cap)
KLEE: WARNING: killing 13924 states (over memory cap)
KLEE: WARNING: killing 13694 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
KLEE: WARNING: killing 14048 states (over memory cap)
KLEE: WARNING: killing 13610 states (over memory cap)
KLEE: WARNING: killing 13491 states (over memory cap)
KLEE: WARNING: killing 13527 states (over memory cap)
KLEE: WARNING: killing 13461 states (over memory cap)
KLEE: WARNING: killing 13396 states (over memory cap)
KLEE: WARNING: killing 13489 states (over memory cap)
KLEE: WARNING: killing 13108 states (over memory cap)
KLEE: WARNING: killing 13462 states (over memory cap)
KLEE: WARNING: killing 14081 states (over memory cap)
KLEE: WARNING: killing 14225 states (over memory cap)
KLEE: WARNING: killing 13894 states (over memory cap)
KLEE: WARNING: killing 14201 states (over memory cap)
KLEE: WARNING: killing 13724 states (over memory cap)
KLEE: WARNING: killing 13863 states (over memory cap)
