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-08_1a-drivers--scsi--fcoe--fcoe.ko-entry_point_false-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.: 144 232 1858 11771
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.502315998077
Defining function fc_queuecommand as symbolic
Defining function fc_eh_abort as symbolic
Defining function fc_eh_device_reset as symbolic
Defining function fc_eh_host_reset as symbolic
Defining function fc_slave_alloc as symbolic
Defining function scsi_change_queue_depth as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Defining function fcoe_ctlr_recv_flogi as symbolic
Removed calls to 'fc_lport_flogi_resp' (function is undefined)
Defining function fc_elsct_send as symbolic
Removed calls to 'fc_lport_logo_resp' (function is undefined)
Defining function dev_uc_del as symbolic
Defining function dev_uc_add as symbolic
Defining function fcoe_ctlr_els_send as symbolic
Defining function fcoe_fc_crc as symbolic
Defining function skb_put as symbolic
Defining function skb_push as symbolic
Defining function vlan_dev_vlan_id as symbolic
Removed calls to 'fcoe_check_wait_queue' (function is undefined)
Defining function fcoe_start_io as symbolic
Defining function fcoe_get_paged_crc_eof as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'fcoe_ctlr_link_up' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'fcoe_clean_pending_queue' (function is undefined)
Defining function fcoe_ctlr_link_down as symbolic
Defining function dev_get_by_index as symbolic
Defining function vlan_dev_real_dev as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function fc_set_mfs as symbolic
Defining function printk as symbolic
Defining function fcoe_link_speed_update as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'kthread_bind' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function kthread_stop as symbolic
Defining function __cpu_to_node as symbolic
Removed calls to 'set_user_nice' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'fc_exch_recv' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function kthread_should_stop as symbolic
Removed calls to 'complete' (function is undefined)
Defining function skb_pull as symbolic
Defining function skb_copy_bits as symbolic
Defining function crc32_le as symbolic
Defining function ___pskb_trim as symbolic
Defining function __pskb_pull_tail as symbolic
Removed calls to 'fcoe_ctlr_init' (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 'dev_add_pack' (function is undefined)
Removed calls to 'fcoe_ctlr_destroy' (function is undefined)
Removed calls to 'fcoe_ctlr_device_delete' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'fc_exch_mgr_free' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Defining function fc_fabric_login as symbolic
Defining function dcb_ieee_getapp_mask as symbolic
Defining function dcb_getapp as symbolic
Removed calls to '__dev_remove_pack' (function is undefined)
Removed calls to 'synchronize_net' (function is undefined)
Defining function dev_mc_del as symbolic
Defining function libfc_vport_create as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function fcoe_libfc_config as symbolic
Defining function fc_exch_mgr_list_clone as symbolic
Defining function fc_exch_mgr_add as symbolic
Defining function fc_exch_mgr_alloc as symbolic
Defining function snprintf as symbolic
Defining function scsi_add_host_with_dma as symbolic
Defining function fcoe_get_wwn as symbolic
Defining function fcoe_wwn_from_mac as symbolic
Defining function fc_lport_config as symbolic
Defining function __alloc_percpu as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'fc_remove_host' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'fc_fcp_destroy' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Defining function fc_fabric_logoff as symbolic
Defining function fc_lport_destroy as symbolic
Defining function find_next_bit as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function del_timer_sync as symbolic
Defining function scsi_host_alloc as symbolic
Defining function fcoe_ctlr_device_add as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function dev_mc_add as symbolic
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'fcoe_ctlr_recv' (function is undefined)
Defining function find_first_bit as symbolic
Defining function skb_clone as symbolic
Defining function rcu_is_watching as symbolic
Defining function fc_get_host_stats as symbolic
Removed calls to 'fcoe_wwn_to_str' (function is undefined)
Removed calls to 'fc_vport_setlink' (function is undefined)
Defining function fc_lport_bsg_request as symbolic
Defining function fcoe_validate_vport_create as symbolic
Defining function strnlen as symbolic
Defining function fc_frame_alloc_fill as symbolic
Defining function _fc_frame_alloc as symbolic
Removed calls to 'fcoe_queue_timer' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'fc_get_host_speed' (function is undefined)
Removed calls to 'fc_set_rport_loss_tmo' (function is undefined)
Removed calls to 'fc_rport_terminate_io' (function is undefined)
Removed calls to 'fc_get_host_port_state' (function is undefined)
Removed calls to 'fcoe_get_lesb' (function is undefined)
Removed calls to 'fcoe_ctlr_get_lesb' (function is undefined)
Removed calls to 'fcoe_ctlr_set_fip_mode' (function is undefined)
Removed calls to 'fcoe_fcf_get_selected' (function is undefined)
Removed calls to 'cpu_maps_update_begin' (function is undefined)
Removed calls to '__unregister_cpu_notifier' (function is undefined)
Removed calls to 'cpu_maps_update_done' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'fc_release_transport' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function fcoe_transport_attach as symbolic
Defining function __register_cpu_notifier as symbolic
Defining function fc_attach_transport as symbolic
Defining function register_dcbevent_notifier as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function fcoe_transport_detach as symbolic
Defining function unregister_dcbevent_notifier as symbolic
Defining function unregister_netdevice_notifier as symbolic
Defining function queue_delayed_work_on as symbolic
Linked our definitions to these undefined functions:
  __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: 0.475749015808
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 295 188 984 6114
INFO: Starting verification
KLEE: WARNING ONCE: function "fcoe_xmit" has inline asm
KLEE: WARNING ONCE: function "fcoe_dcb_app_notification" has inline asm
KLEE: WARNING ONCE: function "fcoe_device_notification" has inline asm
KLEE: WARNING ONCE: function "fcoe_percpu_thread_create" has inline asm
KLEE: WARNING ONCE: function "fcoe_percpu_thread_destroy" has inline asm
KLEE: WARNING ONCE: function "fcoe_percpu_receive_thread" has inline asm
KLEE: WARNING ONCE: function "_fcoe_create" has inline asm
KLEE: WARNING ONCE: function "fcoe_rcv" has inline asm
KLEE: WARNING ONCE: function "fcoe_interface_cleanup" has inline asm
KLEE: WARNING ONCE: function "fcoe_if_destroy" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: fc_get_host_port_state
KLEE: WARNING: undefined reference to function: fc_get_host_speed
KLEE: WARNING: undefined reference to function: fc_rport_terminate_io
KLEE: WARNING: undefined reference to function: fc_set_rport_loss_tmo
KLEE: WARNING: undefined reference to function: fcoe_ctlr_get_lesb
KLEE: WARNING: undefined reference to function: fcoe_ctlr_set_fip_mode
KLEE: WARNING: undefined reference to function: fcoe_fcf_get_selected
KLEE: WARNING: undefined reference to function: fcoe_get_lesb
KLEE: WARNING: undefined reference to function: fcoe_queue_timer
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_a0569e10-0dce-4389-9045-94480bd49d2f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-sUGl_h/linux-4.2-rc1.tar.xz-08_1a-drivers--scsi--fcoe--fcoe.ko-entry_point_false-unreach-call.cil.out.c:13001: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16047 states (over memory cap)
KLEE: WARNING: killing 14777 states (over memory cap)
KLEE: WARNING: killing 14420 states (over memory cap)
KLEE: WARNING: killing 14550 states (over memory cap)
KLEE: WARNING: killing 14992 states (over memory cap)
KLEE: WARNING: killing 14433 states (over memory cap)
KLEE: WARNING: killing 14876 states (over memory cap)
KLEE: WARNING: killing 15110 states (over memory cap)
KLEE: WARNING: killing 14557 states (over memory cap)
KLEE: WARNING: killing 14957 states (over memory cap)
KLEE: WARNING: killing 16148 states (over memory cap)
KLEE: WARNING: killing 16174 states (over memory cap)
KLEE: WARNING: killing 16422 states (over memory cap)
KLEE: WARNING: killing 16081 states (over memory cap)
KLEE: WARNING: killing 16698 states (over memory cap)
KLEE: WARNING: killing 16937 states (over memory cap)
KLEE: WARNING: killing 15350 states (over memory cap)
KLEE: WARNING: killing 15844 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 15704 states (over memory cap)
KLEE: WARNING: killing 15370 states (over memory cap)
KLEE: WARNING: killing 15138 states (over memory cap)
KLEE: WARNING: killing 15484 states (over memory cap)
KLEE: WARNING: killing 15827 states (over memory cap)
KLEE: WARNING: killing 15295 states (over memory cap)
KLEE: WARNING: killing 15739 states (over memory cap)
KLEE: WARNING: killing 15876 states (over memory cap)
KLEE: WARNING: killing 16118 states (over memory cap)
KLEE: WARNING: killing 16355 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 15387 states (over memory cap)
KLEE: WARNING: killing 14904 states (over memory cap)
KLEE: WARNING: killing 15910 states (over memory cap)
KLEE: WARNING: killing 15841 states (over memory cap)
KLEE: WARNING: killing 15413 states (over memory cap)
KLEE: WARNING: killing 16416 states (over memory cap)
KLEE: WARNING: killing 16149 states (over memory cap)
KLEE: WARNING: killing 15819 states (over memory cap)
KLEE: WARNING: killing 15653 states (over memory cap)
KLEE: WARNING: killing 15787 states (over memory cap)
KLEE: WARNING: killing 16232 states (over memory cap)
KLEE: WARNING: killing 16263 states (over memory cap)
KLEE: WARNING: killing 15279 states (over memory cap)
KLEE: WARNING: killing 15466 states (over memory cap)
KLEE: WARNING: killing 15189 states (over memory cap)
KLEE: WARNING: killing 15989 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 15793 states (over memory cap)
KLEE: WARNING: killing 15935 states (over memory cap)
KLEE: WARNING: killing 16114 states (over memory cap)
KLEE: WARNING: killing 14939 states (over memory cap)
KLEE: WARNING: killing 15976 states (over memory cap)
KLEE: WARNING: killing 15917 states (over memory cap)
KLEE: WARNING: killing 14995 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 15917 states (over memory cap)
KLEE: WARNING: killing 15999 states (over memory cap)
KLEE: WARNING: killing 15886 states (over memory cap)
KLEE: WARNING: killing 16220 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 15891 states (over memory cap)
KLEE: WARNING: killing 15327 states (over memory cap)
KLEE: WARNING: killing 15910 states (over memory cap)
KLEE: WARNING: killing 15791 states (over memory cap)
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 16262 states (over memory cap)
KLEE: WARNING: killing 15451 states (over memory cap)
KLEE: WARNING: killing 15828 states (over memory cap)
KLEE: WARNING: killing 14224 states (over memory cap)
KLEE: WARNING: killing 16295 states (over memory cap)
KLEE: WARNING: killing 15688 states (over memory cap)
KLEE: WARNING: killing 15815 states (over memory cap)
KLEE: WARNING: killing 16543 states (over memory cap)
KLEE: WARNING: killing 15888 states (over memory cap)
KLEE: WARNING: killing 15875 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 15340 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15459 states (over memory cap)
KLEE: WARNING: killing 15785 states (over memory cap)
KLEE: WARNING: killing 16315 states (over memory cap)
KLEE: WARNING: killing 15856 states (over memory cap)
KLEE: WARNING: killing 15841 states (over memory cap)
KLEE: WARNING: killing 15588 states (over memory cap)
KLEE: WARNING: killing 15572 states (over memory cap)
KLEE: WARNING: killing 16050 states (over memory cap)
KLEE: WARNING: killing 16133 states (over memory cap)
KLEE: WARNING: killing 15444 states (over memory cap)
KLEE: WARNING: killing 15715 states (over memory cap)
KLEE: WARNING: killing 14974 states (over memory cap)
KLEE: WARNING: killing 15837 states (over memory cap)
KLEE: WARNING: killing 15239 states (over memory cap)
KLEE: WARNING: killing 16050 states (over memory cap)
KLEE: WARNING: killing 15305 states (over memory cap)
KLEE: WARNING: killing 15686 states (over memory cap)
KLEE: WARNING: killing 15670 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 15698 states (over memory cap)
KLEE: WARNING: killing 15103 states (over memory cap)
KLEE: WARNING: killing 16148 states (over memory cap)
KLEE: WARNING: killing 16238 states (over memory cap)
KLEE: WARNING: killing 15982 states (over memory cap)
KLEE: WARNING: killing 16067 states (over memory cap)
KLEE: WARNING: killing 15813 states (over memory cap)
KLEE: WARNING: killing 15419 states (over memory cap)
KLEE: WARNING: killing 15735 states (over memory cap)
KLEE: WARNING: killing 16206 states (over memory cap)
KLEE: WARNING: killing 15810 states (over memory cap)
KLEE: WARNING: killing 15505 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 15438 states (over memory cap)
KLEE: WARNING: killing 15808 states (over memory cap)
KLEE: WARNING: killing 15363 states (over memory cap)
KLEE: WARNING: killing 14969 states (over memory cap)
KLEE: WARNING: killing 15857 states (over memory cap)
KLEE: WARNING: killing 15513 states (over memory cap)
KLEE: WARNING: killing 15450 states (over memory cap)
KLEE: WARNING: killing 15726 states (over memory cap)
KLEE: WARNING: killing 16234 states (over memory cap)
KLEE: WARNING: killing 16078 states (over memory cap)
KLEE: WARNING: killing 16113 states (over memory cap)
KLEE: WARNING: killing 15249 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 15507 states (over memory cap)
KLEE: WARNING: killing 15728 states (over memory cap)
KLEE: WARNING: killing 16329 states (over memory cap)
KLEE: WARNING: killing 15466 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 15529 states (over memory cap)
KLEE: WARNING: killing 15237 states (over memory cap)
KLEE: WARNING: killing 16116 states (over memory cap)
KLEE: WARNING: killing 15585 states (over memory cap)
KLEE: WARNING: killing 15570 states (over memory cap)
KLEE: WARNING: killing 15840 states (over memory cap)
KLEE: WARNING: killing 16349 states (over memory cap)
KLEE: WARNING: killing 16429 states (over memory cap)
KLEE: WARNING: killing 15286 states (over memory cap)
KLEE: WARNING: killing 16492 states (over memory cap)
KLEE: WARNING: killing 15778 states (over memory cap)
KLEE: WARNING: killing 15577 states (over memory cap)
KLEE: WARNING: killing 15604 states (over memory cap)
KLEE: WARNING: killing 16061 states (over memory cap)
KLEE: WARNING: killing 15626 states (over memory cap)
KLEE: WARNING: killing 15381 states (over memory cap)
KLEE: WARNING: killing 15272 states (over memory cap)
KLEE: WARNING: killing 15024 states (over memory cap)
KLEE: WARNING: killing 16029 states (over memory cap)
KLEE: WARNING: killing 16156 states (over memory cap)
KLEE: WARNING: killing 16189 states (over memory cap)
KLEE: WARNING: killing 16084 states (over memory cap)
KLEE: WARNING: killing 15891 states (over memory cap)
KLEE: WARNING: killing 15600 states (over memory cap)
KLEE: WARNING: killing 15722 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15834 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15663 states (over memory cap)
KLEE: WARNING: killing 15747 states (over memory cap)
KLEE: WARNING: killing 15874 states (over memory cap)
KLEE: WARNING: killing 15309 states (over memory cap)
KLEE: WARNING: killing 15338 states (over memory cap)
KLEE: WARNING: killing 15693 states (over memory cap)
KLEE: WARNING: killing 15223 states (over memory cap)
KLEE: WARNING: killing 15849 states (over memory cap)
KLEE: WARNING: killing 16202 states (over memory cap)
KLEE: WARNING: killing 16427 states (over memory cap)
