bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_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.: 330 137 3307 20831
Removed infinite loop in isp1362_irq
Removed infinite loop in isp1362_hc_reset
Removed infinite loop in isp1362_hc_start
Removed infinite loop in isp1362_hc_stop
Removed infinite loop in isp1362_urb_enqueue
Removed infinite loop in isp1362_get_frame
Removed infinite loop in isp1362_hub_status_data
Removed infinite loop in isp1362_hub_control
Removed infinite loop in isp1362_bus_suspend
Removed infinite loop in isp1362_bus_resume
Removed infinite loop in isp1362_suspend
Removed infinite loop in isp1362_resume
Removed infinite loop in isp1362_write_addr
Removed infinite loop in isp1362_write_data32
Removed infinite loop in arch_local_save_flags
Removed infinite loop in isp1362_read_data32
Removed infinite loop in isp1362_read_data16
Removed infinite loop in isp1362_write_data16
Removed infinite loop in finish_transfers
Removed infinite loop in isp1362_read_ptd
Removed infinite loop in postproc_ep
Removed infinite loop in isp1362_read_buffer
Removed infinite loop in isp1362_write_diraddr
Removed infinite loop in isp1362_read_fifo
Removed infinite loop in release_ptd_buffers
Removed infinite loop in remove_ptd
Removed infinite loop in isp1362_enable_int
Removed infinite loop in start_atl_transfers
Removed infinite loop in start_intl_transfers
Removed infinite loop in start_iso_transfers
Removed infinite loop in prepare_ptd
Removed infinite loop in isp1362_write_ptd
Removed infinite loop in enable_istl_transfers
Removed infinite loop in isp1362_write_buffer
Removed infinite loop in isp1362_write_fifo
Removed infinite loop in submit_req
Removed infinite loop in enable_intl_transfers
Removed infinite loop in claim_ptd_buffers
Removed infinite loop in enable_atl_transfers
Removed infinite loop in __isp1362_sw_reset
Removed infinite loop in isp1362_mem_config
Removed infinite loop in finish_unlinks
Removed infinite loop in proc_isp1362_show
Removed infinite loop in dump_regs
INFO: Compilation, preparation and instrumentation time: 0.728899002075
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'usb_put_hcd' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'usb_remove_hcd' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'usb_hcd_resume_root_hub' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'usb_hcd_unlink_urb_from_ep' (function is undefined)
Removed calls to 'usb_put_dev' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function __dynamic_pr_debug as symbolic
Defining function platform_get_resource as symbolic
Defining function dev_get_drvdata as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function usb_disabled as symbolic
Defining function __request_region as symbolic
Defining function usb_create_hcd as symbolic
Defining function usb_add_hcd as symbolic
Defining function printk as symbolic
Defining function create_proc_entry as symbolic
Defining function ioremap_nocache as symbolic
Defining function msecs_to_jiffies as symbolic
Removed calls to 'usb_hcd_giveback_urb' (function is undefined)
Removed calls to 'bitmap_clear' (function is undefined)
Removed calls to 'bitmap_set' (function is undefined)
Defining function usb_hcd_check_unlink_urb as symbolic
Defining function usb_hcd_link_urb_to_ep as symbolic
Defining function usb_get_dev as symbolic
Defining function usb_calc_bus_time as symbolic
Defining function bitmap_find_next_zero_area as symbolic
Defining function del_timer_sync as symbolic
Defining function _dev_info as symbolic
Defining function snprintf as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.43971991539
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 258 107 879 5666
INFO: Starting verification
KLEE: WARNING ONCE: function "isp1362_irq" has inline asm
KLEE: WARNING ONCE: function "isp1362_hub_status_data" has inline asm
KLEE: WARNING ONCE: function "isp1362_hub_control" has inline asm
KLEE: WARNING ONCE: function "isp1362_bus_resume" has inline asm
KLEE: WARNING ONCE: function "isp1362_write_addr" has inline asm
KLEE: WARNING ONCE: function "isp1362_write_data32" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" has inline asm
KLEE: WARNING ONCE: function "isp1362_read_data32" has inline asm
KLEE: WARNING ONCE: function "isp1362_write_data16" has inline asm
KLEE: WARNING ONCE: function "isp1362_read_data16" has inline asm
KLEE: WARNING ONCE: function "finish_transfers" has inline asm
KLEE: WARNING ONCE: function "finish_iso_transfers" has inline asm
KLEE: WARNING ONCE: function "isp1362_read_ptd" has inline asm
KLEE: WARNING ONCE: function "postproc_ep" has inline asm
KLEE: WARNING ONCE: function "isp1362_read_buffer" has inline asm
KLEE: WARNING ONCE: function "isp1362_write_diraddr" has inline asm
KLEE: WARNING ONCE: function "release_ptd_buffers" has inline asm
KLEE: WARNING ONCE: function "remove_ptd" has inline asm
KLEE: WARNING ONCE: function "start_atl_transfers" has inline asm
KLEE: WARNING ONCE: function "start_intl_transfers" has inline asm
KLEE: WARNING ONCE: function "start_iso_transfers" has inline asm
KLEE: WARNING ONCE: function "prepare_ptd" has inline asm
KLEE: WARNING ONCE: function "isp1362_write_ptd" has inline asm
KLEE: WARNING ONCE: function "isp1362_write_buffer" has inline asm
KLEE: WARNING ONCE: function "submit_req" has inline asm
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3951: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11839: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:7689: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9431: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3578: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3585: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3919: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3919: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9334: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9334: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9335: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10615: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:7693: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9104: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uFb7ix/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10006: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
