bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.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.: 538 383 7386 105851
INFO: Compilation, preparation and instrumentation time: 3.32319188118
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function skb_put as symbolic
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Defining function printk as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function schedule_delayed_work as symbolic
Removed calls to 'skb_trim' (function is undefined)
Defining function __alloc_skb as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function queue_delayed_work as symbolic
Defining function find_next_bit as symbolic
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function __alloc_percpu as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mempool_alloc as symbolic
Defining function strnlen as symbolic
Defining function snprintf as symbolic
Defining function crc32_le as symbolic
Removed calls to 'jiffies_to_timespec' (function is undefined)
Removed calls to 'fc_host_post_event' (function is undefined)
Defining function fc_get_event_number as symbolic
Defining function blocking_notifier_call_chain as symbolic
Removed calls to 'module_put' (function is undefined)
Defining function try_module_get as symbolic
Defining function sg_copy_to_buffer as symbolic
Defining function sg_next as symbolic
Removed calls to 'kfree_call_rcu' (function is undefined)
Defining function queue_work as symbolic
Removed calls to 'fc_remote_port_delete' (function is undefined)
Defining function fc_remote_port_add as symbolic
Removed calls to 'int_to_scsilun' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function scsi_is_fc_rport as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'complete' (function is undefined)
Defining function dev_printk as symbolic
Defining function mod_timer as symbolic
Defining function __get_page_tail as symbolic
Defining function fc_block_scsi_eh as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function wait_for_completion_timeout as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'scsi_adjust_queue_depth' (function is undefined)
Defining function blk_queue_init_tags as symbolic
Defining function scsi_track_queue_full as symbolic
Removed calls to 'blk_queue_free_tags' (function is undefined)
Defining function jiffies_to_msecs as symbolic
Defining function scsi_host_alloc as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function kmem_cache_create as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Linked our definitions to these undefined functions:
  strlen
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 2.07938098907
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 950 266 3435 42338
INFO: Starting verification
KLEE: WARNING ONCE: function "fc_fc4_deregister_provider" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "fc_exch_mgr_reset" has inline asm
KLEE: WARNING ONCE: function "fc_exch_done_locked" has inline asm
KLEE: WARNING ONCE: function "fc_exch_release" has inline asm
KLEE: WARNING ONCE: function "fc_exch_timer_set_locked" has inline asm
KLEE: WARNING ONCE: function "fc_exch_mgr_del" has inline asm
KLEE: WARNING ONCE: function "fc_exch_mgr_alloc" has inline asm
KLEE: WARNING ONCE: function "fc_exch_recv" has inline asm
KLEE: WARNING ONCE: function "fc_exch_find" has inline asm
KLEE: WARNING ONCE: function "fc_seq_lookup_recip" has inline asm
KLEE: WARNING ONCE: function "fc_exch_em_alloc" has inline asm
KLEE: WARNING ONCE: function "fc_seq_els_rsp_send" has inline asm
KLEE: WARNING ONCE: function "fc_get_host_stats" has inline asm
KLEE: WARNING ONCE: function "fc_fc4_conf_lport_params" has inline asm
KLEE: WARNING ONCE: function "fc_lport_recv_req" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "kmap_atomic" has inline asm
KLEE: WARNING ONCE: function "__kunmap_atomic" has inline asm
KLEE: WARNING ONCE: function "fc_queuecommand" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_recv" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_pkt_release" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_lock_pkt" has inline asm
KLEE: WARNING ONCE: function "fc_eh_abort" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_cleanup_each_cmd" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_cmd_send" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_rec" has inline asm
KLEE: WARNING ONCE: function "fc_fcp_srr" has inline asm
KLEE: WARNING: undefined reference to function: mempool_free_slab
KLEE: WARNING ONCE: flushing 32768 bytes on read, may be slow and/or crash: MO254[32768] allocated at global:__per_cpu_offset
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:29834: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:29844: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27121: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27156: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27072: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27141: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27172: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27172: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-i1kBnY/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:27161: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
