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--target--iscsi--iscsi_target_mod.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.: 1576 1350 12900 90459
Removed infinite loop in iscsit_remove_cmd_from_connection_recovery
Removed infinite loop in iscsit_release_cmd
Removed infinite loop in sg_page___0
Removed infinite loop in iscsit_close_session
Removed infinite loop in sg_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 2.93567800522
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (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 'wait_for_completion' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function send_sig as symbolic
Defining function del_timer_sync as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'target_execute_cmd' (function is undefined)
Defining function printk as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function transport_handle_cdb_direct as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function percpu_ida_alloc as symbolic
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function kmemdup as symbolic
Defining function target_put_sess_cmd as symbolic
Defining function transport_generic_free_cmd as symbolic
Removed calls to 'percpu_ida_free' (function is undefined)
Defining function transport_check_aborted_status as symbolic
Defining function transport_send_check_condition_and_sense as symbolic
Defining function transport_generic_handle_tmr as symbolic
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'transport_init_se_cmd' (function is undefined)
Defining function target_get_sess_cmd as symbolic
Defining function scsilun_to_int as symbolic
Defining function transport_lookup_cmd_lun as symbolic
Defining function target_setup_cmd_from_cdb as symbolic
Defining function core_alua_check_nonop_delay as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Defining function transport_generic_new_cmd as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function mod_timer as symbolic
Removed calls to 'iov_iter_kvec' (function is undefined)
Defining function sock_recvmsg as symbolic
Defining function core_tmr_alloc_req as symbolic
Defining function transport_lookup_tmr_lun as symbolic
Defining function core_tpg_get_initiator_node_acl as symbolic
Defining function sprintf as symbolic
Removed calls to 'target_put_session' (function is undefined)
Removed calls to 'config_group_init_type_name' (function is undefined)
Removed calls to 'config_item_put' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function kthread_stop as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function snprintf as symbolic
Defining function strstr as symbolic
Defining function in6_pton as symbolic
Defining function in_aton as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'kernel_sigaction' (function is undefined)
Removed calls to 'flush_signals' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'idr_preload' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '_raw_write_lock_bh' (function is undefined)
Removed calls to '_raw_write_unlock_bh' (function is undefined)
Removed calls to '__transport_register_session' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to 'transport_free_session' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Removed calls to 'sock_release' (function is undefined)
Defining function strlcpy as symbolic
Removed calls to 'bitmap_release_region' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Defining function find_next_bit as symbolic
Defining function __bitmap_weight as symbolic
Defining function bitmap_find_free_region as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Defining function wait_for_completion_interruptible as symbolic
Removed calls to 'sg_init_one' (function is undefined)
Defining function kthread_should_stop as symbolic
Defining function transport_wait_for_tasks as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function sg_next as symbolic
Defining function wait_for_completion_interruptible_timeout as symbolic
Defining function set_cpus_allowed_ptr as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function simple_strtoul as symbolic
Removed calls to '_raw_read_lock_bh' (function is undefined)
Removed calls to '_raw_read_unlock_bh' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Defining function kstrdup as symbolic
Defining function kstrtoull as symbolic
Defining function crypto_alloc_base as symbolic
Defining function hex2bin as symbolic
Defining function strsep as symbolic
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function vsnprintf as symbolic
Defining function core_tpg_check_initiator_node_acl as symbolic
Defining function transport_alloc_session_tags as symbolic
Defining function down_interruptible as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function idr_alloc as symbolic
Defining function transport_init_session as symbolic
Defining function zalloc_cpumask_var as symbolic
Defining function try_module_get as symbolic
Defining function core_tpg_deregister as symbolic
Defining function kstrtou16 as symbolic
Defining function core_tpg_register as symbolic
Removed calls to 'msleep' (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 'int_to_scsilun' (function is undefined)
Defining function kernel_sendmsg as symbolic
Defining function kernel_accept as symbolic
Defining function sock_create as symbolic
Defining function kernel_setsockopt as symbolic
Defining function kernel_bind as symbolic
Defining function kernel_listen as symbolic
Defining function capable as symbolic
Defining function kstrtouint as symbolic
Defining function target_show_dynamic_sessions as symbolic
Defining function __request_module as symbolic
Defining function core_tpg_set_initiator_node_queue_depth as symbolic
Defining function core_tpg_set_initiator_node_tag as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'target_unregister_template' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Defining function target_register_template as symbolic
Defining function vzalloc as symbolic
Defining function kmem_cache_create as symbolic
Defining function ldv_release_62 as symbolic
Defining function ldv_probe_62 as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcmp
  strcpy
  strlen
  strncmp
  __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: 3.01645207405
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1687 1197 7997 53938
INFO: Starting verification
KLEE: WARNING ONCE: function "iscsit_add_cmd_to_response_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_add_cmd_to_immediate_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_remove_cmd_from_connection_recovery" has inline asm
KLEE: WARNING ONCE: function "__iscsit_free_cmd" has inline asm
KLEE: WARNING ONCE: function "iscsit_release_cmd" has inline asm
KLEE: WARNING ONCE: function "iscsit_setup_scsi_cmd" has inline asm
KLEE: WARNING ONCE: function "iscsit_check_dataout_hdr" has inline asm
KLEE: WARNING ONCE: function "iscsit_handle_nopin_response_timeout" has inline asm
KLEE: WARNING ONCE: function "iscsit_build_rsp_pdu" has inline asm
KLEE: WARNING ONCE: function "iscsit_logout_post_handler" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_login_thread" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_start_negotiation" has inline asm
KLEE: WARNING ONCE: function "iscsi_post_login_handler" has inline asm
KLEE: WARNING ONCE: function "iscsit_handle_time2retain_timeout" has inline asm
KLEE: WARNING ONCE: function "iscsit_thread_get_cpumask" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_tx_thread" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_rx_thread" has inline asm
KLEE: WARNING ONCE: function "sg_page___0" has inline asm
KLEE: WARNING ONCE: function "iscsit_close_connection" has inline asm
KLEE: WARNING ONCE: function "iscsit_free_queue_reqs_for_conn" has inline asm
KLEE: WARNING ONCE: function "iscsit_get_cmd_from_immediate_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_get_cmd_from_response_queue" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_do_login_rx" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_sk_data_ready" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_sk_state_change" has inline asm
KLEE: WARNING ONCE: function "iscsit_get_tpg_from_np" has inline asm
KLEE: WARNING ONCE: function "iscsit_add_tiqn" has inline asm
KLEE: WARNING ONCE: function "iscsit_close_session" has inline asm
KLEE: WARNING ONCE: function "iscsit_check_session_usage_count" has inline asm
KLEE: WARNING ONCE: function "iscsit_response_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_fe_sendpage_sg" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-yTArrT/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "iscsit_add_cmd_to_response_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_add_cmd_to_immediate_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_remove_cmd_from_connection_recovery" has inline asm
KLEE: WARNING ONCE: function "__iscsit_free_cmd" has inline asm
KLEE: WARNING ONCE: function "iscsit_release_cmd" has inline asm
KLEE: WARNING ONCE: function "iscsit_setup_scsi_cmd" has inline asm
KLEE: WARNING ONCE: function "iscsit_check_dataout_hdr" has inline asm
KLEE: WARNING ONCE: function "iscsit_handle_nopin_response_timeout" has inline asm
KLEE: WARNING ONCE: function "iscsit_build_rsp_pdu" has inline asm
KLEE: WARNING ONCE: function "iscsit_logout_post_handler" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_login_thread" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_start_negotiation" has inline asm
KLEE: WARNING ONCE: function "iscsi_post_login_handler" has inline asm
KLEE: WARNING ONCE: function "iscsit_handle_time2retain_timeout" has inline asm
KLEE: WARNING ONCE: function "iscsit_thread_get_cpumask" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_tx_thread" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_rx_thread" has inline asm
KLEE: WARNING ONCE: function "sg_page___0" has inline asm
KLEE: WARNING ONCE: function "iscsit_close_connection" has inline asm
KLEE: WARNING ONCE: function "iscsit_free_queue_reqs_for_conn" has inline asm
KLEE: WARNING ONCE: function "iscsit_get_cmd_from_immediate_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_get_cmd_from_response_queue" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_do_login_rx" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_sk_data_ready" has inline asm
KLEE: WARNING ONCE: function "iscsi_target_sk_state_change" has inline asm
KLEE: WARNING ONCE: function "iscsit_get_tpg_from_np" has inline asm
KLEE: WARNING ONCE: function "iscsit_add_tiqn" has inline asm
KLEE: WARNING ONCE: function "iscsit_close_session" has inline asm
KLEE: WARNING ONCE: function "iscsit_check_session_usage_count" has inline asm
KLEE: WARNING ONCE: function "iscsit_response_queue" has inline asm
KLEE: WARNING ONCE: function "iscsit_fe_sendpage_sg" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 6.82424402237
