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--xhci-hcd.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.: 717 444 6071 54345
Removed infinite loop in xhci_get_input_control_ctx
Removed infinite loop in arch_local_save_flags
Removed infinite loop in xhci_alloc_container_ctx
Removed infinite loop in xhci_setup_addressable_virt_dev
Removed infinite loop in xhci_endpoint_init
Removed infinite loop in xhci_get_endpoint_interval
Removed infinite loop in xhci_get_endpoint_type
INFO: Compilation, preparation and instrumentation time: 1.87618398666
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'usb_put_hcd' (function is undefined)
Removed calls to 'usb_hcd_pci_remove' (function is undefined)
Removed calls to 'usb_remove_hcd' (function is undefined)
Defining function dev_get_drvdata as symbolic
Defining function usb_hcd_pci_probe as symbolic
Defining function usb_create_shared_hcd as symbolic
Defining function usb_add_hcd as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'usb_hcd_resume_root_hub' (function is undefined)
Removed calls to 'usb_wakeup_notification' (function is undefined)
Removed calls to 'usb_hcd_poll_rh_status' (function is undefined)
Removed calls to 'usb_hcd_unlink_urb_from_ep' (function is undefined)
Removed calls to 'usb_hcd_giveback_urb' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'usb_enable_xhci_ports' (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 'usb_amd_dev_put' (function is undefined)
Removed calls to 'usb_disable_xhci_ports' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function __dynamic_dev_dbg as symbolic
Defining function dev_warn as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function wait_for_completion_interruptible_timeout as symbolic
Removed calls to 'usb_hc_died' (function is undefined)
Defining function dev_err as symbolic
Removed calls to 'dma_pool_free' (function is undefined)
Defining function dma_pool_alloc as symbolic
Defining function _dev_info as symbolic
Defining function radix_tree_delete as symbolic
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function printk as symbolic
Defining function radix_tree_insert as symbolic
Defining function radix_tree_lookup as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'usb_amd_quirk_pll_enable' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function usb_acpi_power_manageable as symbolic
Defining function usb_acpi_set_power_state as symbolic
Defining function usb_hcd_check_unlink_urb as symbolic
Removed calls to 'usb_amd_quirk_pll_disable' (function is undefined)
Defining function __printk_ratelimit as symbolic
Defining function usb_hcd_link_urb_to_ep as symbolic
Defining function sg_next as symbolic
Defining function usb_hcd_is_primary_hcd as symbolic
Removed calls to 'dma_pool_destroy' (function is undefined)
Defining function usb_is_intel_switchable_xhci as symbolic
Removed calls to 'usb_root_hub_lost_power' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'set_timer_slack' (function is undefined)
Defining function mod_timer as symbolic
Defining function dmi_get_system_info as symbolic
Defining function strstr as symbolic
Defining function dma_pool_create as symbolic
Removed calls to 'synchronize_irq' (function is undefined)
Defining function usb_hcd_irq as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_block as symbolic
Defining function pci_enable_msix as symbolic
Defining function __bitmap_weight as symbolic
Defining function pci_set_mwi as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dma_set_mask as symbolic
Defining function usb_amd_find_chipset_info as symbolic
Removed calls to 'complete' (function is undefined)
Defining function ___ratelimit as symbolic
Defining function del_timer as symbolic
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Defining function usb_disabled as symbolic
Defining function platform_get_irq as symbolic
Defining function platform_get_resource as symbolic
Defining function usb_create_hcd as symbolic
Defining function __request_region as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function platform_driver_register as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 2.40187597275
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 879 312 3113 37507
INFO: Starting verification
KLEE: WARNING ONCE: function "xhci_handshake" has inline asm
KLEE: WARNING ONCE: function "xhci_irq" has inline asm
KLEE: WARNING ONCE: function "xhci_run" has inline asm
KLEE: WARNING ONCE: function "xhci_stop" has inline asm
KLEE: WARNING ONCE: function "xhci_shutdown" has inline asm
KLEE: WARNING ONCE: function "xhci_get_frame" has inline asm
KLEE: WARNING ONCE: function "xhci_urb_enqueue" has inline asm
KLEE: WARNING ONCE: function "xhci_urb_dequeue" has inline asm
KLEE: WARNING ONCE: function "xhci_hub_status_data" has inline asm
KLEE: WARNING ONCE: function "xhci_hub_control" has inline asm
KLEE: WARNING ONCE: function "xhci_bus_suspend" has inline asm
KLEE: WARNING ONCE: function "xhci_bus_resume" has inline asm
KLEE: WARNING ONCE: function "xhci_free_dev" has inline asm
KLEE: WARNING ONCE: function "xhci_alloc_streams" has inline asm
KLEE: WARNING ONCE: function "xhci_add_endpoint" has inline asm
KLEE: WARNING ONCE: function "xhci_drop_endpoint" has inline asm
KLEE: WARNING ONCE: function "xhci_check_bandwidth" has inline asm
KLEE: WARNING ONCE: function "xhci_address_device" has inline asm
KLEE: WARNING ONCE: function "xhci_update_hub_device" has inline asm
KLEE: WARNING ONCE: function "xhci_update_device" has inline asm
KLEE: WARNING ONCE: function "xhci_set_usb2_hardware_lpm" has inline asm
KLEE: WARNING ONCE: function "xhci_change_max_exit_latency" has inline asm
KLEE: WARNING ONCE: function "xhci_configure_endpoint" has inline asm
KLEE: WARNING ONCE: function "xhci_count_num_new_endpoints" has inline asm
KLEE: WARNING ONCE: function "xhci_ring_cmd_db" has inline asm
KLEE: WARNING ONCE: function "xhci_cancel_cmd" has inline asm
KLEE: WARNING ONCE: function "xhci_halt" has inline asm
KLEE: WARNING ONCE: function "prepare_ring" has inline asm
KLEE: WARNING ONCE: function "queue_trb" has inline asm
KLEE: WARNING ONCE: function "xhci_ring_device" has inline asm
KLEE: WARNING ONCE: function "xhci_free_stream_info" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "xhci_alloc_container_ctx" has inline asm
KLEE: WARNING ONCE: function "xhci_setup_addressable_virt_dev" has inline asm
KLEE: WARNING ONCE: function "xhci_zero_in_ctx" has inline asm
KLEE: WARNING ONCE: function "xhci_endpoint_init" has inline asm
KLEE: WARNING ONCE: function "xhci_microframes_to_exponent" has inline asm
KLEE: WARNING ONCE: function "xhci_setup_input_ctx_for_config_ep" has inline asm
KLEE: WARNING ONCE: function "xhci_alloc_stream_info" has inline asm
KLEE: WARNING ONCE: function "xhci_setup_streams_ep_input_ctx" has inline asm
KLEE: WARNING ONCE: function "xhci_stop_endpoint_command_watchdog" has inline asm
KLEE: WARNING ONCE: function "xhci_queue_isoc_tx_prepare" has inline asm
KLEE: WARNING ONCE: function "giveback_first_trb" has inline asm
KLEE: WARNING ONCE: function "xhci_reset" has inline asm
KLEE: WARNING ONCE: function "xhci_print_ir_set" has inline asm
KLEE: WARNING ONCE: function "xhci_resume" has inline asm
KLEE: WARNING ONCE: function "xhci_set_cmd_ring_deq" has inline asm
KLEE: WARNING ONCE: function "compliance_mode_recovery" has inline asm
KLEE: WARNING ONCE: function "xhci_mem_init" has inline asm
KLEE: WARNING ONCE: function "xhci_dbg_cmd_ptrs" has inline asm
KLEE: WARNING ONCE: function "xhci_dbg_regs" has inline asm
KLEE: WARNING ONCE: function "xhci_print_run_regs" has inline asm
KLEE: WARNING ONCE: function "xhci_suspend" has inline asm
KLEE: WARNING ONCE: function "xhci_event_ring_work" has inline asm
KLEE: WARNING ONCE: function "xhci_gen_setup" has inline asm
KLEE: WARNING ONCE: function "xhci_print_registers" has inline asm
KLEE: WARNING ONCE: function "handle_cmd_completion" has inline asm
KLEE: WARNING ONCE: function "xhci_dma_to_transfer_ring" has inline asm
KLEE: WARNING ONCE: function "ring_doorbell_for_active_rings" has inline asm
KLEE: WARNING ONCE: function "xhci_get_input_control_ctx" has inline asm
KLEE: WARNING ONCE: function "xhci_quiesce" has inline asm
KLEE: WARNING ONCE: function "xhci_set_link_state" has inline asm
KLEE: WARNING ONCE: function "xhci_test_and_clear_bit" has inline asm
KLEE: WARNING ONCE: function "xhci_ring_ep_doorbell" has inline asm
KLEE: WARNING ONCE: function "xhci_last_valid_endpoint" has inline asm
KLEE: WARNING: undefined reference to function: usb_hcd_pci_shutdown
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:4392: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:4392: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:25532: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:25448: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:6176: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:4392: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:25149: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:6176: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:6176: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:25397: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-RTvvWa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--usb--host--xhci-hcd.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:6176: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
