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-43_2a-drivers--usb--host--oxu210hp-hcd.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.: 168 188 2122 14260
Removed infinite loop in ehci_quiesce
Removed infinite loop in qh_destroy
Removed infinite loop in start_unlink_async
Removed infinite loop in qh_update
Removed infinite loop in intr_submit
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.45393204689
Removed calls to 'dev_err' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'usb_remove_hcd' (function is undefined)
Removed calls to 'usb_put_hcd' (function is undefined)
Defining function usb_disabled as symbolic
Defining function platform_get_resource as symbolic
Defining function devm_ioremap_resource as symbolic
Defining function irq_set_irq_type as symbolic
Defining function usb_create_hcd as symbolic
Defining function usb_add_hcd as symbolic
Defining function device_wakeup_enable as symbolic
Defining function devm_kmalloc 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_hc_died' (function is undefined)
Removed calls to 'usb_hcd_poll_rh_status' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'msleep' (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 'schedule' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Defining function del_timer_sync as symbolic
Defining function mod_timer as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to 'usb_hcd_giveback_urb' (function is undefined)
Defining function scnprintf as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function usb_calc_bus_time as symbolic
Defining function __phys_addr as symbolic
Defining function del_timer 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_resume_2 as symbolic
Defining function ldv_suspend_2 as symbolic
Defining function __platform_driver_register as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  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: 0.511093854904
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 191 121 1049 7269
INFO: Starting verification
KLEE: WARNING ONCE: function "oxu_drv_probe" has inline asm
KLEE: WARNING ONCE: function "oxu_create" has inline asm
KLEE: WARNING ONCE: function "oxu_irq" has inline asm
KLEE: WARNING ONCE: function "oxu_reset" has inline asm
KLEE: WARNING ONCE: function "oxu_run" has inline asm
KLEE: WARNING ONCE: function "oxu_stop" has inline asm
KLEE: WARNING ONCE: function "oxu_shutdown" has inline asm
KLEE: WARNING ONCE: function "oxu_get_frame" has inline asm
KLEE: WARNING ONCE: function "oxu_hub_status_data" has inline asm
KLEE: WARNING ONCE: function "oxu_hub_control" has inline asm
KLEE: WARNING ONCE: function "oxu_bus_suspend" has inline asm
KLEE: WARNING ONCE: function "oxu_bus_resume" has inline asm
KLEE: WARNING ONCE: function "ehci_quiesce" has inline asm
KLEE: WARNING ONCE: function "ehci_work" has inline asm
KLEE: WARNING ONCE: function "ehci_halt" has inline asm
KLEE: WARNING ONCE: function "end_unlink_async" has inline asm
KLEE: WARNING ONCE: function "qh_get" has inline asm
KLEE: WARNING ONCE: function "qh_completions" has inline asm
KLEE: WARNING ONCE: function "qh_put" has inline asm
KLEE: WARNING ONCE: function "start_unlink_async" has inline asm
KLEE: WARNING ONCE: function "timer_action" has inline asm
KLEE: WARNING ONCE: function "intr_deschedule" has inline asm
KLEE: WARNING ONCE: function "qh_destroy" has inline asm
KLEE: WARNING ONCE: function "qh_refresh" has inline asm
KLEE: WARNING ONCE: function "qh_schedule" has inline asm
KLEE: WARNING ONCE: function "qh_link_async" has inline asm
KLEE: WARNING ONCE: function "__oxu_urb_enqueue" has inline asm
KLEE: WARNING ONCE: function "qh_append_tds" has inline asm
KLEE: WARNING ONCE: function "ehci_reset" has inline asm
KLEE: WARNING ONCE: function "oxu_watchdog" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6c74ff26-e01e-4c36-b9b9-45420f229c65/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8392: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8883: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8981: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4236: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9276: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4927: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8392: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:3993: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4792: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9300: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4245: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VcgQnl/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9366: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 8529 states (over memory cap)
KLEE: WARNING: killing 15260 states (over memory cap)
KLEE: WARNING: killing 15192 states (over memory cap)
KLEE: WARNING: killing 8041 states (over memory cap)
KLEE: WARNING: killing 14710 states (over memory cap)
KLEE: WARNING: killing 15131 states (over memory cap)
KLEE: WARNING: killing 8362 states (over memory cap)
KLEE: WARNING: killing 8035 states (over memory cap)
KLEE: WARNING: killing 15668 states (over memory cap)
KLEE: WARNING: killing 8627 states (over memory cap)
KLEE: WARNING: killing 8298 states (over memory cap)
KLEE: WARNING: killing 8209 states (over memory cap)
KLEE: WARNING: killing 8272 states (over memory cap)
KLEE: WARNING: killing 8102 states (over memory cap)
KLEE: WARNING: killing 8481 states (over memory cap)
KLEE: WARNING: killing 8161 states (over memory cap)
KLEE: WARNING: killing 8381 states (over memory cap)
KLEE: WARNING: killing 8449 states (over memory cap)
KLEE: WARNING: killing 8361 states (over memory cap)
KLEE: WARNING: killing 8272 states (over memory cap)
KLEE: WARNING: killing 8415 states (over memory cap)
KLEE: WARNING: killing 8175 states (over memory cap)
KLEE: WARNING: killing 15582 states (over memory cap)
KLEE: WARNING: killing 8296 states (over memory cap)
KLEE: WARNING: killing 8131 states (over memory cap)
KLEE: WARNING: killing 8349 states (over memory cap)
KLEE: WARNING: killing 7873 states (over memory cap)
KLEE: WARNING: killing 8167 states (over memory cap)
KLEE: WARNING: killing 8308 states (over memory cap)
KLEE: WARNING: killing 8222 states (over memory cap)
KLEE: WARNING: killing 8134 states (over memory cap)
KLEE: WARNING: killing 8201 states (over memory cap)
KLEE: WARNING: killing 8345 states (over memory cap)
KLEE: WARNING: killing 8181 states (over memory cap)
KLEE: WARNING: killing 8090 states (over memory cap)
KLEE: WARNING: killing 8083 states (over memory cap)
KLEE: WARNING: killing 8298 states (over memory cap)
KLEE: WARNING: killing 7908 states (over memory cap)
KLEE: WARNING: killing 8050 states (over memory cap)
KLEE: WARNING: killing 7963 states (over memory cap)
KLEE: WARNING: killing 8027 states (over memory cap)
KLEE: WARNING: killing 8090 states (over memory cap)
KLEE: WARNING: killing 8457 states (over memory cap)
KLEE: WARNING: killing 7920 states (over memory cap)
KLEE: WARNING: killing 8513 states (over memory cap)
KLEE: WARNING: killing 8729 states (over memory cap)
KLEE: WARNING: killing 8344 states (over memory cap)
KLEE: WARNING: killing 8333 states (over memory cap)
KLEE: WARNING: killing 8246 states (over memory cap)
KLEE: WARNING: killing 8013 states (over memory cap)
KLEE: WARNING: killing 8148 states (over memory cap)
KLEE: WARNING: killing 8063 states (over memory cap)
KLEE: WARNING: killing 8130 states (over memory cap)
KLEE: WARNING: killing 8046 states (over memory cap)
KLEE: WARNING: killing 8258 states (over memory cap)
KLEE: WARNING: killing 8469 states (over memory cap)
KLEE: WARNING: killing 7869 states (over memory cap)
KLEE: WARNING: killing 8377 states (over memory cap)
KLEE: WARNING: killing 8072 states (over memory cap)
KLEE: WARNING: killing 8283 states (over memory cap)
KLEE: WARNING: killing 8126 states (over memory cap)
KLEE: WARNING: killing 8339 states (over memory cap)
KLEE: WARNING: killing 8258 states (over memory cap)
KLEE: WARNING: killing 8177 states (over memory cap)
KLEE: WARNING: killing 8020 states (over memory cap)
KLEE: WARNING: killing 8377 states (over memory cap)
KLEE: WARNING: killing 8367 states (over memory cap)
KLEE: WARNING: killing 8209 states (over memory cap)
KLEE: WARNING: killing 8564 states (over memory cap)
KLEE: WARNING: killing 8189 states (over memory cap)
KLEE: WARNING: killing 8395 states (over memory cap)
KLEE: WARNING: killing 8389 states (over memory cap)
KLEE: WARNING: killing 8528 states (over memory cap)
KLEE: WARNING: killing 8080 states (over memory cap)
KLEE: WARNING: killing 8144 states (over memory cap)
KLEE: WARNING: killing 8281 states (over memory cap)
KLEE: WARNING: killing 7910 states (over memory cap)
KLEE: WARNING: killing 7824 states (over memory cap)
KLEE: WARNING: killing 8033 states (over memory cap)
KLEE: WARNING: killing 8315 states (over memory cap)
KLEE: WARNING: killing 8309 states (over memory cap)
KLEE: WARNING: killing 8011 states (over memory cap)
KLEE: WARNING: killing 8292 states (over memory cap)
KLEE: WARNING: killing 7924 states (over memory cap)
KLEE: WARNING: killing 8275 states (over memory cap)
KLEE: WARNING: killing 8192 states (over memory cap)
KLEE: WARNING: killing 8182 states (over memory cap)
KLEE: WARNING: killing 8318 states (over memory cap)
KLEE: WARNING: killing 8171 states (over memory cap)
KLEE: WARNING: killing 8518 states (over memory cap)
KLEE: WARNING: killing 8080 states (over memory cap)
KLEE: WARNING: killing 8357 states (over memory cap)
KLEE: WARNING: killing 8705 states (over memory cap)
KLEE: WARNING: killing 8415 states (over memory cap)
KLEE: WARNING: killing 7768 states (over memory cap)
KLEE: WARNING: killing 8044 states (over memory cap)
KLEE: WARNING: killing 8108 states (over memory cap)
KLEE: WARNING: killing 7884 states (over memory cap)
KLEE: WARNING: killing 8087 states (over memory cap)
KLEE: WARNING: killing 8366 states (over memory cap)
KLEE: WARNING: killing 8148 states (over memory cap)
KLEE: WARNING: killing 8282 states (over memory cap)
KLEE: WARNING: killing 8204 states (over memory cap)
KLEE: WARNING: killing 7910 states (over memory cap)
KLEE: WARNING: killing 8256 states (over memory cap)
KLEE: WARNING: killing 8313 states (over memory cap)
KLEE: WARNING: killing 8166 states (over memory cap)
KLEE: WARNING: killing 8157 states (over memory cap)
KLEE: WARNING: killing 8077 states (over memory cap)
KLEE: WARNING: killing 8139 states (over memory cap)
KLEE: WARNING: killing 8275 states (over memory cap)
KLEE: WARNING: killing 8336 states (over memory cap)
KLEE: WARNING: killing 8262 states (over memory cap)
KLEE: WARNING: killing 8255 states (over memory cap)
KLEE: WARNING: killing 8107 states (over memory cap)
KLEE: WARNING: killing 8307 states (over memory cap)
KLEE: WARNING: killing 8371 states (over memory cap)
KLEE: WARNING: killing 8084 states (over memory cap)
KLEE: WARNING: killing 8077 states (over memory cap)
KLEE: WARNING: killing 8347 states (over memory cap)
KLEE: WARNING: killing 8064 states (over memory cap)
KLEE: WARNING: killing 7919 states (over memory cap)
KLEE: WARNING: killing 8325 states (over memory cap)
KLEE: WARNING: killing 7835 states (over memory cap)
KLEE: WARNING: killing 7822 states (over memory cap)
KLEE: WARNING: killing 8232 states (over memory cap)
KLEE: WARNING: killing 8020 states (over memory cap)
KLEE: WARNING: killing 7868 states (over memory cap)
KLEE: WARNING: killing 8138 states (over memory cap)
