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--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 171 1694 12294
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.415703058243
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 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
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.457966089249
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 168 126 846 5682
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_f373fb6e-7b1b-4898-9b52-f5617293fc5e/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-W_0HNu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:5031: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-W_0HNu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:5850: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-W_0HNu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:3659: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-W_0HNu/linux-4.2-rc1.tar.xz-08_1a-drivers--usb--misc--ftdi-elan.ko-entry_point_true-unreach-call.cil.out.c:8225: 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 13557 states (over memory cap)
KLEE: WARNING: killing 16286 states (over memory cap)
KLEE: WARNING: killing 16815 states (over memory cap)
KLEE: WARNING: killing 16743 states (over memory cap)
KLEE: WARNING: killing 16188 states (over memory cap)
KLEE: WARNING: killing 17008 states (over memory cap)
KLEE: WARNING: killing 16951 states (over memory cap)
KLEE: WARNING: killing 17389 states (over memory cap)
KLEE: WARNING: killing 17334 states (over memory cap)
KLEE: WARNING: killing 17276 states (over memory cap)
KLEE: WARNING: killing 17513 states (over memory cap)
KLEE: WARNING: killing 17860 states (over memory cap)
KLEE: WARNING: killing 18005 states (over memory cap)
KLEE: WARNING: killing 17866 states (over memory cap)
KLEE: WARNING: killing 17427 states (over memory cap)
KLEE: WARNING: killing 17004 states (over memory cap)
KLEE: WARNING: killing 17522 states (over memory cap)
KLEE: WARNING: killing 17483 states (over memory cap)
KLEE: WARNING: killing 17429 states (over memory cap)
KLEE: WARNING: killing 17292 states (over memory cap)
KLEE: WARNING: killing 17340 states (over memory cap)
KLEE: WARNING: killing 17295 states (over memory cap)
KLEE: WARNING: killing 17166 states (over memory cap)
KLEE: WARNING: killing 17591 states (over memory cap)
KLEE: WARNING: killing 17262 states (over memory cap)
KLEE: WARNING: killing 16941 states (over memory cap)
KLEE: WARNING: killing 17172 states (over memory cap)
KLEE: WARNING: killing 17414 states (over memory cap)
KLEE: WARNING: killing 9640 states (over memory cap)
KLEE: WARNING: killing 16520 states (over memory cap)
KLEE: WARNING: killing 16847 states (over memory cap)
KLEE: WARNING: killing 17177 states (over memory cap)
KLEE: WARNING: killing 17138 states (over memory cap)
KLEE: WARNING: killing 17105 states (over memory cap)
KLEE: WARNING: killing 9151 states (over memory cap)
KLEE: WARNING: killing 16594 states (over memory cap)
KLEE: WARNING: killing 9211 states (over memory cap)
KLEE: WARNING: killing 17271 states (over memory cap)
KLEE: WARNING: killing 9363 states (over memory cap)
KLEE: WARNING: killing 16846 states (over memory cap)
KLEE: WARNING: killing 9422 states (over memory cap)
KLEE: WARNING: killing 16892 states (over memory cap)
KLEE: WARNING: killing 9211 states (over memory cap)
KLEE: WARNING: killing 16565 states (over memory cap)
KLEE: WARNING: killing 9186 states (over memory cap)
KLEE: WARNING: killing 16337 states (over memory cap)
KLEE: WARNING: killing 9157 states (over memory cap)
KLEE: WARNING: killing 16911 states (over memory cap)
KLEE: WARNING: killing 9214 states (over memory cap)
KLEE: WARNING: killing 16951 states (over memory cap)
KLEE: WARNING: killing 9097 states (over memory cap)
KLEE: WARNING: killing 8998 states (over memory cap)
KLEE: WARNING: killing 17063 states (over memory cap)
KLEE: WARNING: killing 9063 states (over memory cap)
KLEE: WARNING: killing 16471 states (over memory cap)
KLEE: WARNING: killing 9471 states (over memory cap)
KLEE: WARNING: killing 8847 states (over memory cap)
KLEE: WARNING: killing 17207 states (over memory cap)
KLEE: WARNING: killing 9350 states (over memory cap)
KLEE: WARNING: killing 17066 states (over memory cap)
KLEE: WARNING: killing 9586 states (over memory cap)
KLEE: WARNING: killing 16400 states (over memory cap)
KLEE: WARNING: killing 9117 states (over memory cap)
KLEE: WARNING: killing 16613 states (over memory cap)
KLEE: WARNING: killing 9176 states (over memory cap)
KLEE: WARNING: killing 16390 states (over memory cap)
KLEE: WARNING: killing 8891 states (over memory cap)
KLEE: WARNING: killing 8795 states (over memory cap)
KLEE: WARNING: killing 16679 states (over memory cap)
KLEE: WARNING: killing 9028 states (over memory cap)
KLEE: WARNING: killing 8672 states (over memory cap)
KLEE: WARNING: killing 16439 states (over memory cap)
KLEE: WARNING: killing 9420 states (over memory cap)
KLEE: WARNING: killing 16654 states (over memory cap)
KLEE: WARNING: killing 9307 states (over memory cap)
KLEE: WARNING: killing 8700 states (over memory cap)
KLEE: WARNING: killing 8690 states (over memory cap)
KLEE: WARNING: killing 8680 states (over memory cap)
KLEE: WARNING: killing 8675 states (over memory cap)
KLEE: WARNING: killing 8579 states (over memory cap)
KLEE: WARNING: killing 8919 states (over memory cap)
KLEE: WARNING: killing 9080 states (over memory cap)
KLEE: WARNING: killing 8731 states (over memory cap)
KLEE: WARNING: killing 8553 states (over memory cap)
KLEE: WARNING: killing 8802 states (over memory cap)
KLEE: WARNING: killing 8538 states (over memory cap)
KLEE: WARNING: killing 8614 states (over memory cap)
KLEE: WARNING: killing 16263 states (over memory cap)
KLEE: WARNING: killing 9269 states (over memory cap)
KLEE: WARNING: killing 8921 states (over memory cap)
KLEE: WARNING: killing 16719 states (over memory cap)
KLEE: WARNING: killing 9156 states (over memory cap)
KLEE: WARNING: killing 16244 states (over memory cap)
KLEE: WARNING: killing 9299 states (over memory cap)
KLEE: WARNING: killing 8784 states (over memory cap)
KLEE: WARNING: killing 8603 states (over memory cap)
KLEE: WARNING: killing 16171 states (over memory cap)
KLEE: WARNING: killing 9337 states (over memory cap)
KLEE: WARNING: killing 9080 states (over memory cap)
KLEE: WARNING: killing 8481 states (over memory cap)
KLEE: WARNING: killing 8562 states (over memory cap)
KLEE: WARNING: killing 8722 states (over memory cap)
KLEE: WARNING: killing 8459 states (over memory cap)
KLEE: WARNING: killing 8366 states (over memory cap)
KLEE: WARNING: killing 16295 states (over memory cap)
KLEE: WARNING: killing 9428 states (over memory cap)
KLEE: WARNING: killing 9004 states (over memory cap)
KLEE: WARNING: killing 8582 states (over memory cap)
KLEE: WARNING: killing 8656 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 8392 states (over memory cap)
KLEE: WARNING: killing 8634 states (over memory cap)
KLEE: WARNING: killing 8376 states (over memory cap)
KLEE: WARNING: killing 8782 states (over memory cap)
KLEE: WARNING: killing 8606 states (over memory cap)
KLEE: WARNING: killing 8599 states (over memory cap)
KLEE: WARNING: killing 8593 states (over memory cap)
KLEE: WARNING: killing 8836 states (over memory cap)
KLEE: WARNING: killing 9074 states (over memory cap)
KLEE: WARNING: killing 8656 states (over memory cap)
KLEE: WARNING: killing 8488 states (over memory cap)
KLEE: WARNING: killing 8726 states (over memory cap)
KLEE: WARNING: killing 8718 states (over memory cap)
KLEE: WARNING: killing 8467 states (over memory cap)
KLEE: WARNING: killing 8371 states (over memory cap)
KLEE: WARNING: killing 8613 states (over memory cap)
KLEE: WARNING: killing 8602 states (over memory cap)
KLEE: WARNING: killing 8676 states (over memory cap)
KLEE: WARNING: killing 8507 states (over memory cap)
KLEE: WARNING: killing 8577 states (over memory cap)
KLEE: WARNING: killing 8649 states (over memory cap)
KLEE: WARNING: killing 8560 states (over memory cap)
KLEE: WARNING: killing 8471 states (over memory cap)
KLEE: WARNING: killing 8379 states (over memory cap)
KLEE: WARNING: killing 8696 states (over memory cap)
KLEE: WARNING: killing 8934 states (over memory cap)
KLEE: WARNING: killing 15752 states (over memory cap)
KLEE: WARNING: killing 9480 states (over memory cap)
KLEE: WARNING: killing 8664 states (over memory cap)
KLEE: WARNING: killing 8814 states (over memory cap)
KLEE: WARNING: killing 8805 states (over memory cap)
KLEE: WARNING: killing 8475 states (over memory cap)
KLEE: WARNING: killing 8709 states (over memory cap)
KLEE: WARNING: killing 8704 states (over memory cap)
KLEE: WARNING: killing 8699 states (over memory cap)
KLEE: WARNING: killing 8526 states (over memory cap)
KLEE: WARNING: killing 8603 states (over memory cap)
KLEE: WARNING: killing 8832 states (over memory cap)
KLEE: WARNING: killing 8745 states (over memory cap)
KLEE: WARNING: killing 8581 states (over memory cap)
KLEE: WARNING: killing 8573 states (over memory cap)
KLEE: WARNING: killing 9047 states (over memory cap)
KLEE: WARNING: killing 8637 states (over memory cap)
KLEE: WARNING: killing 8631 states (over memory cap)
KLEE: WARNING: killing 8461 states (over memory cap)
KLEE: WARNING: killing 8613 states (over memory cap)
KLEE: WARNING: killing 8445 states (over memory cap)
KLEE: WARNING: killing 8515 states (over memory cap)
KLEE: WARNING: killing 8426 states (over memory cap)
KLEE: WARNING: killing 8655 states (over memory cap)
KLEE: WARNING: killing 8726 states (over memory cap)
