bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--infiniband--ulp--srp--ib_srp.ko_false-unreach-call.cil.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.: 274 741 3501 23642
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.942291021347
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Removed calls to 'ib_set_client_data' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Defining function ib_get_client_data as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function ib_dereg_mr as symbolic
Defining function ib_dealloc_pd as symbolic
Defining function queue_work_on as symbolic
Defining function ib_query_device as symbolic
Defining function printk as symbolic
Defining function ib_alloc_pd as symbolic
Defining function ib_get_dma_mr as symbolic
Defining function dev_set_name as symbolic
Defining function device_register as symbolic
Defining function device_create_file as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to 'dev_printk' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function __scsi_iterate_devices as symbolic
Removed calls to '__ldv_linux_kernel_locking_spinlock_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Defining function ib_fmr_pool_unmap as symbolic
Removed calls to 'ib_destroy_cm_id' (function is undefined)
Removed calls to 'ib_destroy_fmr_pool' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function wait_for_completion_interruptible as symbolic
Defining function ib_send_cm_req as symbolic
Defining function ib_sa_path_rec_get as symbolic
Defining function ib_create_cq as symbolic
Defining function ib_create_qp as symbolic
Removed calls to 'ib_free_fast_reg_page_list' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function ib_destroy_cq as symbolic
Defining function ib_destroy_qp as symbolic
Defining function ib_modify_qp as symbolic
Defining function ib_create_fmr_pool as symbolic
Defining function ib_alloc_fast_reg_mr as symbolic
Defining function ib_alloc_fast_reg_page_list as symbolic
Defining function ib_find_pkey as symbolic
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function blk_mq_tag_to_rq as symbolic
Defining function ib_create_cm_id as symbolic
Defining function ib_send_cm_drep as symbolic
Defining function ib_cm_init_qp_attr as symbolic
Defining function ib_send_cm_rtu as symbolic
Defining function msecs_to_jiffies 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 'debug_dma_mapping_error' (function is undefined)
Defining function __phys_addr as symbolic
Defining function ib_send_cm_dreq as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'scsi_scan_target' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Defining function scsi_host_get as symbolic
Removed calls to 'srp_start_tl_fail_timers' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'srp_rport_get' (function is undefined)
Removed calls to 'srp_remove_host' (function is undefined)
Removed calls to 'srp_stop_rport_timers' (function is undefined)
Removed calls to 'srp_rport_put' (function is undefined)
Defining function ib_query_gid as symbolic
Defining function __cpu_to_node as symbolic
Defining function sprintf as symbolic
Defining function srp_rport_add as symbolic
Removed calls to 'ldv_pre_probe' (function is undefined)
Defining function scsi_change_queue_depth as symbolic
Defining function blk_mq_unique_tag as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function srp_reconnect_rport as symbolic
Removed calls to 'debug_dma_map_sg' (function is undefined)
Defining function sg_next as symbolic
Defining function ib_fmr_pool_map_phys as symbolic
Removed calls to 'blk_queue_rq_timeout' (function is undefined)
Defining function scsi_add_host_with_dma as symbolic
Defining function __bitmap_weight as symbolic
Defining function cancel_work_sync as symbolic
Defining function blk_init_tags as symbolic
Defining function kstrdup as symbolic
Defining function match_token as symbolic
Defining function match_strdup as symbolic
Defining function simple_strtoull as symbolic
Defining function strlcpy as symbolic
Defining function sscanf as symbolic
Defining function match_hex as symbolic
Defining function match_int as symbolic
Defining function strsep as symbolic
Defining function scsi_host_alloc as symbolic
Removed calls to 'ib_unregister_client' (function is undefined)
Removed calls to 'ib_sa_unregister_client' (function is undefined)
Removed calls to 'class_unregister' (function is undefined)
Removed calls to 'srp_release_transport' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'ib_sa_register_client' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function srp_attach_transport as symbolic
Defining function ib_register_client as symbolic
Defining function kstrtoint as symbolic
Defining function srp_tmo_valid as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncmp
  __memcpy
  __memset
  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: 1.00331187248
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 405 662 2807 15077
INFO: Starting verification
KLEE: WARNING ONCE: function "srp_add_one" has inline asm
KLEE: WARNING ONCE: function "srp_unmap_data" has inline asm
KLEE: WARNING ONCE: function "srp_create_ch_ib" has inline asm
KLEE: WARNING ONCE: function "ib_dma_sync_single_for_cpu" has inline asm
KLEE: WARNING ONCE: function "ib_dma_sync_single_for_device" has inline asm
KLEE: WARNING ONCE: function "ib_dma_unmap_single" has inline asm
KLEE: WARNING ONCE: function "ib_dma_map_single" has inline asm
KLEE: WARNING ONCE: function "srp_queuecommand" has inline asm
KLEE: WARNING ONCE: function "srp_finish_mapping" has inline asm
KLEE: WARNING: undefined reference to variable: system_long_wq
KLEE: ERROR: unable to load symbol(system_long_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-3NaHDN/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "srp_add_one" has inline asm
KLEE: WARNING ONCE: function "srp_unmap_data" has inline asm
KLEE: WARNING ONCE: function "srp_create_ch_ib" has inline asm
KLEE: WARNING ONCE: function "ib_dma_sync_single_for_cpu" has inline asm
KLEE: WARNING ONCE: function "ib_dma_sync_single_for_device" has inline asm
KLEE: WARNING ONCE: function "ib_dma_unmap_single" has inline asm
KLEE: WARNING ONCE: function "ib_dma_map_single" has inline asm
KLEE: WARNING ONCE: function "srp_queuecommand" has inline asm
KLEE: WARNING ONCE: function "srp_finish_mapping" has inline asm
KLEE: WARNING: undefined reference to variable: system_long_wq
KLEE: ERROR: unable to load symbol(system_long_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 2.25981807709
