bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-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.: 644 262 2710 18046
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in arch_local_save_flags
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dwc3_prepare_one_trb
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.646835803986
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'pm_runtime_enable' (function is undefined)
Removed calls to 'pm_runtime_forbid' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to '__pm_runtime_disable' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Defining function phy_power_off as symbolic
Removed calls to 'platform_device_unregister' (function is undefined)
Defining function phy_exit as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'usb_del_gadget_udc' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function __pm_runtime_idle as symbolic
Defining function dev_err as symbolic
Defining function platform_get_resource as symbolic
Defining function devm_ioremap_resource as symbolic
Defining function phy_power_on as symbolic
Defining function debugfs_create_dir as symbolic
Removed calls to 'platform_device_put' (function is undefined)
Defining function platform_device_alloc as symbolic
Defining function platform_device_add_resources as symbolic
Defining function platform_device_add as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function __dynamic_dev_dbg as symbolic
Defining function snprintf as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function __phys_addr as symbolic
Defining function phy_init as symbolic
Defining function __pm_runtime_resume as symbolic
Defining function dma_supported as symbolic
Defining function devm_usb_get_phy_by_phandle as symbolic
Defining function devm_usb_get_phy as symbolic
Defining function devm_phy_get as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function __pm_runtime_set_status as symbolic
Removed calls to 'usb_gadget_unmap_request' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Defining function platform_get_irq as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'usb_gadget_set_state' (function is undefined)
Defining function dev_driver_string as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function usb_gadget_map_request as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function sg_next as symbolic
Defining function __dynamic_pr_debug as symbolic
Defining function strlcat as symbolic
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
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
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_suspend_late_10 as symbolic
Defining function ldv_restore_early_10 as symbolic
Defining function ldv_resume_early_10 as symbolic
Defining function ldv_thaw_early_10 as symbolic
Defining function ldv_resume_noirq_10 as symbolic
Defining function ldv_freeze_noirq_10 as symbolic
Defining function ldv_freeze_late_10 as symbolic
Defining function ldv_thaw_noirq_10 as symbolic
Defining function ldv_poweroff_noirq_10 as symbolic
Defining function ldv_poweroff_late_10 as symbolic
Defining function ldv_restore_noirq_10 as symbolic
Defining function ldv_suspend_noirq_10 as symbolic
Defining function __platform_driver_register as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strncmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.710283994675
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 432 190 1367 11039
INFO: Starting verification
KLEE: WARNING ONCE: function "dwc3_probe" has inline asm
KLEE: WARNING ONCE: function "dwc3_event_buffers_cleanup" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "dwc3_send_gadget_generic_command" has inline asm
KLEE: WARNING ONCE: function "dwc3_event_buffers_setup" has inline asm
KLEE: WARNING ONCE: function "dwc3_suspend" has inline asm
KLEE: WARNING ONCE: function "dwc3_resume" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_resume" has inline asm
KLEE: WARNING ONCE: function "__dwc3_gadget_ep_enable" has inline asm
KLEE: WARNING ONCE: function "__dwc3_gadget_ep_disable" has inline asm
KLEE: WARNING ONCE: function "dwc3_send_gadget_ep_cmd" has inline asm
KLEE: WARNING ONCE: function "dwc3_ep0_start_trans" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_complete" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_run_stop" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_prepare" has inline asm
KLEE: WARNING ONCE: function "dwc3_set_mode" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_suspend" has inline asm
KLEE: WARNING ONCE: function "dwc3_interrupt" has inline asm
KLEE: WARNING ONCE: function "dwc3_thread_interrupt" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_disconnect_interrupt" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_reset_interrupt" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_set_link_state" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_resize_tx_fifos" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_set_test_mode" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_6" has inline asm
KLEE: WARNING ONCE: function "dwc3_mode_write" has inline asm
KLEE: WARNING ONCE: function "dwc3_mode_show" has inline asm
KLEE: WARNING ONCE: function "dwc3_testmode_write" has inline asm
KLEE: WARNING ONCE: function "dwc3_testmode_show" has inline asm
KLEE: WARNING ONCE: function "__dwc3_gadget_kick_transfer" has inline asm
KLEE: WARNING ONCE: function "dwc3_link_state_show" has inline asm
KLEE: WARNING ONCE: function "dwc3_gadget_get_link_state" has inline asm
KLEE: WARNING ONCE: function "dwc3_ep0_interrupt" has inline asm
KLEE: WARNING ONCE: function "dwc3_ep0_handle_feature" has inline asm
KLEE: WARNING ONCE: function "dwc3_ep0_set_sel_cmpl" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_8ad8af0d-7a01-443b-9390-af8a1513983e/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 11551 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15371 states (over memory cap)
KLEE: WARNING: killing 15121 states (over memory cap)
KLEE: WARNING: killing 14871 states (over memory cap)
KLEE: WARNING: killing 14943 states (over memory cap)
KLEE: WARNING: killing 13766 states (over memory cap)
KLEE: WARNING: killing 13842 states (over memory cap)
KLEE: WARNING: killing 13707 states (over memory cap)
KLEE: WARNING: killing 13776 states (over memory cap)
KLEE: WARNING: killing 13847 states (over memory cap)
KLEE: WARNING: killing 14328 states (over memory cap)
KLEE: WARNING: killing 13794 states (over memory cap)
KLEE: WARNING: killing 14273 states (over memory cap)
KLEE: WARNING: killing 14958 states (over memory cap)
KLEE: WARNING: killing 15240 states (over memory cap)
KLEE: WARNING: killing 15117 states (over memory cap)
KLEE: WARNING: killing 14988 states (over memory cap)
KLEE: WARNING: killing 15570 states (over memory cap)
KLEE: WARNING: killing 15855 states (over memory cap)
KLEE: WARNING: killing 14828 states (over memory cap)
KLEE: WARNING: killing 16216 states (over memory cap)
KLEE: WARNING: killing 15597 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 15960 states (over memory cap)
KLEE: WARNING: killing 17044 states (over memory cap)
KLEE: WARNING: killing 16026 states (over memory cap)
KLEE: WARNING: killing 16409 states (over memory cap)
KLEE: WARNING: killing 16685 states (over memory cap)
KLEE: WARNING: killing 15772 states (over memory cap)
KLEE: WARNING: killing 16449 states (over memory cap)
KLEE: WARNING: killing 15431 states (over memory cap)
KLEE: WARNING: killing 15209 states (over memory cap)
KLEE: WARNING: killing 16086 states (over memory cap)
KLEE: WARNING: killing 15375 states (over memory cap)
KLEE: WARNING: killing 15748 states (over memory cap)
KLEE: WARNING: killing 15231 states (over memory cap)
KLEE: WARNING: killing 15607 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8529: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15283 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:5737: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:13319: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:10537: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15261 states (over memory cap)
KLEE: WARNING: killing 15634 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8649: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15124 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:11052: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8663: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8786: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:12986: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8554: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15962 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:5551: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15557 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8496: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15415 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8368: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15588 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:7743: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15766 states (over memory cap)
KLEE: WARNING: killing 15941 states (over memory cap)
KLEE: WARNING: killing 15049 states (over memory cap)
KLEE: WARNING: killing 16192 states (over memory cap)
KLEE: WARNING: killing 15690 states (over memory cap)
KLEE: WARNING: killing 15871 states (over memory cap)
KLEE: WARNING: killing 15460 states (over memory cap)
KLEE: WARNING: killing 16119 states (over memory cap)
KLEE: WARNING: killing 15811 states (over memory cap)
KLEE: WARNING: killing 15793 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
KLEE: WARNING: killing 16234 states (over memory cap)
KLEE: WARNING: killing 15740 states (over memory cap)
KLEE: WARNING: killing 15630 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8468: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:10970: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15788 states (over memory cap)
KLEE: WARNING: killing 15669 states (over memory cap)
KLEE: WARNING: killing 15940 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:7743: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15443 states (over memory cap)
KLEE: WARNING: killing 15806 states (over memory cap)
KLEE: WARNING: killing 15698 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:13417: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15873 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:13219: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 16206 states (over memory cap)
KLEE: WARNING: killing 15614 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 14725 states (over memory cap)
KLEE: WARNING: killing 16033 states (over memory cap)
KLEE: WARNING: killing 16110 states (over memory cap)
KLEE: WARNING: killing 15053 states (over memory cap)
KLEE: WARNING: killing 15794 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:12848: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:8309: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14910 states (over memory cap)
KLEE: WARNING: killing 16398 states (over memory cap)
KLEE: WARNING: killing 15630 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:12741: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15704 states (over memory cap)
KLEE: WARNING: killing 15783 states (over memory cap)
KLEE: WARNING: killing 15487 states (over memory cap)
KLEE: WARNING: killing 16034 states (over memory cap)
KLEE: WARNING: killing 15836 states (over memory cap)
KLEE: WARNING: killing 15446 states (over memory cap)
KLEE: WARNING: killing 15336 states (over memory cap)
KLEE: WARNING: killing 15603 states (over memory cap)
KLEE: WARNING: killing 16149 states (over memory cap)
KLEE: WARNING: killing 15760 states (over memory cap)
KLEE: WARNING: killing 15278 states (over memory cap)
KLEE: WARNING: killing 15726 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: WARNING: killing 15605 states (over memory cap)
KLEE: WARNING: killing 15406 states (over memory cap)
KLEE: WARNING: killing 15759 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 15731 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15790 states (over memory cap)
KLEE: WARNING: killing 15678 states (over memory cap)
KLEE: WARNING: killing 15942 states (over memory cap)
KLEE: WARNING: killing 15924 states (over memory cap)
KLEE: WARNING: killing 15729 states (over memory cap)
KLEE: WARNING: killing 15709 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
KLEE: WARNING: killing 15587 states (over memory cap)
KLEE: WARNING: killing 16125 states (over memory cap)
KLEE: WARNING: killing 15920 states (over memory cap)
KLEE: WARNING: killing 16095 states (over memory cap)
KLEE: WARNING: killing 15621 states (over memory cap)
KLEE: WARNING: killing 15612 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 15391 states (over memory cap)
KLEE: WARNING: killing 15290 states (over memory cap)
KLEE: WARNING: killing 15547 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: WARNING: killing 15604 states (over memory cap)
KLEE: WARNING: killing 15317 states (over memory cap)
KLEE: WARNING: killing 15480 states (over memory cap)
KLEE: WARNING: killing 15647 states (over memory cap)
KLEE: WARNING: killing 16166 states (over memory cap)
KLEE: WARNING: killing 15521 states (over memory cap)
KLEE: WARNING: killing 15868 states (over memory cap)
KLEE: WARNING: killing 15674 states (over memory cap)
KLEE: WARNING: killing 16114 states (over memory cap)
KLEE: WARNING: killing 15653 states (over memory cap)
KLEE: WARNING: killing 15547 states (over memory cap)
KLEE: WARNING: killing 15803 states (over memory cap)
KLEE: WARNING: killing 15514 states (over memory cap)
KLEE: WARNING: killing 15140 states (over memory cap)
KLEE: WARNING: killing 15667 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:5739: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15471 states (over memory cap)
KLEE: WARNING: killing 15987 states (over memory cap)
KLEE: WARNING: killing 15527 states (over memory cap)
KLEE: WARNING: killing 15951 states (over memory cap)
KLEE: WARNING: killing 15580 states (over memory cap)
KLEE: WARNING: killing 15836 states (over memory cap)
KLEE: WARNING: killing 15912 states (over memory cap)
KLEE: WARNING: killing 15896 states (over memory cap)
KLEE: WARNING: killing 15619 states (over memory cap)
KLEE: WARNING: killing 15072 states (over memory cap)
KLEE: WARNING: killing 15670 states (over memory cap)
KLEE: WARNING: killing 15833 states (over memory cap)
KLEE: WARNING: killing 15815 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YfMlxB/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--dwc3--dwc3.ko-entry_point_false-unreach-call.cil.out.c:12987: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15438 states (over memory cap)
KLEE: WARNING: killing 15332 states (over memory cap)
KLEE: WARNING: killing 15403 states (over memory cap)
KLEE: WARNING: killing 15918 states (over memory cap)
KLEE: WARNING: killing 15817 states (over memory cap)
KLEE: WARNING: killing 15974 states (over memory cap)
KLEE: WARNING: killing 16136 states (over memory cap)
KLEE: WARNING: killing 15510 states (over memory cap)
KLEE: WARNING: killing 15759 states (over memory cap)
KLEE: WARNING: killing 15654 states (over memory cap)
KLEE: WARNING: killing 16167 states (over memory cap)
KLEE: WARNING: killing 16156 states (over memory cap)
KLEE: WARNING: killing 15788 states (over memory cap)
KLEE: WARNING: killing 15255 states (over memory cap)
KLEE: WARNING: killing 15326 states (over memory cap)
KLEE: WARNING: killing 16619 states (over memory cap)
KLEE: WARNING: killing 15559 states (over memory cap)
KLEE: WARNING: killing 15540 states (over memory cap)
KLEE: WARNING: killing 15705 states (over memory cap)
KLEE: WARNING: killing 15512 states (over memory cap)
KLEE: WARNING: killing 15321 states (over memory cap)
KLEE: WARNING: killing 15655 states (over memory cap)
KLEE: WARNING: killing 15555 states (over memory cap)
KLEE: WARNING: killing 15882 states (over memory cap)
KLEE: WARNING: killing 15954 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 15758 states (over memory cap)
KLEE: WARNING: killing 15922 states (over memory cap)
KLEE: WARNING: killing 15645 states (over memory cap)
KLEE: WARNING: killing 15801 states (over memory cap)
KLEE: WARNING: killing 15450 states (over memory cap)
KLEE: WARNING: killing 15944 states (over memory cap)
KLEE: WARNING: killing 15848 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 15643 states (over memory cap)
KLEE: WARNING: killing 15544 states (over memory cap)
KLEE: WARNING: killing 15539 states (over memory cap)
