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--staging--keucr--keucr.ko-ldv_main1_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.: 163 173 2419 32438
INFO: Compilation, preparation and instrumentation time: 0.974838972092
Removed calls to 'scsi_cmd_get_serial' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (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 'wait_for_completion' (function is undefined)
Removed calls to 'blk_queue_update_dma_alignment' (function is undefined)
Removed calls to 'blk_queue_max_hw_sectors' (function is undefined)
Defining function sscanf as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function printk as symbolic
Removed calls to 'scsi_report_bus_reset' (function is undefined)
Defining function dev_get_drvdata as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Defining function dev_set_drvdata as symbolic
Defining function kthread_stop as symbolic
Defining function scsi_host_alloc as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'scsi_scan_host' (function is undefined)
Removed calls to 'complete_and_exit' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Removed calls to 'usb_sg_cancel' (function is undefined)
Removed calls to 'usb_sg_wait' (function is undefined)
Defining function usb_sg_init as symbolic
Removed calls to 'usb_reset_endpoint' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Defining function usb_submit_urb as symbolic
Defining function usb_unlink_urb as symbolic
Defining function wait_for_completion_interruptible_timeout as symbolic
Defining function set_freezable as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function __refrigerator as symbolic
Defining function freezing_slow_path as symbolic
Defining function scsi_add_host_with_dma as symbolic
Defining function usb_alloc_urb as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function wait_for_completion_interruptible as symbolic
Defining function kthread_should_stop as symbolic
Defining function sg_next as symbolic
Removed calls to 'scsi_eh_prep_cmnd' (function is undefined)
Removed calls to 'scsi_eh_restore_cmnd' (function is undefined)
Removed calls to 'scsi_report_device_reset' (function is undefined)
Defining function usb_lock_device_for_reset as symbolic
Defining function usb_reset_device as symbolic
Removed calls to '___udelay' (function is undefined)
Defining function usb_alloc_coherent as symbolic
Defining function sprintf as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function usb_register_driver as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.583508014679
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 286 156 1143 12039
INFO: Starting verification
KLEE: WARNING ONCE: function "command_abort" has inline asm
KLEE: WARNING ONCE: function "quiesce_and_remove_host" has inline asm
KLEE: WARNING ONCE: function "usb_stor_Bulk_reset" has inline asm
KLEE: WARNING ONCE: function "ENE_stor_invoke_transport" has inline asm
KLEE: WARNING ONCE: function "usb_stor_invoke_transport" has inline asm
KLEE: WARNING ONCE: function "usb_stor_control_thread" has inline asm
KLEE: WARNING ONCE: function "usb_stor_scan_thread" has inline asm
KLEE: WARNING ONCE: function "usb_stor_bulk_transfer_sglist" has inline asm
KLEE: WARNING ONCE: function "usb_stor_msg_common" has inline asm
KLEE: WARNING ONCE: function "usb_stor_access_xfer_buf" has inline asm
KLEE: WARNING ONCE: function "Conv_D_MediaAddr" has inline asm
KLEE: WARNING ONCE: function "Inc_D_MediaAddr" has inline asm
KLEE: WARNING ONCE: function "Make_D_LogTable" has inline asm
KLEE: WARNING ONCE: function "Load_D_LogBlockAddr" has inline asm
KLEE: WARNING ONCE: function "Read_D_PhyOneSect" has inline asm
KLEE: WARNING ONCE: function "Copy_D_PhyOneSect" has inline asm
KLEE: WARNING ONCE: function "Search_D_CIS" has inline asm
KLEE: WARNING ONCE: function "usb_stor_stop_transport" has inline asm
KLEE: WARNING ONCE: function "Set_D_LogBlockAddr" has inline asm
KLEE: WARNING ONCE: function "Check_D_FailBlock" has inline asm
KLEE: WARNING ONCE: function "Check_D_DataStatus" has inline asm
KLEE: WARNING ONCE: flushing 16384 bytes on read, may be slow and/or crash: MO32[16384] allocated at global:Assign
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8672: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8673: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8641: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8642: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8103: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:12854: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8558: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8559: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8649: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-n5gPaw/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:8208: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
