bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.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.: 1457 646 8483 66763
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.90382409096
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__dynamic_dev_dbg' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'usb_remove_hcd' (function is undefined)
Removed calls to 'usb_put_hcd' (function is undefined)
Removed calls to 'usb_del_gadget_udc' (function is undefined)
Removed calls to 'clk_disable' (function is undefined)
Removed calls to 'clk_unprepare' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function del_timer as symbolic
Defining function cancel_work_sync as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function printk as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'usb_hcd_unlink_urb_from_ep' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'usb_hcd_giveback_urb' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Defining function of_match_device as symbolic
Defining function platform_get_irq as symbolic
Removed calls to 'dev_warn' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function platform_get_resource as symbolic
Defining function devm_ioremap_resource as symbolic
Defining function of_usb_get_dr_mode as symbolic
Defining function devm_phy_get as symbolic
Defining function devm_usb_get_phy as symbolic
Defining function phy_power_on as symbolic
Defining function phy_init as symbolic
Removed calls to 'usleep_range' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_regset32 as symbolic
Defining function debugfs_create_file as symbolic
Defining function usb_disabled as symbolic
Defining function dma_set_mask as symbolic
Defining function usb_create_hcd as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'usb_hcd_resume_root_hub' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Defining function usb_add_hcd as symbolic
Defining function device_wakeup_enable as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'usb_gadget_giveback_request' (function is undefined)
Removed calls to 'iowrite32_rep' (function is undefined)
Defining function usb_gadget_map_request as symbolic
Defining function devm_clk_get as symbolic
Defining function devm_regulator_bulk_get as symbolic
Defining function regulator_bulk_enable as symbolic
Defining function regulator_bulk_disable as symbolic
Defining function usb_add_gadget_udc as symbolic
Defining function snprintf as symbolic
Defining function phy_power_off as symbolic
Defining function phy_exit as symbolic
Removed calls to 'ioread32_rep' (function is undefined)
Removed calls to 'usb_gadget_unmap_request' (function is undefined)
Defining function usb_speed_string as symbolic
Defining function clk_prepare as symbolic
Defining function clk_enable as symbolic
Defining function of_find_property as symbolic
Defining function of_property_read_u32_array as symbolic
Defining function devm_request_threaded_irq as symbolic
Defining function mod_timer as symbolic
Defining function queue_work_on as symbolic
Defining function dma_supported as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function usb_hcd_check_unlink_urb as symbolic
Defining function usb_hcd_link_urb_to_ep as symbolic
Removed calls to 'usb_hcd_unmap_urb_for_dma' (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 usb_calc_bus_time as symbolic
Defining function usb_hub_clear_tt_buffer as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function ldv_suspend_late_13 as symbolic
Defining function ldv_restore_early_13 as symbolic
Defining function ldv_resume_early_13 as symbolic
Defining function ldv_thaw_early_13 as symbolic
Defining function ldv_resume_noirq_13 as symbolic
Defining function ldv_freeze_noirq_13 as symbolic
Defining function ldv_prepare_13 as symbolic
Defining function ldv_freeze_late_13 as symbolic
Defining function ldv_thaw_noirq_13 as symbolic
Defining function ldv_poweroff_noirq_13 as symbolic
Defining function ldv_poweroff_late_13 as symbolic
Defining function ldv_restore_noirq_13 as symbolic
Defining function ldv_suspend_noirq_13 as symbolic
Defining function ldv_complete_13 as symbolic
Defining function __platform_driver_register as symbolic
Linked our definitions to these undefined functions:
  strncmp
  __kmalloc
  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: 2.1443669796
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1381 510 3739 45801
INFO: Starting verification
KLEE: WARNING ONCE: function "dwc2_hcd_release" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_reset_func" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_qh_unlink" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_qh_free_ddma" has inline asm
KLEE: WARNING ONCE: function "dwc2_release_channel_ddma" has inline asm
KLEE: WARNING ONCE: function "dwc2_handle_common_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_get_hwparams" has inline asm
KLEE: WARNING ONCE: function "dwc2_gadget_init" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_init" has inline asm
KLEE: WARNING ONCE: function "dwc2_core_init" has inline asm
KLEE: WARNING ONCE: function "dwc2_conn_id_status_change" has inline asm
KLEE: WARNING ONCE: function "dwc2_wakeup_detected" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_dump_state" has inline asm
KLEE: WARNING ONCE: function "dwc2_dump_global_registers" has inline asm
KLEE: WARNING ONCE: function "dwc2_dump_host_registers" has inline asm
KLEE: WARNING ONCE: function "_dwc2_hcd_start" has inline asm
KLEE: WARNING ONCE: function "dwc2_core_host_init" has inline asm
KLEE: WARNING ONCE: function "dwc2_init_fs_ls_pclk_sel" has inline asm
KLEE: WARNING ONCE: function "dwc2_flush_tx_fifo" has inline asm
KLEE: WARNING ONCE: function "dwc2_flush_rx_fifo" has inline asm
KLEE: WARNING ONCE: function "dwc2_enable_host_interrupts" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_core_init_disconnected" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_start" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_corereset" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_init_fifo" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_en_gsint" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_ctrl_epint" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_complete_setup" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_start_req" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_write_fifo" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_ep_sethalt" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_stall_ep0" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "dwc2_core_reset" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_init" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_irq" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_initep" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_dump" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_set_ep_maxpacket" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_epint" has inline asm
KLEE: WARNING ONCE: function "dwc2_exit_hibernation" has inline asm
KLEE: WARNING ONCE: function "kill_all_requests" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_handle_outdone" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_rx_data" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_program_zlp" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_txfifo_flush" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_disconnect" has inline asm
KLEE: WARNING ONCE: function "dwc2_enter_hibernation" has inline asm
KLEE: WARNING ONCE: function "dwc2_suspend" has inline asm
KLEE: WARNING ONCE: function "dwc2_resume" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_resume" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_suspend" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_ep_disable" has inline asm
KLEE: WARNING ONCE: function "_dwc2_hcd_get_frame_number" has inline asm
KLEE: WARNING ONCE: function "_dwc2_hcd_urb_enqueue" has inline asm
KLEE: WARNING ONCE: function "_dwc2_hcd_urb_dequeue" has inline asm
KLEE: WARNING ONCE: function "_dwc2_hcd_hub_control" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_queue_transactions" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_start_xfer_ddma" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_start_transfer" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_halt" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_continue_transfer" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_write_packet" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_do_ping" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_start_transfer_ddma" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_qh_deactivate" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_qh_add" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_qtd_add" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_init" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_qh_init_ddma" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_stop" has inline asm
KLEE: WARNING ONCE: function "dwc2_handle_hcd_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_read_packet" has inline asm
KLEE: WARNING ONCE: function "dwc2_calc_frame_interval" has inline asm
KLEE: WARNING ONCE: function "dwc2_release_channel" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_xfercomp_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_ack_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_stall_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_xacterr_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_ahberr_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_babble_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_frmovrun_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_nyet_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_nak_intr" has inline asm
KLEE: WARNING ONCE: function "dwc2_halt_channel" has inline asm
KLEE: WARNING ONCE: function "dwc2_update_urb_state_abn" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_save_data_toggle" has inline asm
KLEE: WARNING ONCE: function "dwc2_get_actual_xfer_length" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dwc2_update_urb_state" has inline asm
KLEE: WARNING ONCE: function "dwc2_complete_periodic_xfer" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_gadget_getframe" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_vbus_session" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_pullup" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_ep_enable" has inline asm
KLEE: WARNING ONCE: function "state_show" has inline asm
KLEE: WARNING ONCE: function "testmode_write" has inline asm
KLEE: WARNING ONCE: function "testmode_show" has inline asm
KLEE: WARNING ONCE: function "fifo_show" has inline asm
KLEE: WARNING ONCE: function "ep_show" has inline asm
KLEE: WARNING ONCE: function "dwc2_disable_host_interrupts" has inline asm
KLEE: WARNING ONCE: function "dwc2_hc_cleanup" has inline asm
KLEE: WARNING ONCE: function "dwc2_disable_global_interrupts" has inline asm
KLEE: WARNING ONCE: function "dwc2_enable_global_interrupts" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_core_connect" has inline asm
KLEE: WARNING ONCE: function "s3c_hsotg_set_test_mode" has inline asm
KLEE: WARNING ONCE: function "dwc2_is_controller_alive" has inline asm
KLEE: WARNING ONCE: function "dwc2_hcd_get_frame_number" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_11" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_9" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_d81c35ff-752a-4a0c-be8e-71b5199f9260/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING: killing 20608 states (over memory cap)
KLEE: WARNING: killing 16041 states (over memory cap)
KLEE: WARNING: killing 15133 states (over memory cap)
KLEE: WARNING: killing 14827 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15050 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:17625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:27759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:30758: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:30540: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:30645: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14145 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:30328: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14963 states (over memory cap)
KLEE: WARNING: killing 14837 states (over memory cap)
KLEE: WARNING: killing 14120 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:31928: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:31139: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:30898: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14850 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:31100: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:31055: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:30994: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 16140 states (over memory cap)
KLEE: WARNING: killing 16186 states (over memory cap)
KLEE: WARNING: killing 16747 states (over memory cap)
KLEE: WARNING: killing 17141 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:32276: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17199 states (over memory cap)
KLEE: WARNING: killing 16672 states (over memory cap)
KLEE: WARNING: killing 16979 states (over memory cap)
KLEE: WARNING: killing 17714 states (over memory cap)
KLEE: WARNING: killing 18030 states (over memory cap)
KLEE: WARNING: killing 17501 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:12330: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17115 states (over memory cap)
KLEE: WARNING: killing 17753 states (over memory cap)
KLEE: WARNING: killing 17236 states (over memory cap)
KLEE: WARNING: killing 16875 states (over memory cap)
KLEE: WARNING: killing 16272 states (over memory cap)
KLEE: WARNING: killing 17159 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wu_JPJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--dwc2--dwc2.ko-entry_point_true-unreach-call.cil.out.c:11040: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16558 states (over memory cap)
KLEE: WARNING: killing 15704 states (over memory cap)
KLEE: WARNING: killing 16255 states (over memory cap)
KLEE: WARNING: killing 15822 states (over memory cap)
KLEE: WARNING: killing 16035 states (over memory cap)
KLEE: WARNING: killing 16259 states (over memory cap)
KLEE: WARNING: killing 16475 states (over memory cap)
KLEE: WARNING: killing 15390 states (over memory cap)
KLEE: WARNING: killing 16430 states (over memory cap)
KLEE: WARNING: killing 16729 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_d81c35ff-752a-4a0c-be8e-71b5199f9260/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16136 states (over memory cap)
KLEE: WARNING: killing 16111 states (over memory cap)
KLEE: WARNING: killing 16819 states (over memory cap)
KLEE: WARNING: killing 16153 states (over memory cap)
KLEE: WARNING: killing 16369 states (over memory cap)
KLEE: WARNING: killing 17156 states (over memory cap)
KLEE: WARNING: killing 16413 states (over memory cap)
KLEE: WARNING: killing 16634 states (over memory cap)
KLEE: WARNING: killing 16452 states (over memory cap)
KLEE: WARNING: killing 16438 states (over memory cap)
KLEE: WARNING: killing 16256 states (over memory cap)
KLEE: WARNING: killing 16479 states (over memory cap)
KLEE: WARNING: killing 16784 states (over memory cap)
KLEE: WARNING: killing 16197 states (over memory cap)
KLEE: WARNING: killing 16821 states (over memory cap)
KLEE: WARNING: killing 16486 states (over memory cap)
KLEE: WARNING: killing 15421 states (over memory cap)
KLEE: WARNING: killing 16357 states (over memory cap)
KLEE: WARNING: killing 16254 states (over memory cap)
KLEE: WARNING: killing 15917 states (over memory cap)
KLEE: WARNING: killing 16936 states (over memory cap)
KLEE: WARNING: killing 16201 states (over memory cap)
KLEE: WARNING: killing 16417 states (over memory cap)
KLEE: WARNING: killing 16636 states (over memory cap)
KLEE: WARNING: killing 16850 states (over memory cap)
KLEE: WARNING: killing 16203 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 16235 states (over memory cap)
KLEE: WARNING: killing 16383 states (over memory cap)
KLEE: WARNING: killing 16838 states (over memory cap)
KLEE: WARNING: killing 16507 states (over memory cap)
KLEE: WARNING: killing 16567 states (over memory cap)
KLEE: WARNING: killing 17178 states (over memory cap)
KLEE: WARNING: killing 15908 states (over memory cap)
KLEE: WARNING: killing 16202 states (over memory cap)
KLEE: WARNING: killing 16729 states (over memory cap)
KLEE: WARNING: killing 17100 states (over memory cap)
KLEE: WARNING: killing 16531 states (over memory cap)
KLEE: WARNING: killing 15738 states (over memory cap)
KLEE: WARNING: killing 15632 states (over memory cap)
KLEE: WARNING: killing 16235 states (over memory cap)
KLEE: WARNING: killing 16531 states (over memory cap)
KLEE: WARNING: killing 16740 states (over memory cap)
KLEE: WARNING: killing 16106 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
KLEE: WARNING: killing 17229 states (over memory cap)
KLEE: WARNING: killing 15972 states (over memory cap)
KLEE: WARNING: killing 16727 states (over memory cap)
KLEE: WARNING: killing 16947 states (over memory cap)
KLEE: WARNING: killing 16542 states (over memory cap)
KLEE: WARNING: killing 16374 states (over memory cap)
KLEE: WARNING: killing 16433 states (over memory cap)
KLEE: WARNING: killing 16797 states (over memory cap)
KLEE: WARNING: killing 16627 states (over memory cap)
KLEE: WARNING: killing 16768 states (over memory cap)
KLEE: WARNING: killing 16141 states (over memory cap)
KLEE: WARNING: killing 16122 states (over memory cap)
KLEE: WARNING: killing 16258 states (over memory cap)
KLEE: WARNING: killing 16701 states (over memory cap)
KLEE: WARNING: killing 16381 states (over memory cap)
KLEE: WARNING: killing 15979 states (over memory cap)
KLEE: WARNING: killing 15659 states (over memory cap)
KLEE: WARNING: killing 16481 states (over memory cap)
KLEE: WARNING: killing 16611 states (over memory cap)
KLEE: WARNING: killing 16368 states (over memory cap)
KLEE: WARNING: killing 16351 states (over memory cap)
KLEE: WARNING: killing 16033 states (over memory cap)
KLEE: WARNING: killing 15863 states (over memory cap)
KLEE: WARNING: killing 16227 states (over memory cap)
KLEE: WARNING: killing 16362 states (over memory cap)
KLEE: WARNING: killing 16267 states (over memory cap)
KLEE: WARNING: killing 16254 states (over memory cap)
KLEE: WARNING: killing 16774 states (over memory cap)
KLEE: WARNING: killing 16382 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 16938 states (over memory cap)
KLEE: WARNING: killing 16621 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 15761 states (over memory cap)
KLEE: WARNING: killing 16338 states (over memory cap)
KLEE: WARNING: killing 16698 states (over memory cap)
KLEE: WARNING: killing 15937 states (over memory cap)
KLEE: WARNING: killing 15843 states (over memory cap)
KLEE: WARNING: killing 16427 states (over memory cap)
KLEE: WARNING: killing 16409 states (over memory cap)
KLEE: WARNING: killing 16623 states (over memory cap)
KLEE: WARNING: killing 16688 states (over memory cap)
KLEE: WARNING: killing 16374 states (over memory cap)
KLEE: WARNING: killing 16508 states (over memory cap)
KLEE: WARNING: killing 16642 states (over memory cap)
KLEE: WARNING: killing 15365 states (over memory cap)
