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--infiniband--ulp--ipoib--ib_ipoib.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.: 468 700 5648 36999
Removed infinite loop in skb_orphan
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_page
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in skb_orphan___0
Removed infinite loop in dma_unmap_single_attrs___0
Removed infinite loop in dma_map_single_attrs___0
Removed infinite loop in dma_unmap_page___0
Removed infinite loop in dma_map_page___0
Removed infinite loop in dma_sync_single_for_device
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in napi_enable
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.26283407211
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function jiffies_to_msecs as symbolic
Defining function printk as symbolic
Defining function queue_work_on as symbolic
Removed calls to '__local_bh_disable_ip' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to '__local_bh_enable_ip' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function skb_pull as symbolic
Removed calls to 'dst_release' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function ib_query_qp as symbolic
Defining function ib_modify_qp as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function rcu_read_lock_held as symbolic
Defining function rcu_read_lock_bh_held as symbolic
Defining function mod_timer as symbolic
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'rb_insert_color' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'call_rcu_sched' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function lock_is_held as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function ib_sa_path_rec_get as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function ib_init_ah_from_path as symbolic
Defining function dev_queue_xmit_sk as symbolic
Defining function ib_create_ah as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function cancel_delayed_work as symbolic
Defining function rcu_is_watching as symbolic
Removed calls to 'napi_disable' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function dev_change_flags as symbolic
Removed calls to 'ib_destroy_cm_id' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function round_jiffies_relative as symbolic
Defining function ib_destroy_ah as symbolic
Removed calls to 'netif_schedule_queue' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function ib_destroy_qp as symbolic
Defining function del_timer_sync as symbolic
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Defining function skb_put as symbolic
Defining function napi_gro_receive as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function netif_receive_skb_sk as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'ib_sa_cancel_query' (function is undefined)
Removed calls to 'ib_sa_free_multicast' (function is undefined)
Defining function skb_dequeue as symbolic
Defining function ib_detach_mcast as symbolic
Defining function ib_find_pkey as symbolic
Defining function ib_create_cm_id as symbolic
Defining function ib_cm_listen as symbolic
Defining function ib_send_cm_drep as symbolic
Defining function prandom_u32 as symbolic
Defining function ib_send_cm_rep as symbolic
Defining function vzalloc as symbolic
Defining function ib_send_cm_rej as symbolic
Defining function ib_cm_init_qp_attr as symbolic
Defining function ib_create_qp as symbolic
Removed calls to 'dump_stack' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'unregister_netdevice_many' (function is undefined)
Defining function rtnl_is_locked as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function ib_destroy_cq as symbolic
Defining function ib_dereg_mr as symbolic
Defining function ib_dealloc_pd as symbolic
Defining function ib_destroy_srq as symbolic
Defining function skb_push as symbolic
Defining function simple_strtoul as symbolic
Defining function sprintf as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'ib_set_client_data' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Defining function ib_get_client_data as symbolic
Defining function ib_unregister_event_handler as symbolic
Defining function ib_query_port as symbolic
Defining function ib_query_pkey as symbolic
Defining function ib_query_gid as symbolic
Defining function ib_register_event_handler as symbolic
Defining function device_create_file as symbolic
Defining function snprintf as symbolic
Defining function debugfs_create_file as symbolic
Defining function register_netdev as symbolic
Defining function ib_alloc_pd as symbolic
Defining function ib_get_dma_mr as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function ib_create_cq as symbolic
Removed calls to 'icmp_send' (function is undefined)
Removed calls to 'icmpv6_send' (function is undefined)
Defining function ib_query_device as symbolic
Defining function ib_create_srq as symbolic
Defining function __vmalloc as symbolic
Defining function ib_send_cm_req as symbolic
Defining function ib_send_cm_rtu as symbolic
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Defining function alloc_netdev_mqs as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'rb_replace_node' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function ib_sa_get_mcmember_rec as symbolic
Defining function rtnl_trylock as symbolic
Defining function dev_set_mtu as symbolic
Defining function ib_sa_join_multicast as symbolic
Defining function ib_attach_mcast as symbolic
Defining function sscanf as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function capable as symbolic
Defining function register_netdevice as symbolic
Defining function ib_modify_cq as symbolic
Defining function strlcpy as symbolic
Defining function nla_put as symbolic
Removed calls to 'netdev_update_features' (function is undefined)
Defining function __dev_get_by_index as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release as symbolic
Defining function seq_open as symbolic
Defining function seq_printf as symbolic
Defining function rb_first as symbolic
Defining function rb_next as symbolic
Defining function ib_rate_to_mbps as symbolic
Defining function seq_putc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'rtnl_link_unregister' (function is undefined)
Removed calls to 'ib_unregister_client' (function is undefined)
Removed calls to 'ib_sa_unregister_client' (function is undefined)
Removed calls to 'ib_sa_register_client' (function is undefined)
Defining function ldv_ndo_init_28 as symbolic
Defining function ib_register_client as symbolic
Defining function rtnl_link_register as symbolic
Defining function debugfs_create_dir as symbolic
Defining function ldv_release_21 as symbolic
Defining function ldv_init_21 as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  __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.23209309578
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 643 590 3372 22997
INFO: Starting verification
KLEE: WARNING ONCE: function "ipoib_open" has inline asm
KLEE: WARNING ONCE: function "ipoib_stop" has inline asm
KLEE: WARNING ONCE: function "ipoib_neigh_get" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_send" has inline asm
KLEE: WARNING ONCE: function "ipoib_neigh_alloc" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "ipoib_cm_create_tx" has inline asm
KLEE: WARNING ONCE: function "ipoib_send" has inline asm
KLEE: WARNING ONCE: function "ipoib_neigh_put" has inline asm
KLEE: WARNING ONCE: function "ipoib_cm_send" has inline asm
KLEE: WARNING ONCE: function "ib_dma_map_single___0" has inline asm
KLEE: WARNING ONCE: function "ib_dma_unmap_single___0" has inline asm
KLEE: WARNING ONCE: function "ipoib_put_ah" has inline asm
KLEE: WARNING ONCE: function "ipoib_neigh_dtor" has inline asm
KLEE: WARNING ONCE: function "ipoib_cm_destroy_tx" has inline asm
KLEE: WARNING ONCE: function "ib_dma_map_single" has inline asm
KLEE: WARNING ONCE: function "ib_dma_unmap_single" has inline asm
KLEE: WARNING ONCE: function "ipoib_ib_dev_down" has inline asm
KLEE: WARNING ONCE: function "ipoib_ib_dev_stop" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock___0" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock___0" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock___2" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock___2" has inline asm
KLEE: WARNING ONCE: function "ipoib_cm_handle_tx_wc" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock_bh" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock_bh" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_leave" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock_bh___1" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock_bh___1" has inline asm
KLEE: WARNING ONCE: function "ipoib_ib_dev_open" has inline asm
KLEE: WARNING ONCE: function "ipoib_ib_dev_up" has inline asm
KLEE: WARNING ONCE: function "ipoib_pkey_dev_check_presence" has inline asm
KLEE: WARNING ONCE: function "napi_enable" has inline asm
KLEE: WARNING ONCE: function "ipoib_dev_cleanup" has inline asm
KLEE: WARNING ONCE: function "ipoib_ib_dev_cleanup" has inline asm
KLEE: WARNING ONCE: function "ipoib_transport_dev_cleanup" has inline asm
KLEE: WARNING ONCE: function "ipoib_set_umcast" has inline asm
KLEE: WARNING ONCE: function "ipoib_add_one" has inline asm
KLEE: WARNING ONCE: function "ipoib_remove_one" has inline asm
KLEE: WARNING ONCE: function "ipoib_dev_init" has inline asm
KLEE: WARNING ONCE: function "ipoib_ib_completion" has inline asm
KLEE: WARNING ONCE: function "ipoib_cm_tx_handler" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_join_task" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_restart_task" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "__ipoib_ib_dev_flush" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_join" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_join_complete" has inline asm
KLEE: WARNING ONCE: function "ipoib_mcast_attach" has inline asm
KLEE: WARNING ONCE: function "ipoib_vlan_add" has inline asm
KLEE: WARNING ONCE: function "__ipoib_vlan_add" has inline asm
KLEE: WARNING ONCE: function "ipoib_vlan_delete" has inline asm
KLEE: WARNING ONCE: function "ipoib_set_mode" has inline asm
KLEE: WARNING ONCE: function "set_mode" has inline asm
KLEE: WARNING ONCE: function "ipoib_poll" has inline asm
KLEE: WARNING ONCE: function "main" 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_69f0f36e-571d-4ef2-a248-acfc30f7a7f6/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YiKYd3/linux-4.2-rc1.tar.xz-32_7a-drivers--infiniband--ulp--ipoib--ib_ipoib.ko-entry_point_true-unreach-call.cil.out.c:7720: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11486 states (over memory cap)
KLEE: WARNING: killing 23770 states (over memory cap)
KLEE: WARNING: killing 23231 states (over memory cap)
KLEE: WARNING: killing 22860 states (over memory cap)
KLEE: WARNING: killing 23312 states (over memory cap)
KLEE: WARNING: killing 23621 states (over memory cap)
KLEE: WARNING: killing 22089 states (over memory cap)
KLEE: WARNING: killing 21483 states (over memory cap)
KLEE: WARNING: killing 22874 states (over memory cap)
KLEE: WARNING: killing 23090 states (over memory cap)
KLEE: WARNING: killing 24178 states (over memory cap)
KLEE: WARNING: killing 24750 states (over memory cap)
KLEE: WARNING: killing 24922 states (over memory cap)
KLEE: WARNING: killing 25048 states (over memory cap)
KLEE: WARNING: killing 24415 states (over memory cap)
KLEE: WARNING: killing 24323 states (over memory cap)
KLEE: WARNING: killing 24501 states (over memory cap)
KLEE: WARNING: killing 23312 states (over memory cap)
KLEE: WARNING: killing 23628 states (over memory cap)
KLEE: WARNING: killing 23498 states (over memory cap)
KLEE: WARNING: killing 22101 states (over memory cap)
KLEE: WARNING: killing 24341 states (over memory cap)
KLEE: WARNING: killing 22852 states (over memory cap)
KLEE: WARNING: killing 24231 states (over memory cap)
KLEE: WARNING: killing 25020 states (over memory cap)
KLEE: WARNING: killing 24295 states (over memory cap)
KLEE: WARNING: killing 24111 states (over memory cap)
KLEE: WARNING: killing 24892 states (over memory cap)
KLEE: WARNING: killing 22870 states (over memory cap)
KLEE: WARNING: killing 24279 states (over memory cap)
KLEE: WARNING: killing 22205 states (over memory cap)
KLEE: WARNING: killing 24025 states (over memory cap)
KLEE: WARNING: killing 24898 states (over memory cap)
KLEE: WARNING: killing 22979 states (over memory cap)
KLEE: WARNING: killing 23992 states (over memory cap)
KLEE: WARNING: killing 24661 states (over memory cap)
KLEE: WARNING: killing 24289 states (over memory cap)
KLEE: WARNING: killing 23322 states (over memory cap)
KLEE: WARNING: killing 24145 states (over memory cap)
KLEE: WARNING: killing 24610 states (over memory cap)
KLEE: WARNING: killing 25079 states (over memory cap)
KLEE: WARNING: killing 24467 states (over memory cap)
KLEE: WARNING: killing 23052 states (over memory cap)
KLEE: WARNING: killing 24404 states (over memory cap)
KLEE: WARNING: killing 23201 states (over memory cap)
KLEE: WARNING: killing 22531 states (over memory cap)
KLEE: WARNING: killing 24513 states (over memory cap)
KLEE: WARNING: killing 23792 states (over memory cap)
KLEE: WARNING: killing 23228 states (over memory cap)
KLEE: WARNING: killing 24629 states (over memory cap)
KLEE: WARNING: killing 24508 states (over memory cap)
KLEE: WARNING: killing 23756 states (over memory cap)
KLEE: WARNING: killing 23726 states (over memory cap)
KLEE: WARNING: killing 23757 states (over memory cap)
KLEE: WARNING: killing 23729 states (over memory cap)
KLEE: WARNING: killing 23993 states (over memory cap)
KLEE: WARNING: killing 24214 states (over memory cap)
KLEE: WARNING: killing 24144 states (over memory cap)
KLEE: WARNING: killing 24251 states (over memory cap)
KLEE: WARNING: killing 23221 states (over memory cap)
KLEE: WARNING: killing 24399 states (over memory cap)
KLEE: WARNING: killing 23989 states (over memory cap)
KLEE: WARNING: killing 23776 states (over memory cap)
KLEE: WARNING: killing 23413 states (over memory cap)
KLEE: WARNING: killing 22858 states (over memory cap)
KLEE: WARNING: killing 24135 states (over memory cap)
KLEE: WARNING: killing 23587 states (over memory cap)
KLEE: WARNING: killing 23948 states (over memory cap)
KLEE: WARNING: killing 24881 states (over memory cap)
KLEE: WARNING: killing 24426 states (over memory cap)
KLEE: WARNING: killing 24789 states (over memory cap)
KLEE: WARNING: killing 23336 states (over memory cap)
KLEE: WARNING: killing 23793 states (over memory cap)
KLEE: WARNING: killing 23003 states (over memory cap)
KLEE: WARNING: killing 24367 states (over memory cap)
KLEE: WARNING: killing 23577 states (over memory cap)
KLEE: WARNING: killing 22975 states (over memory cap)
KLEE: WARNING: killing 23184 states (over memory cap)
KLEE: WARNING: killing 24260 states (over memory cap)
KLEE: WARNING: killing 23773 states (over memory cap)
KLEE: WARNING: killing 23891 states (over memory cap)
KLEE: WARNING: killing 23354 states (over memory cap)
KLEE: WARNING: killing 24422 states (over memory cap)
KLEE: WARNING: killing 24018 states (over memory cap)
KLEE: WARNING: killing 23765 states (over memory cap)
KLEE: WARNING: killing 23548 states (over memory cap)
KLEE: WARNING: killing 24102 states (over memory cap)
KLEE: WARNING: killing 22517 states (over memory cap)
KLEE: WARNING: killing 24955 states (over memory cap)
KLEE: WARNING: killing 23847 states (over memory cap)
KLEE: WARNING: killing 24385 states (over memory cap)
KLEE: WARNING: killing 24137 states (over memory cap)
KLEE: WARNING: killing 23874 states (over memory cap)
KLEE: WARNING: killing 23341 states (over memory cap)
KLEE: WARNING: killing 23555 states (over memory cap)
KLEE: WARNING: killing 23488 states (over memory cap)
KLEE: WARNING: killing 24129 states (over memory cap)
KLEE: WARNING: killing 23605 states (over memory cap)
KLEE: WARNING: killing 23909 states (over memory cap)
KLEE: WARNING: killing 22809 states (over memory cap)
KLEE: WARNING: killing 24981 states (over memory cap)
KLEE: WARNING: killing 23279 states (over memory cap)
KLEE: WARNING: killing 24620 states (over memory cap)
KLEE: WARNING: killing 24044 states (over memory cap)
KLEE: WARNING: killing 23925 states (over memory cap)
KLEE: WARNING: killing 24699 states (over memory cap)
KLEE: WARNING: killing 23274 states (over memory cap)
KLEE: WARNING: killing 22785 states (over memory cap)
KLEE: WARNING: killing 24115 states (over memory cap)
KLEE: WARNING: killing 24699 states (over memory cap)
KLEE: WARNING: killing 23699 states (over memory cap)
KLEE: WARNING: killing 23632 states (over memory cap)
KLEE: WARNING: killing 23940 states (over memory cap)
KLEE: WARNING: killing 23174 states (over memory cap)
KLEE: WARNING: killing 24363 states (over memory cap)
KLEE: WARNING: killing 23781 states (over memory cap)
KLEE: WARNING: killing 23718 states (over memory cap)
KLEE: WARNING: killing 24344 states (over memory cap)
KLEE: WARNING: killing 23768 states (over memory cap)
KLEE: WARNING: killing 24526 states (over memory cap)
KLEE: WARNING: killing 25297 states (over memory cap)
KLEE: WARNING: killing 21772 states (over memory cap)
KLEE: WARNING: killing 24426 states (over memory cap)
KLEE: WARNING: killing 24311 states (over memory cap)
KLEE: WARNING: killing 23915 states (over memory cap)
