bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-commit-tester/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.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.: 201 92 947 6537
Removed infinite loop in vhci_urb_enqueue
Removed infinite loop in show_status
INFO: Compilation, preparation and instrumentation time: 0.40976190567
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function sscanf as symbolic
Defining function printk as symbolic
Defining function sockfd_to_socket as symbolic
Defining function usbip_start_threads as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'usb_hcd_poll_rh_status' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'usb_put_hcd' (function is undefined)
Removed calls to 'usb_remove_hcd' (function is undefined)
Defining function dev_printk as symbolic
Defining function dev_get_drvdata as symbolic
Defining function _dev_info as symbolic
Defining function usb_create_hcd as symbolic
Defining function usb_add_hcd as symbolic
Removed calls to 'usbip_task_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'usbip_event_add' (function is undefined)
Removed calls to 'usbip_stop_eh' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '__wake_up' (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 'list_del' (function is undefined)
Removed calls to 'usb_hcd_resume_root_hub' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function usb_hcd_check_unlink_urb as symbolic
Defining function dev_err as symbolic
Defining function usb_hcd_link_urb_to_ep as symbolic
Removed calls to 'usb_put_dev' (function is undefined)
Defining function usb_get_dev as symbolic
Defining function sysfs_create_group as symbolic
Removed calls to 'usbip_header_correct_endian' (function is undefined)
Removed calls to 'usbip_dump_header' (function is undefined)
Removed calls to 'usbip_pack_pdu' (function is undefined)
Removed calls to 'usbip_dump_urb' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'usbip_stop_threads' (function is undefined)
Removed calls to 'sock_release' (function is undefined)
Defining function usbip_start_eh as symbolic
Defining function kernel_sock_shutdown as symbolic
Defining function autoremove_wake_function as symbolic
Defining function kernel_sendmsg as symbolic
Defining function usbip_alloc_iso_desc_pdu as symbolic
Defining function usbip_event_happened as symbolic
Defining function usbip_xmit as symbolic
Defining function usbip_recv_xbuff as symbolic
Defining function usbip_recv_iso as symbolic
Defining function sprintf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Defining function usb_disabled as symbolic
Defining function platform_driver_register as symbolic
Defining function platform_device_register as symbolic
Defining function strlen as symbolic
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: 0.387709140778
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 275 81 577 4041
INFO: Starting verification
KLEE: WARNING ONCE: function "store_attach" has inline asm
KLEE: WARNING ONCE: function "rh_port_connect" has inline asm
KLEE: WARNING ONCE: function "vhci_hcd_probe" has inline asm
KLEE: WARNING ONCE: function "vhci_hcd_suspend" has inline asm
KLEE: WARNING ONCE: function "vhci_hcd_resume" has inline asm
KLEE: WARNING ONCE: function "vhci_start" has inline asm
KLEE: WARNING ONCE: function "vhci_stop" has inline asm
KLEE: WARNING ONCE: function "vhci_get_frame_number" has inline asm
KLEE: WARNING ONCE: function "vhci_urb_enqueue" has inline asm
KLEE: WARNING ONCE: function "vhci_urb_dequeue" has inline asm
KLEE: WARNING ONCE: function "vhci_hub_status" has inline asm
KLEE: WARNING ONCE: function "vhci_hub_control" has inline asm
KLEE: WARNING ONCE: function "vhci_shutdown_connection" has inline asm
KLEE: WARNING ONCE: function "rh_port_disconnect" has inline asm
KLEE: WARNING ONCE: function "store_detach" has inline asm
KLEE: WARNING ONCE: function "show_status" has inline asm
KLEE: WARNING ONCE: function "vhci_rx_loop" has inline asm
KLEE: WARNING ONCE: function "pickup_urb_and_free_priv" has inline asm
KLEE: WARNING ONCE: function "vhci_tx_loop" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:4752: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:4752: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9568 bytes on read, may be slow and/or crash: MO46[9568] allocated at global:
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7309: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7862: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7844: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:6573: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7913: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:6729: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:6729: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:6871: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7461: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7847: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7865: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:4752: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:6733: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7328: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:4795: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7476: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7477: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:6754: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:4752: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7034: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7034: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7868: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:7919: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2BTgMd/main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c:4752: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
