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-08_1a-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 183 2128 14313
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
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.466288089752
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 _raw_spin_lock_irqsave as symbolic
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)
Defining function ldv_resume_2 as symbolic
Defining function ldv_suspend_2 as symbolic
Defining function __platform_driver_register as symbolic
Linked our definitions to these undefined functions:
  __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: 0.519253969193
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 189 120 1048 7224
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_2ecff437-b98c-451d-969e-2972434961e2/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9009: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8911: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9304: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8416: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9328: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4122: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4806: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8416: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:3883: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8540: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4131: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 8313 states (over memory cap)
KLEE: WARNING: killing 15688 states (over memory cap)
KLEE: WARNING: killing 15536 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-vp43pu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15557 states (over memory cap)
KLEE: WARNING: killing 15579 states (over memory cap)
KLEE: WARNING: killing 8324 states (over memory cap)
KLEE: WARNING: killing 8306 states (over memory cap)
KLEE: WARNING: killing 8134 states (over memory cap)
KLEE: WARNING: killing 8200 states (over memory cap)
KLEE: WARNING: killing 8186 states (over memory cap)
KLEE: WARNING: killing 8254 states (over memory cap)
KLEE: WARNING: killing 8400 states (over memory cap)
KLEE: WARNING: killing 15908 states (over memory cap)
KLEE: WARNING: killing 8681 states (over memory cap)
KLEE: WARNING: killing 8267 states (over memory cap)
KLEE: WARNING: killing 8179 states (over memory cap)
KLEE: WARNING: killing 8323 states (over memory cap)
KLEE: WARNING: killing 7991 states (over memory cap)
KLEE: WARNING: killing 8534 states (over memory cap)
KLEE: WARNING: killing 8446 states (over memory cap)
KLEE: WARNING: killing 8750 states (over memory cap)
KLEE: WARNING: killing 8264 states (over memory cap)
KLEE: WARNING: killing 8330 states (over memory cap)
KLEE: WARNING: killing 8318 states (over memory cap)
KLEE: WARNING: killing 8069 states (over memory cap)
KLEE: WARNING: killing 8217 states (over memory cap)
KLEE: WARNING: killing 8363 states (over memory cap)
KLEE: WARNING: killing 8506 states (over memory cap)
KLEE: WARNING: killing 8420 states (over memory cap)
KLEE: WARNING: killing 8408 states (over memory cap)
KLEE: WARNING: killing 7924 states (over memory cap)
KLEE: WARNING: killing 8301 states (over memory cap)
KLEE: WARNING: killing 8214 states (over memory cap)
KLEE: WARNING: killing 8204 states (over memory cap)
KLEE: WARNING: killing 8265 states (over memory cap)
KLEE: WARNING: killing 8176 states (over memory cap)
KLEE: WARNING: killing 8244 states (over memory cap)
KLEE: WARNING: killing 8155 states (over memory cap)
KLEE: WARNING: killing 8375 states (over memory cap)
KLEE: WARNING: killing 8212 states (over memory cap)
KLEE: WARNING: killing 8353 states (over memory cap)
KLEE: WARNING: killing 8417 states (over memory cap)
KLEE: WARNING: killing 8407 states (over memory cap)
KLEE: WARNING: killing 8167 states (over memory cap)
KLEE: WARNING: killing 8543 states (over memory cap)
KLEE: WARNING: killing 8301 states (over memory cap)
KLEE: WARNING: killing 8212 states (over memory cap)
KLEE: WARNING: killing 8435 states (over memory cap)
KLEE: WARNING: killing 8040 states (over memory cap)
KLEE: WARNING: killing 8258 states (over memory cap)
KLEE: WARNING: killing 8095 states (over memory cap)
KLEE: WARNING: killing 8163 states (over memory cap)
KLEE: WARNING: killing 8154 states (over memory cap)
KLEE: WARNING: killing 7689 states (over memory cap)
KLEE: WARNING: killing 8284 states (over memory cap)
KLEE: WARNING: killing 8427 states (over memory cap)
KLEE: WARNING: killing 8340 states (over memory cap)
KLEE: WARNING: killing 8179 states (over memory cap)
KLEE: WARNING: killing 8169 states (over memory cap)
KLEE: WARNING: killing 8009 states (over memory cap)
KLEE: WARNING: killing 7850 states (over memory cap)
KLEE: WARNING: killing 8518 states (over memory cap)
KLEE: WARNING: killing 8133 states (over memory cap)
KLEE: WARNING: killing 8124 states (over memory cap)
KLEE: WARNING: killing 8266 states (over memory cap)
KLEE: WARNING: killing 8181 states (over memory cap)
KLEE: WARNING: killing 8322 states (over memory cap)
KLEE: WARNING: killing 8239 states (over memory cap)
KLEE: WARNING: killing 8160 states (over memory cap)
KLEE: WARNING: killing 8078 states (over memory cap)
KLEE: WARNING: killing 8367 states (over memory cap)
KLEE: WARNING: killing 8503 states (over memory cap)
KLEE: WARNING: killing 8126 states (over memory cap)
KLEE: WARNING: killing 8264 states (over memory cap)
KLEE: WARNING: killing 8036 states (over memory cap)
KLEE: WARNING: killing 8547 states (over memory cap)
KLEE: WARNING: killing 8389 states (over memory cap)
KLEE: WARNING: killing 8161 states (over memory cap)
KLEE: WARNING: killing 8371 states (over memory cap)
KLEE: WARNING: killing 7846 states (over memory cap)
KLEE: WARNING: killing 8500 states (over memory cap)
KLEE: WARNING: killing 7680 states (over memory cap)
KLEE: WARNING: killing 8189 states (over memory cap)
KLEE: WARNING: killing 8180 states (over memory cap)
KLEE: WARNING: killing 8024 states (over memory cap)
KLEE: WARNING: killing 7944 states (over memory cap)
KLEE: WARNING: killing 8520 states (over memory cap)
KLEE: WARNING: killing 8000 states (over memory cap)
KLEE: WARNING: killing 8210 states (over memory cap)
KLEE: WARNING: killing 8423 states (over memory cap)
KLEE: WARNING: killing 8487 states (over memory cap)
KLEE: WARNING: killing 8264 states (over memory cap)
KLEE: WARNING: killing 8400 states (over memory cap)
KLEE: WARNING: killing 8173 states (over memory cap)
KLEE: WARNING: killing 8239 states (over memory cap)
KLEE: WARNING: killing 8088 states (over memory cap)
KLEE: WARNING: killing 8223 states (over memory cap)
KLEE: WARNING: killing 8071 states (over memory cap)
KLEE: WARNING: killing 8278 states (over memory cap)
KLEE: WARNING: killing 8122 states (over memory cap)
KLEE: WARNING: killing 8188 states (over memory cap)
KLEE: WARNING: killing 8252 states (over memory cap)
KLEE: WARNING: killing 8100 states (over memory cap)
KLEE: WARNING: killing 7874 states (over memory cap)
KLEE: WARNING: killing 7723 states (over memory cap)
KLEE: WARNING: killing 8291 states (over memory cap)
KLEE: WARNING: killing 8281 states (over memory cap)
KLEE: WARNING: killing 8418 states (over memory cap)
KLEE: WARNING: killing 8054 states (over memory cap)
KLEE: WARNING: killing 7974 states (over memory cap)
KLEE: WARNING: killing 8108 states (over memory cap)
KLEE: WARNING: killing 8388 states (over memory cap)
KLEE: WARNING: killing 8523 states (over memory cap)
KLEE: WARNING: killing 8157 states (over memory cap)
KLEE: WARNING: killing 8225 states (over memory cap)
KLEE: WARNING: killing 8288 states (over memory cap)
KLEE: WARNING: killing 8139 states (over memory cap)
KLEE: WARNING: killing 8269 states (over memory cap)
KLEE: WARNING: killing 8121 states (over memory cap)
KLEE: WARNING: killing 8182 states (over memory cap)
KLEE: WARNING: killing 8107 states (over memory cap)
KLEE: WARNING: killing 8453 states (over memory cap)
KLEE: WARNING: killing 8228 states (over memory cap)
KLEE: WARNING: killing 8079 states (over memory cap)
KLEE: WARNING: killing 8567 states (over memory cap)
KLEE: WARNING: killing 8066 states (over memory cap)
KLEE: WARNING: killing 8341 states (over memory cap)
KLEE: WARNING: killing 8617 states (over memory cap)
KLEE: WARNING: killing 8189 states (over memory cap)
KLEE: WARNING: killing 8392 states (over memory cap)
KLEE: WARNING: killing 8245 states (over memory cap)
KLEE: WARNING: killing 8308 states (over memory cap)
KLEE: WARNING: killing 8442 states (over memory cap)
KLEE: WARNING: killing 8153 states (over memory cap)
KLEE: WARNING: killing 8076 states (over memory cap)
KLEE: WARNING: killing 7998 states (over memory cap)
KLEE: WARNING: killing 8267 states (over memory cap)
KLEE: WARNING: killing 8047 states (over memory cap)
KLEE: WARNING: killing 8388 states (over memory cap)
KLEE: WARNING: killing 8097 states (over memory cap)
KLEE: WARNING: killing 8025 states (over memory cap)
KLEE: WARNING: killing 8156 states (over memory cap)
KLEE: WARNING: killing 8146 states (over memory cap)
KLEE: WARNING: killing 8280 states (over memory cap)
KLEE: WARNING: killing 8205 states (over memory cap)
KLEE: WARNING: killing 8269 states (over memory cap)
KLEE: WARNING: killing 7980 states (over memory cap)
KLEE: WARNING: killing 8182 states (over memory cap)
KLEE: WARNING: killing 8313 states (over memory cap)
KLEE: WARNING: killing 7890 states (over memory cap)
KLEE: WARNING: killing 8227 states (over memory cap)
KLEE: WARNING: killing 8214 states (over memory cap)
KLEE: WARNING: killing 8074 states (over memory cap)
KLEE: WARNING: killing 8133 states (over memory cap)
KLEE: WARNING: killing 8469 states (over memory cap)
KLEE: WARNING: killing 8603 states (over memory cap)
KLEE: WARNING: killing 8387 states (over memory cap)
KLEE: WARNING: killing 7829 states (over memory cap)
KLEE: WARNING: killing 8093 states (over memory cap)
KLEE: WARNING: killing 8154 states (over memory cap)
KLEE: WARNING: killing 7872 states (over memory cap)
KLEE: WARNING: killing 8276 states (over memory cap)
KLEE: WARNING: killing 8749 states (over memory cap)
KLEE: WARNING: killing 8197 states (over memory cap)
KLEE: WARNING: killing 8189 states (over memory cap)
KLEE: WARNING: killing 8252 states (over memory cap)
KLEE: WARNING: killing 8315 states (over memory cap)
KLEE: WARNING: killing 8371 states (over memory cap)
KLEE: WARNING: killing 8367 states (over memory cap)
KLEE: WARNING: killing 8158 states (over memory cap)
KLEE: WARNING: killing 8149 states (over memory cap)
KLEE: WARNING: killing 8074 states (over memory cap)
KLEE: WARNING: killing 8132 states (over memory cap)
KLEE: WARNING: killing 7926 states (over memory cap)
KLEE: WARNING: killing 8120 states (over memory cap)
KLEE: WARNING: killing 8042 states (over memory cap)
KLEE: WARNING: killing 8377 states (over memory cap)
KLEE: WARNING: killing 8162 states (over memory cap)
KLEE: WARNING: killing 8024 states (over memory cap)
KLEE: WARNING: killing 8352 states (over memory cap)
KLEE: WARNING: killing 8413 states (over memory cap)
KLEE: WARNING: killing 8204 states (over memory cap)
KLEE: WARNING: killing 8065 states (over memory cap)
KLEE: WARNING: killing 8394 states (over memory cap)
KLEE: WARNING: killing 8184 states (over memory cap)
KLEE: WARNING: killing 8243 states (over memory cap)
KLEE: WARNING: killing 8105 states (over memory cap)
KLEE: WARNING: killing 8164 states (over memory cap)
KLEE: WARNING: killing 8156 states (over memory cap)
KLEE: WARNING: killing 8079 states (over memory cap)
KLEE: WARNING: killing 8137 states (over memory cap)
KLEE: WARNING: killing 8129 states (over memory cap)
KLEE: WARNING: killing 7919 states (over memory cap)
KLEE: WARNING: killing 8314 states (over memory cap)
KLEE: WARNING: killing 8040 states (over memory cap)
KLEE: WARNING: killing 8164 states (over memory cap)
KLEE: WARNING: killing 8292 states (over memory cap)
KLEE: WARNING: killing 8220 states (over memory cap)
KLEE: WARNING: killing 8277 states (over memory cap)
KLEE: WARNING: killing 8201 states (over memory cap)
KLEE: WARNING: killing 8394 states (over memory cap)
KLEE: WARNING: killing 8321 states (over memory cap)
KLEE: WARNING: killing 7920 states (over memory cap)
KLEE: WARNING: killing 8307 states (over memory cap)
