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-43_2a-drivers--scsi--fcoe--fcoe.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.: 144 241 1852 11865
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.504757165909
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 'module_put' (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
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 del_timer_sync as symbolic
Defining function scsi_host_alloc as symbolic
Defining function try_module_get 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 '_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 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)
Removed calls to 'ldv_check_final_state' (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
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  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.487550020218
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 295 193 988 6222
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_1842f334-94c6-46cb-9907-abdb25f19e5a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GTwigo/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--fcoe--fcoe.ko-entry_point_true-unreach-call.cil.out.c:12950: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15219 states (over memory cap)
KLEE: WARNING: killing 15019 states (over memory cap)
KLEE: WARNING: killing 14550 states (over memory cap)
KLEE: WARNING: killing 14569 states (over memory cap)
KLEE: WARNING: killing 14750 states (over memory cap)
KLEE: WARNING: killing 14456 states (over memory cap)
KLEE: WARNING: killing 15591 states (over memory cap)
KLEE: WARNING: killing 15143 states (over memory cap)
KLEE: WARNING: killing 14955 states (over memory cap)
KLEE: WARNING: killing 15828 states (over memory cap)
KLEE: WARNING: killing 16545 states (over memory cap)
KLEE: WARNING: killing 17102 states (over memory cap)
KLEE: WARNING: killing 15770 states (over memory cap)
KLEE: WARNING: killing 16535 states (over memory cap)
KLEE: WARNING: killing 15306 states (over memory cap)
KLEE: WARNING: killing 15756 states (over memory cap)
KLEE: WARNING: killing 15688 states (over memory cap)
KLEE: WARNING: killing 16029 states (over memory cap)
KLEE: WARNING: killing 15383 states (over memory cap)
KLEE: WARNING: killing 15414 states (over memory cap)
KLEE: WARNING: killing 14980 states (over memory cap)
KLEE: WARNING: killing 15689 states (over memory cap)
KLEE: WARNING: killing 14832 states (over memory cap)
KLEE: WARNING: killing 15697 states (over memory cap)
KLEE: WARNING: killing 15990 states (over memory cap)
KLEE: WARNING: killing 15865 states (over memory cap)
KLEE: WARNING: killing 16262 states (over memory cap)
KLEE: WARNING: killing 16296 states (over memory cap)
KLEE: WARNING: killing 15708 states (over memory cap)
KLEE: WARNING: killing 15533 states (over memory cap)
KLEE: WARNING: killing 16139 states (over memory cap)
KLEE: WARNING: killing 16020 states (over memory cap)
KLEE: WARNING: killing 15788 states (over memory cap)
KLEE: WARNING: killing 15415 states (over memory cap)
KLEE: WARNING: killing 15860 states (over memory cap)
KLEE: WARNING: killing 15834 states (over memory cap)
KLEE: WARNING: killing 16331 states (over memory cap)
KLEE: WARNING: killing 14985 states (over memory cap)
KLEE: WARNING: killing 16345 states (over memory cap)
KLEE: WARNING: killing 15408 states (over memory cap)
KLEE: WARNING: killing 15795 states (over memory cap)
KLEE: WARNING: killing 16645 states (over memory cap)
KLEE: WARNING: killing 15198 states (over memory cap)
KLEE: WARNING: killing 15742 states (over memory cap)
KLEE: WARNING: killing 15618 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 15889 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 15655 states (over memory cap)
KLEE: WARNING: killing 15380 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 15805 states (over memory cap)
KLEE: WARNING: killing 15638 states (over memory cap)
KLEE: WARNING: killing 16226 states (over memory cap)
KLEE: WARNING: killing 15653 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: WARNING: killing 16122 states (over memory cap)
KLEE: WARNING: killing 15405 states (over memory cap)
KLEE: WARNING: killing 15985 states (over memory cap)
KLEE: WARNING: killing 15575 states (over memory cap)
KLEE: WARNING: killing 15711 states (over memory cap)
KLEE: WARNING: killing 15844 states (over memory cap)
KLEE: WARNING: killing 15178 states (over memory cap)
KLEE: WARNING: killing 15360 states (over memory cap)
KLEE: WARNING: killing 15891 states (over memory cap)
KLEE: WARNING: killing 16025 states (over memory cap)
KLEE: WARNING: killing 15563 states (over memory cap)
KLEE: WARNING: killing 16447 states (over memory cap)
KLEE: WARNING: killing 16181 states (over memory cap)
KLEE: WARNING: killing 15273 states (over memory cap)
KLEE: WARNING: killing 16550 states (over memory cap)
KLEE: WARNING: killing 16091 states (over memory cap)
KLEE: WARNING: killing 15427 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15205 states (over memory cap)
KLEE: WARNING: killing 16073 states (over memory cap)
KLEE: WARNING: killing 15669 states (over memory cap)
KLEE: WARNING: killing 15402 states (over memory cap)
KLEE: WARNING: killing 16622 states (over memory cap)
KLEE: WARNING: killing 15975 states (over memory cap)
KLEE: WARNING: killing 15472 states (over memory cap)
KLEE: WARNING: killing 15944 states (over memory cap)
KLEE: WARNING: killing 15836 states (over memory cap)
KLEE: WARNING: killing 15872 states (over memory cap)
KLEE: WARNING: killing 15075 states (over memory cap)
KLEE: WARNING: killing 15005 states (over memory cap)
KLEE: WARNING: killing 15827 states (over memory cap)
KLEE: WARNING: killing 16101 states (over memory cap)
KLEE: WARNING: killing 15408 states (over memory cap)
KLEE: WARNING: killing 15933 states (over memory cap)
KLEE: WARNING: killing 15331 states (over memory cap)
KLEE: WARNING: killing 15467 states (over memory cap)
KLEE: WARNING: killing 15403 states (over memory cap)
KLEE: WARNING: killing 15730 states (over memory cap)
KLEE: WARNING: killing 16102 states (over memory cap)
KLEE: WARNING: killing 15902 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: WARNING: killing 15622 states (over memory cap)
KLEE: WARNING: killing 16047 states (over memory cap)
KLEE: WARNING: killing 14771 states (over memory cap)
KLEE: WARNING: killing 15972 states (over memory cap)
KLEE: WARNING: killing 16056 states (over memory cap)
KLEE: WARNING: killing 15653 states (over memory cap)
KLEE: WARNING: killing 15734 states (over memory cap)
KLEE: WARNING: killing 15192 states (over memory cap)
KLEE: WARNING: killing 15805 states (over memory cap)
KLEE: WARNING: killing 16327 states (over memory cap)
KLEE: WARNING: killing 15009 states (over memory cap)
KLEE: WARNING: killing 15817 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 15411 states (over memory cap)
KLEE: WARNING: killing 15349 states (over memory cap)
KLEE: WARNING: killing 15814 states (over memory cap)
KLEE: WARNING: killing 15752 states (over memory cap)
KLEE: WARNING: killing 15789 states (over memory cap)
KLEE: WARNING: killing 16069 states (over memory cap)
KLEE: WARNING: killing 15625 states (over memory cap)
KLEE: WARNING: killing 15895 states (over memory cap)
KLEE: WARNING: killing 16032 states (over memory cap)
KLEE: WARNING: killing 16108 states (over memory cap)
KLEE: WARNING: killing 14956 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 15495 states (over memory cap)
KLEE: WARNING: killing 15721 states (over memory cap)
KLEE: WARNING: killing 15706 states (over memory cap)
KLEE: WARNING: killing 15792 states (over memory cap)
KLEE: WARNING: killing 16013 states (over memory cap)
KLEE: WARNING: killing 15952 states (over memory cap)
KLEE: WARNING: killing 15752 states (over memory cap)
KLEE: WARNING: killing 15501 states (over memory cap)
KLEE: WARNING: killing 15632 states (over memory cap)
KLEE: WARNING: killing 15617 states (over memory cap)
KLEE: WARNING: killing 15462 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: WARNING: killing 15813 states (over memory cap)
KLEE: WARNING: killing 15896 states (over memory cap)
KLEE: WARNING: killing 16023 states (over memory cap)
KLEE: WARNING: killing 15684 states (over memory cap)
KLEE: WARNING: killing 15482 states (over memory cap)
KLEE: WARNING: killing 15702 states (over memory cap)
KLEE: WARNING: killing 15361 states (over memory cap)
KLEE: WARNING: killing 15395 states (over memory cap)
KLEE: WARNING: killing 16082 states (over memory cap)
KLEE: WARNING: killing 15177 states (over memory cap)
KLEE: WARNING: killing 15351 states (over memory cap)
KLEE: WARNING: killing 16457 states (over memory cap)
KLEE: WARNING: killing 16539 states (over memory cap)
KLEE: WARNING: killing 16203 states (over memory cap)
KLEE: WARNING: killing 15443 states (over memory cap)
KLEE: WARNING: killing 15430 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15255 states (over memory cap)
KLEE: WARNING: killing 16082 states (over memory cap)
KLEE: WARNING: killing 15927 states (over memory cap)
KLEE: WARNING: killing 16004 states (over memory cap)
KLEE: WARNING: killing 16455 states (over memory cap)
KLEE: WARNING: killing 15379 states (over memory cap)
KLEE: WARNING: killing 15785 states (over memory cap)
KLEE: WARNING: killing 16133 states (over memory cap)
KLEE: WARNING: killing 15573 states (over memory cap)
KLEE: WARNING: killing 15512 states (over memory cap)
KLEE: WARNING: killing 15776 states (over memory cap)
KLEE: WARNING: killing 15855 states (over memory cap)
KLEE: WARNING: killing 15796 states (over memory cap)
KLEE: WARNING: killing 15417 states (over memory cap)
