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--bfa--bfa.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.: 489 2118 14895 146246
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 5.12581992149
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function snprintf as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to 'scsi_cmd_get_serial' (function is undefined)
Removed calls to 'scsi_dma_unmap' (function is undefined)
Removed calls to 'dev_printk' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'int_to_scsilun' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function scsi_change_queue_depth as symbolic
Defining function scsi_is_fc_rport as symbolic
Defining function scsilun_to_int as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function schedule_timeout as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function printk as symbolic
Defining function __scsi_iterate_devices as symbolic
Defining function scsi_track_queue_full as symbolic
Defining function sg_next as symbolic
Defining function scsi_dma_map as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'blk_queue_max_segments' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function sg_copy_to_buffer as symbolic
Defining function sg_copy_from_buffer as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to 'complete' (function is undefined)
Defining function queue_work_on as symbolic
Defining function sprintf as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function fc_vport_terminate as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'scsi_device_put' (function is undefined)
Defining function scsi_device_lookup as symbolic
Defining function wake_up_process as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'fc_remove_host' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'fc_remote_port_rolechg' (function is undefined)
Removed calls to 'fc_remote_port_delete' (function is undefined)
Defining function fc_remote_port_add as symbolic
Defining function idr_alloc as symbolic
Defining function scsi_add_host_with_dma as symbolic
Defining function scsi_host_alloc as symbolic
Defining function strncat as symbolic
Defining function scsi_is_host_device as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'bfad_debugfs_init' (function is undefined)
Removed calls to 'bfad_debugfs_exit' (function is undefined)
Defining function kthread_stop as symbolic
Removed calls to 'vfree' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Defining function pci_disable_pcie_error_reporting as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Defining function kthread_create_on_node as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Defining function mod_timer as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function pci_enable_msix_range as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function fc_vport_create as symbolic
Removed calls to 'fc_host_post_vendor_event' (function is undefined)
Defining function fc_get_event_number as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function strlcpy as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_enable_pcie_error_reporting as symbolic
Defining function pci_iomap as symbolic
Defining function pcie_get_readrq as symbolic
Defining function pcie_set_readrq as symbolic
Defining function pci_save_state as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_cleanup_aer_uncorrect_error_status as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function strstr as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_suspend_38 as symbolic
Defining function ldv_release_38 as symbolic
Defining function ldv_probe_38 as symbolic
Defining function ldv_shutdown_37 as symbolic
Defining function fixed_size_llseek as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to 'fc_release_transport' (function is undefined)
Defining function __pci_register_driver as symbolic
Defining function fc_attach_transport as symbolic
Defining function memdup_user as symbolic
Defining function sscanf as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  strncmp
  strncpy
  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: 5.6630961895
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 860 1871 10211 116400
INFO: Starting verification
KLEE: WARNING ONCE: function "bfad_im_abort_handler" has inline asm
KLEE: WARNING ONCE: function "bfa_ioim_send_abort" has inline asm
KLEE: WARNING ONCE: function "bfa_ioim_send_ioreq" has inline asm
KLEE: WARNING ONCE: function "bfa_itnim_send_fwcreate" has inline asm
KLEE: WARNING ONCE: function "bfa_itnim_send_fwdelete" has inline asm
KLEE: WARNING ONCE: function "bfa_fcxp_queue" has inline asm
KLEE: WARNING ONCE: function "bfa_fcport_send_disable" has inline asm
KLEE: WARNING ONCE: function "bfa_fcport_send_enable" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_fwcheck" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_fwcheck_entry" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_fwver_get" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_hw_sem_get" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_hwinit" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_hwinit_entry" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_semwait" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_disabling_sync" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_boot" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_pll_init" has inline asm
KLEE: WARNING ONCE: function "bfa_flash_raw_read" has inline asm
KLEE: WARNING ONCE: function "bfa_flash_sem_get" has inline asm
KLEE: WARNING ONCE: function "bfa_flash_fifo_flush" has inline asm
KLEE: WARNING ONCE: function "bfa_flash_status_read" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_sem_get" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_enabling" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_mbox_send" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_initfail_sync" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_smem_read" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_ready" has inline asm
KLEE: WARNING ONCE: function "bfa_iocpf_sm_fail_sync" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_sm_getattr" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_hb_check" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_mbox_poll" has inline asm
KLEE: WARNING ONCE: function "bfa_iocfc_israttr_set" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_fwsig_invalidate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_mbox_queue" has inline asm
KLEE: WARNING ONCE: function "bfa_fcport_send_stats_clear" has inline asm
KLEE: WARNING ONCE: function "bfa_iocfc_sm_disabling" has inline asm
KLEE: WARNING ONCE: function "bfa_iocfc_sm_failed_entry" has inline asm
KLEE: WARNING ONCE: function "bfa_iocfc_sm_stopping" has inline asm
KLEE: WARNING ONCE: function "bfa_iocfc_sm_init_failed_entry" has inline asm
KLEE: WARNING ONCE: function "bfa_fcport_send_stats_get" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_debug_fwcore" has inline asm
KLEE: WARNING ONCE: function "bfa_phy_read" has inline asm
KLEE: WARNING ONCE: function "bfa_phy_update" has inline asm
KLEE: WARNING ONCE: function "bfa_phy_get_stats" has inline asm
KLEE: WARNING ONCE: function "bfa_phy_get_attr" has inline asm
KLEE: WARNING ONCE: function "bfa_dport_send_req" has inline asm
KLEE: WARNING ONCE: function "bfa_fcdiag_queuetest_send" has inline asm
KLEE: WARNING ONCE: function "bfa_fcdiag_loopback" has inline asm
KLEE: WARNING ONCE: function "bfa_diag_memtest_done" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_fw_stats_clear" has inline asm
KLEE: WARNING ONCE: function "bfa_lps_send_login" has inline asm
KLEE: WARNING ONCE: function "bfa_lps_send_logout" has inline asm
KLEE: WARNING ONCE: function "bfa_lps_send_set_n2n_pid" has inline asm
KLEE: WARNING ONCE: function "bfa_rport_send_fwcreate" has inline asm
KLEE: WARNING ONCE: function "bfa_rport_sm_online" has inline asm
KLEE: WARNING ONCE: function "bfa_rport_send_fwdelete" has inline asm
KLEE: WARNING ONCE: function "bfa_tskim_send" has inline asm
KLEE: WARNING ONCE: function "bfa_cb_tskim_done" has inline asm
KLEE: WARNING ONCE: function "bfa_tskim_send_abort" has inline asm
KLEE: WARNING ONCE: function "bfa_uf_post_all" has inline asm
KLEE: WARNING ONCE: function "bfa_hwct_reqq_ack" has inline asm
KLEE: WARNING ONCE: function "bfa_hwct_rspq_ack" has inline asm
KLEE: WARNING ONCE: function "bfa_hwcb_rspq_ack" has inline asm
KLEE: WARNING ONCE: function "bfa_hwct2_rspq_ack" has inline asm
KLEE: WARNING ONCE: function "bfa_hwcb_reqq_ack_msix" has inline asm
KLEE: WARNING ONCE: function "bfa_hwcb_rspq_ack_msix" has inline asm
KLEE: WARNING ONCE: function "bfa_msix_all" has inline asm
KLEE: WARNING ONCE: function "bfa_msix_lpu_err" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_msgget" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_pll_init" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_firmware_lock" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_notify_fail" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_ownership_reset" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_sync_start" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_sync_join" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_sync_leave" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_sync_ack" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_sync_complete" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_set_cur_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_get_cur_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_set_alt_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_cb_get_alt_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_firmware_lock" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_firmware_unlock" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_notify_fail" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_ownership_reset" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_sync_start" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_sync_join" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_sync_leave" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_sync_ack" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_sync_complete" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_set_cur_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_get_cur_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_set_alt_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_get_alt_ioc_fwstate" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_pll_init" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_map_port" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct_isr_mode_set" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct2_pll_init" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct2_map_port" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct2_lpu_read_stat" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct2_poweron" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct2_clk_reset" has inline asm
KLEE: WARNING ONCE: function "bfa_isr_enable" has inline asm
KLEE: WARNING ONCE: function "bfa_intx" has inline asm
KLEE: WARNING ONCE: function "bfad_rport_online_wait" has inline asm
KLEE: WARNING ONCE: function "bfa_flash_sem_put" has inline asm
KLEE: WARNING ONCE: function "bfa_isr_disable" has inline asm
KLEE: WARNING ONCE: function "bfa_phy_busy" has inline asm
KLEE: WARNING ONCE: function "bfa_ioc_ct2_mac_reset" has inline asm
KLEE: WARNING ONCE: function "bfad_drv_uninit" has inline asm
KLEE: WARNING ONCE: function "bfad_debugfs_write_regwr" has inline asm
KLEE: WARNING ONCE: function "bfad_debugfs_write_regrd" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_98defe93-eac9-437b-acfa-bae6c9fdc8f9/symbiotic/lib/verifier/__VERIFIER_make_symbolic.c:8: wrong size given to klee_make_symbolic[_name]
KLEE: NOTE: now ignoring this error at this location
No error found.
RESULT: true
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_98defe93-eac9-437b-acfa-bae6c9fdc8f9/symbiotic/witness.graphml
INFO: Total time elapsed: 13.7444050312
