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--misc--ftdi-elan.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.: 154 296 2012 13741
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.472290992737
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'usb_put_dev' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function sprintf as symbolic
Defining function no_llseek as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function usb_find_interface as symbolic
Defining function printk as symbolic
Defining function down_interruptible as symbolic
Defining function usb_alloc_urb as symbolic
Defining function usb_alloc_coherent as symbolic
Defining function usb_submit_urb as symbolic
Defining function _copy_from_user as symbolic
Defining function usb_bulk_msg as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'usb_deregister_dev' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to 'down' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Defining function cancel_delayed_work as symbolic
Defining function usb_get_dev as symbolic
Defining function usb_register_dev as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function usb_register_driver as symbolic
Defining function queue_work_on as symbolic
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.540552139282
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 172 252 1274 6904
INFO: Starting verification
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_e3cfbc80-0d83-4827-a843-6a43a07b8fc1/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wya2nJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:5929: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wya2nJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:5110: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wya2nJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:3652: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12482 states (over memory cap)
KLEE: WARNING: killing 16112 states (over memory cap)
KLEE: WARNING: killing 16242 states (over memory cap)
KLEE: WARNING: killing 16469 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wya2nJ/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:8304: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16704 states (over memory cap)
KLEE: WARNING: killing 16448 states (over memory cap)
KLEE: WARNING: killing 16977 states (over memory cap)
KLEE: WARNING: killing 17414 states (over memory cap)
KLEE: WARNING: killing 17845 states (over memory cap)
KLEE: WARNING: killing 17595 states (over memory cap)
KLEE: WARNING: killing 17747 states (over memory cap)
KLEE: WARNING: killing 17881 states (over memory cap)
KLEE: WARNING: killing 18031 states (over memory cap)
KLEE: WARNING: killing 18080 states (over memory cap)
KLEE: WARNING: killing 17555 states (over memory cap)
KLEE: WARNING: killing 17501 states (over memory cap)
KLEE: WARNING: killing 17072 states (over memory cap)
KLEE: WARNING: killing 17696 states (over memory cap)
KLEE: WARNING: killing 17363 states (over memory cap)
KLEE: WARNING: killing 17128 states (over memory cap)
KLEE: WARNING: killing 17553 states (over memory cap)
KLEE: WARNING: killing 17227 states (over memory cap)
KLEE: WARNING: killing 17276 states (over memory cap)
KLEE: WARNING: killing 17132 states (over memory cap)
KLEE: WARNING: killing 17371 states (over memory cap)
KLEE: WARNING: killing 16860 states (over memory cap)
KLEE: WARNING: killing 16815 states (over memory cap)
KLEE: WARNING: killing 17144 states (over memory cap)
KLEE: WARNING: killing 17568 states (over memory cap)
KLEE: WARNING: killing 9254 states (over memory cap)
KLEE: WARNING: killing 16404 states (over memory cap)
KLEE: WARNING: killing 9315 states (over memory cap)
KLEE: WARNING: killing 16902 states (over memory cap)
KLEE: WARNING: killing 16960 states (over memory cap)
KLEE: WARNING: killing 9355 states (over memory cap)
KLEE: WARNING: killing 17093 states (over memory cap)
KLEE: WARNING: killing 17143 states (over memory cap)
KLEE: WARNING: killing 9303 states (over memory cap)
KLEE: WARNING: killing 17546 states (over memory cap)
KLEE: WARNING: killing 9271 states (over memory cap)
KLEE: WARNING: killing 17040 states (over memory cap)
KLEE: WARNING: killing 9421 states (over memory cap)
KLEE: WARNING: killing 17069 states (over memory cap)
KLEE: WARNING: killing 16936 states (over memory cap)
KLEE: WARNING: killing 9012 states (over memory cap)
KLEE: WARNING: killing 16888 states (over memory cap)
KLEE: WARNING: killing 9069 states (over memory cap)
KLEE: WARNING: killing 16835 states (over memory cap)
KLEE: WARNING: killing 9490 states (over memory cap)
KLEE: WARNING: killing 16782 states (over memory cap)
KLEE: WARNING: killing 9371 states (over memory cap)
KLEE: WARNING: killing 16555 states (over memory cap)
KLEE: WARNING: killing 8900 states (over memory cap)
KLEE: WARNING: killing 16860 states (over memory cap)
KLEE: WARNING: killing 9227 states (over memory cap)
KLEE: WARNING: killing 9130 states (over memory cap)
KLEE: WARNING: killing 16801 states (over memory cap)
KLEE: WARNING: killing 9368 states (over memory cap)
KLEE: WARNING: killing 16566 states (over memory cap)
KLEE: WARNING: killing 8986 states (over memory cap)
KLEE: WARNING: killing 16520 states (over memory cap)
KLEE: WARNING: killing 9223 states (over memory cap)
KLEE: WARNING: killing 16736 states (over memory cap)
KLEE: WARNING: killing 9108 states (over memory cap)
KLEE: WARNING: killing 9103 states (over memory cap)
KLEE: WARNING: killing 8744 states (over memory cap)
KLEE: WARNING: killing 16405 states (over memory cap)
KLEE: WARNING: killing 9500 states (over memory cap)
KLEE: WARNING: killing 8712 states (over memory cap)
KLEE: WARNING: killing 16861 states (over memory cap)
KLEE: WARNING: killing 9205 states (over memory cap)
KLEE: WARNING: killing 8762 states (over memory cap)
KLEE: WARNING: killing 8665 states (over memory cap)
KLEE: WARNING: killing 16425 states (over memory cap)
KLEE: WARNING: killing 9244 states (over memory cap)
KLEE: WARNING: killing 16726 states (over memory cap)
KLEE: WARNING: killing 9217 states (over memory cap)
KLEE: WARNING: killing 16243 states (over memory cap)
KLEE: WARNING: killing 9529 states (over memory cap)
KLEE: WARNING: killing 16545 states (over memory cap)
KLEE: WARNING: killing 9075 states (over memory cap)
KLEE: WARNING: killing 16665 states (over memory cap)
KLEE: WARNING: killing 9562 states (over memory cap)
KLEE: WARNING: killing 8701 states (over memory cap)
KLEE: WARNING: killing 8696 states (over memory cap)
KLEE: WARNING: killing 8602 states (over memory cap)
KLEE: WARNING: killing 8762 states (over memory cap)
KLEE: WARNING: killing 8671 states (over memory cap)
KLEE: WARNING: killing 8748 states (over memory cap)
KLEE: WARNING: killing 8657 states (over memory cap)
KLEE: WARNING: killing 8819 states (over memory cap)
KLEE: WARNING: killing 8559 states (over memory cap)
KLEE: WARNING: killing 8634 states (over memory cap)
KLEE: WARNING: killing 8708 states (over memory cap)
KLEE: WARNING: killing 8871 states (over memory cap)
KLEE: WARNING: killing 8697 states (over memory cap)
KLEE: WARNING: killing 8437 states (over memory cap)
KLEE: WARNING: killing 8765 states (over memory cap)
KLEE: WARNING: killing 8586 states (over memory cap)
KLEE: WARNING: killing 8411 states (over memory cap)
KLEE: WARNING: killing 8737 states (over memory cap)
KLEE: WARNING: killing 8564 states (over memory cap)
KLEE: WARNING: killing 15925 states (over memory cap)
KLEE: WARNING: killing 9210 states (over memory cap)
KLEE: WARNING: killing 8703 states (over memory cap)
KLEE: WARNING: killing 8526 states (over memory cap)
KLEE: WARNING: killing 8602 states (over memory cap)
KLEE: WARNING: killing 8590 states (over memory cap)
KLEE: WARNING: killing 8585 states (over memory cap)
KLEE: WARNING: killing 8576 states (over memory cap)
KLEE: WARNING: killing 8816 states (over memory cap)
KLEE: WARNING: killing 8477 states (over memory cap)
KLEE: WARNING: killing 8966 states (over memory cap)
KLEE: WARNING: killing 8462 states (over memory cap)
KLEE: WARNING: killing 8702 states (over memory cap)
KLEE: WARNING: killing 8775 states (over memory cap)
KLEE: WARNING: killing 8440 states (over memory cap)
KLEE: WARNING: killing 8597 states (over memory cap)
KLEE: WARNING: killing 8837 states (over memory cap)
KLEE: WARNING: killing 8666 states (over memory cap)
KLEE: WARNING: killing 8494 states (over memory cap)
KLEE: WARNING: killing 8567 states (over memory cap)
KLEE: WARNING: killing 8398 states (over memory cap)
KLEE: WARNING: killing 8799 states (over memory cap)
KLEE: WARNING: killing 8712 states (over memory cap)
KLEE: WARNING: killing 9031 states (over memory cap)
KLEE: WARNING: killing 8450 states (over memory cap)
KLEE: WARNING: killing 8361 states (over memory cap)
