bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--scsi--qla2xxx--tcm_qla2xxx.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.: 169 183 1640 10516
Removed infinite loop in tcm_qla2xxx_free_session
Removed infinite loop in tcm_qla2xxx_put_sess
Removed infinite loop in tcm_qla2xxx_shutdown_sess
Removed infinite loop in tcm_qla2xxx_shutdown_session
Removed infinite loop in tcm_qla2xxx_close_session
Removed infinite loop in dma_unmap_sg_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.517265796661
Removed calls to 'qlt_unreg_sess' (function is undefined)
Defining function printk as symbolic
Defining function btree_update as symbolic
Defining function btree_insert as symbolic
Defining function btree_lookup as symbolic
Defining function btree_remove as symbolic
Defining function transport_init_session_tags as symbolic
Defining function snprintf as symbolic
Defining function core_tpg_check_initiator_node_acl as symbolic
Defining function queue_work_on as symbolic
Defining function transport_generic_free_cmd as symbolic
Defining function target_submit_tmr as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'transport_generic_request_failure' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function target_submit_cmd as symbolic
Removed calls to 'qlt_free_mcmd' (function is undefined)
Removed calls to 'qlt_free_cmd' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'target_sess_cmd_list_set_waiting' (function is undefined)
Removed calls to 'qlt_xmit_tm_rsp' (function is undefined)
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Removed calls to 'qlt_stop_phase2' (function is undefined)
Removed calls to 'qlt_lport_deregister' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'btree_destroy' (function is undefined)
Defining function core_tpg_del_initiator_node_acl as symbolic
Defining function qlt_stop_phase1 as symbolic
Defining function core_tpg_deregister as symbolic
Defining function kstrtoull as symbolic
Defining function btree_get_prev as symbolic
Defining function btree_last as symbolic
Defining function sprintf as symbolic
Defining function vmalloc as symbolic
Defining function qlt_xmit_response as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function qlt_rdy_to_xfer as symbolic
Defining function target_put_sess_cmd as symbolic
Defining function fc_parse_pr_out_transport_id as symbolic
Defining function fc_get_pr_transport_id_len as symbolic
Defining function fc_get_pr_transport_id as symbolic
Defining function fc_get_fabric_proto_ident as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'qlt_enable_vha' (function is undefined)
Removed calls to 'configfs_undepend_item' (function is undefined)
Defining function configfs_depend_item as symbolic
Removed calls to 'scsi_host_put' (function is undefined)
Defining function fc_vport_terminate as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'target_fabric_configfs_deregister' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Removed calls to 'target_wait_for_sess_cmds' (function is undefined)
Removed calls to 'transport_deregister_session_configfs' (function is undefined)
Removed calls to 'transport_deregister_session' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'transport_free_session' (function is undefined)
Removed calls to '__transport_register_session' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function ldv_release_2 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function target_fabric_configfs_init as symbolic
Defining function target_fabric_configfs_register as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function mempool_alloc as symbolic
Defining function ldv_some_page as symbolic
Defining function strncmp as symbolic
Linked our definitions to these undefined functions:
  strchr
  strlen
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.484345912933
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 255 166 782 5386
INFO: Starting verification
KLEE: WARNING ONCE: function "tcm_qla2xxx_shutdown_session" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_close_session" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_aborted_task" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_wwn_show_attr_version" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_handle_dif_work" has inline asm
KLEE: WARNING: undefined reference to variable: btree_geo32
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: Type for btree_geo32 is not sized
KLEE: WARNING: Unable to find size for global variable: btree_geo32 (use will result in out of bounds access)
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-0IfkFd/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "tcm_qla2xxx_shutdown_session" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_close_session" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_aborted_task" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_wwn_show_attr_version" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "tcm_qla2xxx_handle_dif_work" has inline asm
KLEE: WARNING: undefined reference to variable: btree_geo32
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: Type for btree_geo32 is not sized
KLEE: WARNING: Unable to find size for global variable: btree_geo32 (use will result in out of bounds access)
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 1.173787117
