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--scsi--qla4xxx--qla4xxx.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.: 1162 918 11586 74389
Removed infinite loop in qla4_82xx_wr_32
Removed infinite loop in qla4_82xx_rd_32
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in qla4_82xx_pci_is_same_window
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 2.43503499031
Removed calls to 'dev_printk' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function snprintf as symbolic
Defining function dma_alloc_attrs as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function skip_spaces as symbolic
Defining function printk as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function wait_for_completion_timeout as symbolic
Removed calls to '_raw_write_unlock_irqrestore' (function is undefined)
Defining function _raw_write_lock_irqsave as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'iscsi_session_teardown' (function is undefined)
Defining function iscsi_set_param as symbolic
Defining function iscsi_conn_send_pdu as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'iscsi_destroy_endpoint' (function is undefined)
Removed calls to 'iscsi_destroy_iface' (function is undefined)
Removed calls to 'dma_pool_free' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to 'iscsi_destroy_flashnode_sess' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function schedule_timeout_uninterruptible as symbolic
Defining function try_module_get as symbolic
Defining function dma_pool_alloc as symbolic
Defining function vzalloc as symbolic
Defining function strlcpy as symbolic
Defining function sprintf as symbolic
Defining function scsi_is_host_device as symbolic
Defining function strncasecmp as symbolic
Removed calls to 'module_put' (function is undefined)
Removed calls to 'iscsi_block_session' (function is undefined)
Defining function iscsi_session_setup as symbolic
Defining function iscsi_conn_setup as symbolic
Defining function iscsi_get_discovery_parent_name as symbolic
Defining function vmalloc as symbolic
Removed calls to 'iscsi_unblock_session' (function is undefined)
Defining function scsi_queue_work as symbolic
Defining function find_first_zero_bit as symbolic
Defining function iscsi_find_flashnode_sess as symbolic
Defining function iscsi_create_flashnode_sess as symbolic
Defining function iscsi_create_flashnode_conn as symbolic
Defining function iscsi_switch_str_param as symbolic
Defining function kmemdup as symbolic
Defining function iscsi_flashnode_bus_match as symbolic
Defining function iscsi_find_flashnode_conn as symbolic
Defining function device_for_each_child as symbolic
Defining function iscsi_is_session_dev as symbolic
Defining function iscsi_session_chkready as symbolic
Removed calls to 'bsg_job_done' (function is undefined)
Defining function sg_copy_from_buffer as symbolic
Defining function sg_copy_to_buffer as symbolic
Defining function iscsi_get_ipaddress_state_name as symbolic
Defining function iscsi_get_router_state_name as symbolic
Defining function iscsi_create_iface as symbolic
Defining function ___ratelimit as symbolic
Defining function iscsi_create_endpoint as symbolic
Defining function iscsi_complete_pdu as symbolic
Defining function __phys_addr as symbolic
Defining function sysfs_format_mac as symbolic
Defining function iscsi_get_port_state_name as symbolic
Defining function iscsi_get_port_speed_name as symbolic
Defining function iscsi_session_get_param as symbolic
Defining function iscsi_conn_get_addr_param as symbolic
Defining function iscsi_conn_get_param as symbolic
Defining function in6_pton as symbolic
Defining function in4_pton as symbolic
Defining function iscsi_conn_bind as symbolic
Defining function iscsi_lookup_endpoint as symbolic
Removed calls to 'iscsi_conn_login_event' (function is undefined)
Removed calls to 'iscsi_session_failure' (function is undefined)
Defining function iscsi_is_session_online as symbolic
Defining function iscsi_conn_start as symbolic
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function scsi_change_queue_depth as symbolic
Removed calls to 'scsi_block_requests' (function is undefined)
Removed calls to 'iscsi_host_for_each_session' (function is undefined)
Removed calls to 'scsi_unblock_requests' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function schedule_timeout as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Defining function blk_mq_tag_to_rq as symbolic
Removed calls to 'scsi_dma_unmap' (function is undefined)
Defining function iscsi_block_scsi_eh as symbolic
Removed calls to 'int_to_scsilun' (function is undefined)
Defining function scsi_dma_map as symbolic
Defining function sg_next as symbolic
Defining function mempool_alloc as symbolic
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_set_master' (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 '__const_udelay' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Defining function qla4_8xxx_need_reset as symbolic
Removed calls to '_dev_info' (function is undefined)
Defining function kobject_uevent_env as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function queue_work_on as symbolic
Defining function iscsi_itt_to_task as symbolic
Defining function pcie_capability_read_word as symbolic
Removed calls to 'iounmap' (function is undefined)
Defining function __printk_ratelimit as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to '___might_sleep' (function is undefined)
Defining function _cond_resched as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function pci_enable_msix_range as symbolic
Defining function pci_request_regions as symbolic
Removed calls to '__udelay' (function is undefined)
Defining function msleep_interruptible as symbolic
Defining function pci_set_mwi as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to 'sysfs_remove_bin_file' (function is undefined)
Removed calls to 'iscsi_destroy_all_flashnode' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function pci_disable_pcie_error_reporting as symbolic
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'dma_pool_destroy' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function pci_get_domain_bus_and_slot as symbolic
Defining function pci_enable_device as symbolic
Defining function iscsi_host_alloc as symbolic
Defining function pci_enable_pcie_error_reporting as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'iscsi_post_host_event' (function is undefined)
Removed calls to 'iscsi_ping_comp_event' (function is undefined)
Defining function pci_save_state as symbolic
Defining function sysfs_create_bin_file as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function mod_timer as symbolic
Defining function scsi_add_host_with_dma as symbolic
Defining function blk_init_tags as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Defining function dma_pool_create as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_cleanup_aer_uncorrect_error_status as symbolic
Defining function kstrtoll as symbolic
Defining function memory_read_from_buffer as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'iscsi_conn_stop' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function ldv_shutdown_21 as symbolic
Defining function ldv_probe_26 as symbolic
Defining function ldv_suspend_22 as symbolic
Defining function ldv_release_22 as symbolic
Defining function ldv_probe_22 as symbolic
Defining function ldv_release_20 as symbolic
Defining function ldv_probe_20 as symbolic
Defining function kmem_cache_create as symbolic
Defining function iscsi_register_transport as symbolic
Defining function iscsi_unregister_transport as symbolic
Defining function __pci_register_driver as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  strncmp
  strncpy
  __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: 2.83218407631
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 763 730 6563 49258
INFO: Starting verification
KLEE: WARNING ONCE: function "qla4xxx_mailbox_command" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_wr_32" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_wr_reg_indirect" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_rd_reg_indirect" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_set_win_base" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_crb_win_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_set_crbwindow_2M" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rd_32" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_session_create" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_session_destroy" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_sysfs_ddb_login" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_sysfs_ddb_logout_sid" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_session_logout_ddb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_get_ddb_index" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_sess_conn_setup" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_ping_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_vendor_specific" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_send_passthru0" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_ddb_change" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_eh_abort" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_eh_host_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_host_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_recover_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_mailbox_premature_completion" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_initialize_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_dead_adapter_cleanup" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_free_irqs" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_disable_msix" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_enable_mbox_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_alloc_fw_dump" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_build_ddb_list" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_ddb_changed" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_set_idc_dontreset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_send_marker_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_send_command_to_isp" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_disable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_enable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_load_risc" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_try_start_fw" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_interrupt_service_routine" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_isp_reset" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_complete_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rd_shdw_req_q_out" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rd_shdw_rsp_q_in" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_md_rd_32" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_md_wr_32" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_idc_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_queue_mbox_cmd" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_process_mbox_intr" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rom_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_device_state_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_update_idc_reg" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_need_reset_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_get_minidump" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_clear_idc_dontreset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_response_queue" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_isr_decode_mailbox" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_dump_registers" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_spurious_interrupt" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_mem_write_2M" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_is_same_window" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_mem_read_2M" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_flash_read_u32" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_flash_lock" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_init_rings" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_request_irqs" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_enable_msix" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_default_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_mailbox_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_disable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_enable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_start_firmware" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_interrupt_service_routine" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_isp_reset" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_queue_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_complete_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_rd_reg" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_wr_reg" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_drv_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_drv_unlock" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_rom_lock_recovery" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_queue_mbox_cmd" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_process_mbox_intr" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_can_perform_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_enable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_start_firmware" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_interrupt_service_routine" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_soft_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_hw_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_queue_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_complete_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_queue_mbox_cmd" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_mbox_intr" has inline asm
KLEE: WARNING ONCE: function "ql4xxx_sem_lock" has inline asm
KLEE: WARNING ONCE: function "__qla4xxx_disable_intrs" has inline asm
KLEE: WARNING ONCE: function "ql4xxx_sem_spinlock" has inline asm
KLEE: WARNING ONCE: function "rd_nvram_word" has inline asm
KLEE: WARNING ONCE: function "ql4xxx_sem_unlock" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_probe_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_remove_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_free_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_do_dpc" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_timer" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_watchdog" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_pci_error_detected" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_pci_slot_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_pci_resume" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_msix_rsp_q" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_sysfs_write_fw_dump" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_idc_dontreset" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: iscsi_conn_stop
KLEE: WARNING: undefined reference to function: mempool_free_slab
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_95c77270-29c4-4f55-b7d0-6e34e03596ef/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-WwD7ul/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--qla4xxx--qla4xxx.ko-entry_point_true-unreach-call.cil.out.c:23706: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15529 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 28584 states (over memory cap)
KLEE: WARNING: killing 26582 states (over memory cap)
KLEE: WARNING: killing 26478 states (over memory cap)
KLEE: WARNING: killing 27254 states (over memory cap)
KLEE: WARNING: killing 27321 states (over memory cap)
KLEE: WARNING: killing 29775 states (over memory cap)
KLEE: WARNING: killing 30868 states (over memory cap)
KLEE: WARNING: killing 30657 states (over memory cap)
KLEE: WARNING: killing 29618 states (over memory cap)
KLEE: WARNING: killing 28421 states (over memory cap)
KLEE: WARNING: killing 29577 states (over memory cap)
KLEE: WARNING: killing 27998 states (over memory cap)
KLEE: WARNING: killing 28566 states (over memory cap)
KLEE: WARNING: killing 29226 states (over memory cap)
KLEE: WARNING: killing 29766 states (over memory cap)
KLEE: WARNING: killing 29996 states (over memory cap)
KLEE: WARNING: killing 30175 states (over memory cap)
KLEE: WARNING: killing 28781 states (over memory cap)
KLEE: WARNING: killing 29969 states (over memory cap)
KLEE: WARNING: killing 29731 states (over memory cap)
KLEE: WARNING: killing 29815 states (over memory cap)
KLEE: WARNING: killing 29533 states (over memory cap)
KLEE: WARNING: killing 28079 states (over memory cap)
KLEE: WARNING: killing 29371 states (over memory cap)
KLEE: WARNING: killing 29626 states (over memory cap)
KLEE: WARNING: killing 30095 states (over memory cap)
KLEE: WARNING: killing 28605 states (over memory cap)
KLEE: WARNING: killing 29077 states (over memory cap)
KLEE: WARNING: killing 30327 states (over memory cap)
KLEE: WARNING: killing 29331 states (over memory cap)
KLEE: WARNING: killing 29516 states (over memory cap)
KLEE: WARNING: killing 30411 states (over memory cap)
KLEE: WARNING: killing 28721 states (over memory cap)
KLEE: WARNING: killing 31426 states (over memory cap)
KLEE: WARNING: killing 28634 states (over memory cap)
KLEE: WARNING: killing 29241 states (over memory cap)
KLEE: WARNING: killing 28188 states (over memory cap)
KLEE: WARNING: killing 28653 states (over memory cap)
KLEE: WARNING: killing 29855 states (over memory cap)
KLEE: WARNING: killing 30072 states (over memory cap)
KLEE: WARNING: killing 30291 states (over memory cap)
KLEE: WARNING: killing 29347 states (over memory cap)
KLEE: WARNING: killing 30102 states (over memory cap)
KLEE: WARNING: killing 29786 states (over memory cap)
KLEE: WARNING: killing 29234 states (over memory cap)
KLEE: WARNING: killing 28756 states (over memory cap)
KLEE: WARNING: killing 29251 states (over memory cap)
KLEE: WARNING: killing 30733 states (over memory cap)
KLEE: WARNING: killing 28467 states (over memory cap)
KLEE: WARNING: killing 27744 states (over memory cap)
KLEE: WARNING: killing 29490 states (over memory cap)
KLEE: WARNING: killing 31317 states (over memory cap)
KLEE: WARNING: killing 29995 states (over memory cap)
KLEE: WARNING: killing 29489 states (over memory cap)
KLEE: WARNING: killing 29460 states (over memory cap)
KLEE: WARNING: killing 30029 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
KLEE: output directory is "/tmp/symbiotic-WwD7ul/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "qla4xxx_mailbox_command" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_wr_32" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_wr_reg_indirect" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_rd_reg_indirect" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_set_win_base" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_crb_win_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_set_crbwindow_2M" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rd_32" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_session_create" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_session_destroy" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_sysfs_ddb_login" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_sysfs_ddb_logout_sid" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_session_logout_ddb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_get_ddb_index" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_sess_conn_setup" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_ping_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_vendor_specific" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_send_passthru0" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_ddb_change" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_eh_abort" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_eh_host_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_host_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_recover_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_mailbox_premature_completion" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_initialize_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_dead_adapter_cleanup" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_free_irqs" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_disable_msix" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_enable_mbox_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_alloc_fw_dump" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_build_ddb_list" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_ddb_changed" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_set_idc_dontreset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_send_marker_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_send_command_to_isp" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_disable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_enable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_load_risc" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_try_start_fw" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_interrupt_service_routine" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_isp_reset" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_complete_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rd_shdw_req_q_out" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rd_shdw_rsp_q_in" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_md_rd_32" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_md_wr_32" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_idc_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_queue_mbox_cmd" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_process_mbox_intr" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_rom_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_device_state_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_update_idc_reg" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_need_reset_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_get_minidump" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_clear_idc_dontreset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_response_queue" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_isr_decode_mailbox" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_dump_registers" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_spurious_interrupt" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_mem_write_2M" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_is_same_window" has inline asm
KLEE: WARNING ONCE: function "qla4_82xx_pci_mem_read_2M" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_flash_read_u32" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_flash_lock" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_init_rings" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_request_irqs" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_enable_msix" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_default_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_mailbox_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_disable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_enable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_start_firmware" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_interrupt_service_routine" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_isp_reset" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_queue_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_complete_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_rd_reg" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_wr_reg" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_drv_lock" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_drv_unlock" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_rom_lock_recovery" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_queue_mbox_cmd" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_process_mbox_intr" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_can_perform_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_enable_intrs" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_start_firmware" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_intr_handler" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_interrupt_service_routine" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_soft_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_hw_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_queue_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_complete_iocb" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_queue_mbox_cmd" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_process_mbox_intr" has inline asm
KLEE: WARNING ONCE: function "ql4xxx_sem_lock" has inline asm
KLEE: WARNING ONCE: function "__qla4xxx_disable_intrs" has inline asm
KLEE: WARNING ONCE: function "ql4xxx_sem_spinlock" has inline asm
KLEE: WARNING ONCE: function "rd_nvram_word" has inline asm
KLEE: WARNING ONCE: function "ql4xxx_sem_unlock" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_probe_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_remove_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_free_adapter" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_do_dpc" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_timer" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_watchdog" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_pci_error_detected" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_pci_slot_reset" has inline asm
KLEE: WARNING ONCE: function "qla4xxx_pci_resume" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_msix_rsp_q" has inline asm
KLEE: WARNING ONCE: function "qla4_8xxx_sysfs_write_fw_dump" has inline asm
KLEE: WARNING ONCE: function "qla4_83xx_idc_dontreset" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: iscsi_conn_stop
KLEE: WARNING: undefined reference to function: mempool_free_slab
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_95c77270-29c4-4f55-b7d0-6e34e03596ef/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-WwD7ul/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--qla4xxx--qla4xxx.ko-entry_point_true-unreach-call.cil.out.c:23706: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15529 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 28584 states (over memory cap)
KLEE: WARNING: killing 26582 states (over memory cap)
KLEE: WARNING: killing 26478 states (over memory cap)
KLEE: WARNING: killing 27254 states (over memory cap)
KLEE: WARNING: killing 27321 states (over memory cap)
KLEE: WARNING: killing 29775 states (over memory cap)
KLEE: WARNING: killing 30868 states (over memory cap)
KLEE: WARNING: killing 30657 states (over memory cap)
KLEE: WARNING: killing 29618 states (over memory cap)
KLEE: WARNING: killing 28421 states (over memory cap)
KLEE: WARNING: killing 29577 states (over memory cap)
KLEE: WARNING: killing 27998 states (over memory cap)
KLEE: WARNING: killing 28566 states (over memory cap)
KLEE: WARNING: killing 29226 states (over memory cap)
KLEE: WARNING: killing 29766 states (over memory cap)
KLEE: WARNING: killing 29996 states (over memory cap)
KLEE: WARNING: killing 30175 states (over memory cap)
KLEE: WARNING: killing 28781 states (over memory cap)
KLEE: WARNING: killing 29969 states (over memory cap)
KLEE: WARNING: killing 29731 states (over memory cap)
KLEE: WARNING: killing 29815 states (over memory cap)
KLEE: WARNING: killing 29533 states (over memory cap)
KLEE: WARNING: killing 28079 states (over memory cap)
KLEE: WARNING: killing 29371 states (over memory cap)
KLEE: WARNING: killing 29626 states (over memory cap)
KLEE: WARNING: killing 30095 states (over memory cap)
KLEE: WARNING: killing 28605 states (over memory cap)
KLEE: WARNING: killing 29077 states (over memory cap)
KLEE: WARNING: killing 30327 states (over memory cap)
KLEE: WARNING: killing 29331 states (over memory cap)
KLEE: WARNING: killing 29516 states (over memory cap)
KLEE: WARNING: killing 30411 states (over memory cap)
KLEE: WARNING: killing 28721 states (over memory cap)
KLEE: WARNING: killing 31426 states (over memory cap)
KLEE: WARNING: killing 28634 states (over memory cap)
KLEE: WARNING: killing 29241 states (over memory cap)
KLEE: WARNING: killing 28188 states (over memory cap)
KLEE: WARNING: killing 28653 states (over memory cap)
KLEE: WARNING: killing 29855 states (over memory cap)
KLEE: WARNING: killing 30072 states (over memory cap)
KLEE: WARNING: killing 30291 states (over memory cap)
KLEE: WARNING: killing 29347 states (over memory cap)
KLEE: WARNING: killing 30102 states (over memory cap)
KLEE: WARNING: killing 29786 states (over memory cap)
KLEE: WARNING: killing 29234 states (over memory cap)
KLEE: WARNING: killing 28756 states (over memory cap)
KLEE: WARNING: killing 29251 states (over memory cap)
KLEE: WARNING: killing 30733 states (over memory cap)
KLEE: WARNING: killing 28467 states (over memory cap)
KLEE: WARNING: killing 27744 states (over memory cap)
KLEE: WARNING: killing 29490 states (over memory cap)
KLEE: WARNING: killing 31317 states (over memory cap)
KLEE: WARNING: killing 29995 states (over memory cap)
KLEE: WARNING: killing 29489 states (over memory cap)
KLEE: WARNING: killing 29460 states (over memory cap)
KLEE: WARNING: killing 30029 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007fc59cb31390
4  libc.so.6       0x00007fc59beea428 gsignal + 56
5  libc.so.6       0x00007fc59beec02a abort + 362
6  libc.so.6       0x00007fc59bee2bd7
7  libc.so.6       0x00007fc59bee2c82
8  klee            0x000000000061be59 klee::DiscretePDF<klee::ExecutionState*>::remove(klee::ExecutionState*) + 73
9  klee            0x00000000006195f1 klee::WeightedRandomSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 241
10 klee            0x0000000000617416 klee::InterleavedSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 54
11 klee            0x00000000005cecfe klee::Executor::updateStates(klee::ExecutionState*) + 46
12 klee            0x00000000005da8eb klee::Executor::run(klee::ExecutionState&) + 2155
13 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
14 klee            0x0000000000593c63 main + 8867
15 libc.so.6       0x00007fc59bed5830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 340.016283989
