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--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.: 150 183 1700 12483
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.526882886887
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'usb_put_dev' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__list_del_entry' (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 _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)
Removed calls to 'ldv_check_final_state' (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 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.597166061401
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 168 137 888 5920
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_2eef0e58-c478-4cbe-951e-5411c8650e4b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-CvOTAL/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:5848: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-CvOTAL/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:5029: 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 11397 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-CvOTAL/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:3766: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16645 states (over memory cap)
KLEE: WARNING: killing 16879 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 16647 states (over memory cap)
KLEE: WARNING: killing 16484 states (over memory cap)
KLEE: WARNING: killing 16518 states (over memory cap)
KLEE: WARNING: killing 17646 states (over memory cap)
KLEE: WARNING: killing 17986 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-CvOTAL/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:8175: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17245 states (over memory cap)
KLEE: WARNING: killing 17680 states (over memory cap)
KLEE: WARNING: killing 18208 states (over memory cap)
KLEE: WARNING: killing 17870 states (over memory cap)
KLEE: WARNING: killing 18502 states (over memory cap)
KLEE: WARNING: killing 17966 states (over memory cap)
KLEE: WARNING: killing 17916 states (over memory cap)
KLEE: WARNING: killing 9686 states (over memory cap)
KLEE: WARNING: killing 17376 states (over memory cap)
KLEE: WARNING: killing 17138 states (over memory cap)
KLEE: WARNING: killing 17281 states (over memory cap)
KLEE: WARNING: killing 17235 states (over memory cap)
KLEE: WARNING: killing 17656 states (over memory cap)
KLEE: WARNING: killing 17234 states (over memory cap)
KLEE: WARNING: killing 17289 states (over memory cap)
KLEE: WARNING: killing 9496 states (over memory cap)
KLEE: WARNING: killing 16566 states (over memory cap)
KLEE: WARNING: killing 17551 states (over memory cap)
KLEE: WARNING: killing 16855 states (over memory cap)
KLEE: WARNING: killing 9410 states (over memory cap)
KLEE: WARNING: killing 16421 states (over memory cap)
KLEE: WARNING: killing 17217 states (over memory cap)
KLEE: WARNING: killing 9444 states (over memory cap)
KLEE: WARNING: killing 16783 states (over memory cap)
KLEE: WARNING: killing 16842 states (over memory cap)
KLEE: WARNING: killing 9389 states (over memory cap)
KLEE: WARNING: killing 16971 states (over memory cap)
KLEE: WARNING: killing 9543 states (over memory cap)
KLEE: WARNING: killing 17467 states (over memory cap)
KLEE: WARNING: killing 9606 states (over memory cap)
KLEE: WARNING: killing 16772 states (over memory cap)
KLEE: WARNING: killing 9119 states (over memory cap)
KLEE: WARNING: killing 17091 states (over memory cap)
KLEE: WARNING: killing 9633 states (over memory cap)
KLEE: WARNING: killing 16762 states (over memory cap)
KLEE: WARNING: killing 9244 states (over memory cap)
KLEE: WARNING: killing 16798 states (over memory cap)
KLEE: WARNING: killing 17035 states (over memory cap)
KLEE: WARNING: killing 9103 states (over memory cap)
KLEE: WARNING: killing 16711 states (over memory cap)
KLEE: WARNING: killing 9426 states (over memory cap)
KLEE: WARNING: killing 16649 states (over memory cap)
KLEE: WARNING: killing 9397 states (over memory cap)
KLEE: WARNING: killing 16691 states (over memory cap)
KLEE: WARNING: killing 9278 states (over memory cap)
KLEE: WARNING: killing 16728 states (over memory cap)
KLEE: WARNING: killing 9253 states (over memory cap)
KLEE: WARNING: killing 8889 states (over memory cap)
KLEE: WARNING: killing 16398 states (over memory cap)
KLEE: WARNING: killing 9217 states (over memory cap)
KLEE: WARNING: killing 8854 states (over memory cap)
KLEE: WARNING: killing 8846 states (over memory cap)
KLEE: WARNING: killing 16769 states (over memory cap)
KLEE: WARNING: killing 9264 states (over memory cap)
KLEE: WARNING: killing 16715 states (over memory cap)
KLEE: WARNING: killing 9323 states (over memory cap)
KLEE: WARNING: killing 8786 states (over memory cap)
KLEE: WARNING: killing 16650 states (over memory cap)
KLEE: WARNING: killing 9284 states (over memory cap)
KLEE: WARNING: killing 8755 states (over memory cap)
KLEE: WARNING: killing 8831 states (over memory cap)
KLEE: WARNING: killing 8736 states (over memory cap)
KLEE: WARNING: killing 16731 states (over memory cap)
KLEE: WARNING: killing 8794 states (over memory cap)
KLEE: WARNING: killing 16498 states (over memory cap)
KLEE: WARNING: killing 9202 states (over memory cap)
KLEE: WARNING: killing 16014 states (over memory cap)
KLEE: WARNING: killing 9342 states (over memory cap)
KLEE: WARNING: killing 8906 states (over memory cap)
KLEE: WARNING: killing 8724 states (over memory cap)
KLEE: WARNING: killing 16549 states (over memory cap)
KLEE: WARNING: killing 9386 states (over memory cap)
KLEE: WARNING: killing 8780 states (over memory cap)
KLEE: WARNING: killing 8682 states (over memory cap)
KLEE: WARNING: killing 16477 states (over memory cap)
KLEE: WARNING: killing 9603 states (over memory cap)
KLEE: WARNING: killing 8570 states (over memory cap)
KLEE: WARNING: killing 8650 states (over memory cap)
KLEE: WARNING: killing 8814 states (over memory cap)
KLEE: WARNING: killing 8546 states (over memory cap)
KLEE: WARNING: killing 8709 states (over memory cap)
KLEE: WARNING: killing 8786 states (over memory cap)
KLEE: WARNING: killing 16268 states (over memory cap)
KLEE: WARNING: killing 9273 states (over memory cap)
KLEE: WARNING: killing 8756 states (over memory cap)
KLEE: WARNING: killing 8574 states (over memory cap)
KLEE: WARNING: killing 16279 states (over memory cap)
KLEE: WARNING: killing 9653 states (over memory cap)
KLEE: WARNING: killing 8630 states (over memory cap)
KLEE: WARNING: killing 8539 states (over memory cap)
KLEE: WARNING: killing 15776 states (over memory cap)
KLEE: WARNING: killing 9522 states (over memory cap)
KLEE: WARNING: killing 8841 states (over memory cap)
KLEE: WARNING: killing 8499 states (over memory cap)
KLEE: WARNING: killing 8658 states (over memory cap)
KLEE: WARNING: killing 8654 states (over memory cap)
KLEE: WARNING: killing 8810 states (over memory cap)
KLEE: WARNING: killing 16266 states (over memory cap)
KLEE: WARNING: killing 9207 states (over memory cap)
KLEE: WARNING: killing 8701 states (over memory cap)
KLEE: WARNING: killing 8940 states (over memory cap)
KLEE: WARNING: killing 8686 states (over memory cap)
KLEE: WARNING: killing 9008 states (over memory cap)
KLEE: WARNING: killing 8505 states (over memory cap)
KLEE: WARNING: killing 8497 states (over memory cap)
KLEE: WARNING: killing 8737 states (over memory cap)
KLEE: WARNING: killing 8480 states (over memory cap)
KLEE: WARNING: killing 8718 states (over memory cap)
KLEE: WARNING: killing 8626 states (over memory cap)
KLEE: WARNING: killing 8536 states (over memory cap)
KLEE: WARNING: killing 8364 states (over memory cap)
KLEE: WARNING: killing 8768 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 9653 states (over memory cap)
KLEE: WARNING: killing 8823 states (over memory cap)
KLEE: WARNING: killing 8405 states (over memory cap)
KLEE: WARNING: killing 8638 states (over memory cap)
KLEE: WARNING: killing 8713 states (over memory cap)
KLEE: WARNING: killing 8787 states (over memory cap)
KLEE: WARNING: killing 8616 states (over memory cap)
KLEE: WARNING: killing 8445 states (over memory cap)
KLEE: WARNING: killing 8763 states (over memory cap)
