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--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.: 170 219 2273 14864
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.57919716835
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
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock 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.626120090485
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 191 157 1185 7601
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_72d53fec-64c6-4169-b4f3-d0969556f1fa/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8426: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9019: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8921: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4239: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8550: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:8426: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4816: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9314: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:3876: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9338: 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 9149 states (over memory cap)
KLEE: WARNING: killing 15287 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:4248: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15803 states (over memory cap)
KLEE: WARNING: killing 15327 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 8173 states (over memory cap)
KLEE: WARNING: killing 15349 states (over memory cap)
KLEE: WARNING: killing 8369 states (over memory cap)
KLEE: WARNING: killing 8273 states (over memory cap)
KLEE: WARNING: killing 8260 states (over memory cap)
KLEE: WARNING: killing 8086 states (over memory cap)
KLEE: WARNING: killing 15929 states (over memory cap)
KLEE: WARNING: killing 8694 states (over memory cap)
KLEE: WARNING: killing 8359 states (over memory cap)
KLEE: WARNING: killing 8345 states (over memory cap)
KLEE: WARNING: killing 8494 states (over memory cap)
KLEE: WARNING: killing 8321 states (over memory cap)
KLEE: WARNING: killing 8230 states (over memory cap)
KLEE: WARNING: killing 8141 states (over memory cap)
KLEE: WARNING: killing 8523 states (over memory cap)
KLEE: WARNING: killing 8276 states (over memory cap)
KLEE: WARNING: killing 8026 states (over memory cap)
KLEE: WARNING: killing 8330 states (over memory cap)
KLEE: WARNING: killing 8315 states (over memory cap)
KLEE: WARNING: killing 8228 states (over memory cap)
KLEE: WARNING: killing 8136 states (over memory cap)
KLEE: WARNING: killing 8282 states (over memory cap)
KLEE: WARNING: killing 8271 states (over memory cap)
KLEE: WARNING: killing 8180 states (over memory cap)
KLEE: WARNING: killing 8324 states (over memory cap)
KLEE: WARNING: killing 8002 states (over memory cap)
KLEE: WARNING: killing 8303 states (over memory cap)
KLEE: WARNING: killing 8055 states (over memory cap)
KLEE: WARNING: killing 8047 states (over memory cap)
KLEE: WARNING: killing 8112 states (over memory cap)
KLEE: WARNING: killing 8178 states (over memory cap)
KLEE: WARNING: killing 8398 states (over memory cap)
KLEE: WARNING: killing 8235 states (over memory cap)
KLEE: WARNING: killing 8301 states (over memory cap)
KLEE: WARNING: killing 8059 states (over memory cap)
KLEE: WARNING: killing 8122 states (over memory cap)
KLEE: WARNING: killing 8191 states (over memory cap)
KLEE: WARNING: killing 8257 states (over memory cap)
KLEE: WARNING: killing 8710 states (over memory cap)
KLEE: WARNING: killing 8009 states (over memory cap)
KLEE: WARNING: killing 8455 states (over memory cap)
KLEE: WARNING: killing 8216 states (over memory cap)
KLEE: WARNING: killing 8209 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-lyt8q_/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--oxu210hp-hcd.ko-entry_point_true-unreach-call.cil.out.c:9404: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7967 states (over memory cap)
KLEE: WARNING: killing 8414 states (over memory cap)
KLEE: WARNING: killing 8327 states (over memory cap)
KLEE: WARNING: killing 8090 states (over memory cap)
KLEE: WARNING: killing 8155 states (over memory cap)
KLEE: WARNING: killing 7842 states (over memory cap)
KLEE: WARNING: killing 8357 states (over memory cap)
KLEE: WARNING: killing 8120 states (over memory cap)
KLEE: WARNING: killing 8191 states (over memory cap)
KLEE: WARNING: killing 8104 states (over memory cap)
KLEE: WARNING: killing 7943 states (over memory cap)
KLEE: WARNING: killing 8389 states (over memory cap)
KLEE: WARNING: killing 8230 states (over memory cap)
KLEE: WARNING: killing 7920 states (over memory cap)
KLEE: WARNING: killing 8287 states (over memory cap)
KLEE: WARNING: killing 8351 states (over memory cap)
KLEE: WARNING: killing 8418 states (over memory cap)
KLEE: WARNING: killing 8412 states (over memory cap)
KLEE: WARNING: killing 8332 states (over memory cap)
KLEE: WARNING: killing 7947 states (over memory cap)
KLEE: WARNING: killing 8235 states (over memory cap)
KLEE: WARNING: killing 8151 states (over memory cap)
KLEE: WARNING: killing 7919 states (over memory cap)
KLEE: WARNING: killing 8284 states (over memory cap)
KLEE: WARNING: killing 8125 states (over memory cap)
KLEE: WARNING: killing 8261 states (over memory cap)
KLEE: WARNING: killing 8549 states (over memory cap)
KLEE: WARNING: killing 8020 states (over memory cap)
KLEE: WARNING: killing 8089 states (over memory cap)
KLEE: WARNING: killing 8304 states (over memory cap)
KLEE: WARNING: killing 8439 states (over memory cap)
KLEE: WARNING: killing 8506 states (over memory cap)
KLEE: WARNING: killing 8128 states (over memory cap)
KLEE: WARNING: killing 8342 states (over memory cap)
KLEE: WARNING: killing 8187 states (over memory cap)
KLEE: WARNING: killing 8621 states (over memory cap)
KLEE: WARNING: killing 8244 states (over memory cap)
KLEE: WARNING: killing 8384 states (over memory cap)
KLEE: WARNING: killing 8008 states (over memory cap)
KLEE: WARNING: killing 7929 states (over memory cap)
KLEE: WARNING: killing 8139 states (over memory cap)
KLEE: WARNING: killing 8349 states (over memory cap)
KLEE: WARNING: killing 7978 states (over memory cap)
KLEE: WARNING: killing 8191 states (over memory cap)
KLEE: WARNING: killing 7963 states (over memory cap)
KLEE: WARNING: killing 8170 states (over memory cap)
KLEE: WARNING: killing 7872 states (over memory cap)
KLEE: WARNING: killing 8081 states (over memory cap)
KLEE: WARNING: killing 8289 states (over memory cap)
KLEE: WARNING: killing 8283 states (over memory cap)
KLEE: WARNING: killing 7840 states (over memory cap)
KLEE: WARNING: killing 8480 states (over memory cap)
KLEE: WARNING: killing 8401 states (over memory cap)
KLEE: WARNING: killing 8036 states (over memory cap)
KLEE: WARNING: killing 8101 states (over memory cap)
KLEE: WARNING: killing 8526 states (over memory cap)
KLEE: WARNING: killing 8087 states (over memory cap)
KLEE: WARNING: killing 8154 states (over memory cap)
KLEE: WARNING: killing 8146 states (over memory cap)
KLEE: WARNING: killing 8208 states (over memory cap)
KLEE: WARNING: killing 8203 states (over memory cap)
KLEE: WARNING: killing 8121 states (over memory cap)
KLEE: WARNING: killing 8259 states (over memory cap)
KLEE: WARNING: killing 8033 states (over memory cap)
KLEE: WARNING: killing 8386 states (over memory cap)
KLEE: WARNING: killing 8308 states (over memory cap)
KLEE: WARNING: killing 8085 states (over memory cap)
KLEE: WARNING: killing 7933 states (over memory cap)
KLEE: WARNING: killing 8068 states (over memory cap)
KLEE: WARNING: killing 8276 states (over memory cap)
KLEE: WARNING: killing 8271 states (over memory cap)
KLEE: WARNING: killing 8337 states (over memory cap)
KLEE: WARNING: killing 7974 states (over memory cap)
KLEE: WARNING: killing 8249 states (over memory cap)
KLEE: WARNING: killing 8095 states (over memory cap)
KLEE: WARNING: killing 8163 states (over memory cap)
KLEE: WARNING: killing 8085 states (over memory cap)
KLEE: WARNING: killing 7933 states (over memory cap)
KLEE: WARNING: killing 8278 states (over memory cap)
KLEE: WARNING: killing 8276 states (over memory cap)
KLEE: WARNING: killing 8336 states (over memory cap)
KLEE: WARNING: killing 8753 states (over memory cap)
KLEE: WARNING: killing 8183 states (over memory cap)
KLEE: WARNING: killing 7960 states (over memory cap)
KLEE: WARNING: killing 8304 states (over memory cap)
KLEE: WARNING: killing 8156 states (over memory cap)
KLEE: WARNING: killing 8288 states (over memory cap)
KLEE: WARNING: killing 8142 states (over memory cap)
KLEE: WARNING: killing 8413 states (over memory cap)
KLEE: WARNING: killing 8055 states (over memory cap)
KLEE: WARNING: killing 8046 states (over memory cap)
KLEE: WARNING: killing 7831 states (over memory cap)
KLEE: WARNING: killing 8239 states (over memory cap)
KLEE: WARNING: killing 8302 states (over memory cap)
KLEE: WARNING: killing 8223 states (over memory cap)
KLEE: WARNING: killing 8216 states (over memory cap)
KLEE: WARNING: killing 8281 states (over memory cap)
KLEE: WARNING: killing 8132 states (over memory cap)
KLEE: WARNING: killing 8124 states (over memory cap)
KLEE: WARNING: killing 8050 states (over memory cap)
KLEE: WARNING: killing 8250 states (over memory cap)
KLEE: WARNING: killing 8102 states (over memory cap)
KLEE: WARNING: killing 8305 states (over memory cap)
KLEE: WARNING: killing 8296 states (over memory cap)
KLEE: WARNING: killing 8013 states (over memory cap)
KLEE: WARNING: killing 8207 states (over memory cap)
KLEE: WARNING: killing 7853 states (over memory cap)
KLEE: WARNING: killing 8055 states (over memory cap)
KLEE: WARNING: killing 8320 states (over memory cap)
KLEE: WARNING: killing 8245 states (over memory cap)
KLEE: WARNING: killing 8240 states (over memory cap)
KLEE: WARNING: killing 8370 states (over memory cap)
KLEE: WARNING: killing 8432 states (over memory cap)
KLEE: WARNING: killing 8423 states (over memory cap)
KLEE: WARNING: killing 7939 states (over memory cap)
KLEE: WARNING: killing 8407 states (over memory cap)
KLEE: WARNING: killing 8403 states (over memory cap)
KLEE: WARNING: killing 8258 states (over memory cap)
KLEE: WARNING: killing 8044 states (over memory cap)
KLEE: WARNING: killing 7901 states (over memory cap)
KLEE: WARNING: killing 8100 states (over memory cap)
KLEE: WARNING: killing 8428 states (over memory cap)
KLEE: WARNING: killing 8284 states (over memory cap)
KLEE: WARNING: killing 7937 states (over memory cap)
KLEE: WARNING: killing 8064 states (over memory cap)
KLEE: WARNING: killing 7855 states (over memory cap)
KLEE: WARNING: killing 8116 states (over memory cap)
KLEE: WARNING: killing 8452 states (over memory cap)
KLEE: WARNING: killing 8174 states (over memory cap)
KLEE: WARNING: killing 8368 states (over memory cap)
KLEE: WARNING: killing 8158 states (over memory cap)
KLEE: WARNING: killing 8422 states (over memory cap)
KLEE: WARNING: killing 8077 states (over memory cap)
KLEE: WARNING: killing 8140 states (over memory cap)
