bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-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.: 183 154 1292 8364
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.367063999176
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'dev_set_drvdata' (function is undefined)
Removed calls to 'input_free_device' (function is undefined)
Removed calls to 'rc_free_device' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'input_set_abs_params' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'complete_all' (function is undefined)
Removed calls to 'rc_unregister_device' (function is undefined)
Removed calls to 'usb_deregister_dev' (function is undefined)
Defining function usb_submit_urb as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Removed calls to 'rc_keyup' (function is undefined)
Removed calls to 'rc_keydown' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function dev_warn as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function printk as symbolic
Defining function _dev_info as symbolic
Defining function mod_timer as symbolic
Defining function rc_g_keycode_from_table as symbolic
Defining function dev_get_drvdata as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function usb_get_dev as symbolic
Defining function usb_ifnum_to_if as symbolic
Defining function sysfs_create_group as symbolic
Defining function dev_err as symbolic
Defining function usb_register_dev as symbolic
Defining function usb_alloc_urb as symbolic
Defining function input_allocate_device as symbolic
Defining function snprintf as symbolic
Defining function strlcat as symbolic
Defining function input_register_device as symbolic
Defining function rc_allocate_device as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function rc_register_device as symbolic
Removed calls to 'complete' (function is undefined)
Defining function wait_for_completion_interruptible as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function schedule_timeout as symbolic
Defining function sscanf as symbolic
Defining function noop_llseek as symbolic
Defining function usb_find_interface as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_reset_resume_4 as symbolic
Defining function usb_register_driver as symbolic
Defining function del_timer as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.383892059326
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 235 156 770 4634
INFO: Starting verification
KLEE: WARNING ONCE: function "imon_probe" has inline asm
KLEE: WARNING ONCE: function "send_packet" 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_b16d3d3b-4a3e-4ba6-a9fd-e8afee0e0b3d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MvxB87/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:6624: 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 17882 states (over memory cap)
KLEE: WARNING: killing 9908 states (over memory cap)
KLEE: WARNING: killing 9803 states (over memory cap)
KLEE: WARNING: killing 9137 states (over memory cap)
KLEE: WARNING: killing 9916 states (over memory cap)
KLEE: WARNING: killing 9176 states (over memory cap)
KLEE: WARNING: killing 9392 states (over memory cap)
KLEE: WARNING: killing 9773 states (over memory cap)
KLEE: WARNING: killing 9752 states (over memory cap)
KLEE: WARNING: killing 9973 states (over memory cap)
KLEE: WARNING: killing 9478 states (over memory cap)
KLEE: WARNING: killing 9702 states (over memory cap)
KLEE: WARNING: killing 10158 states (over memory cap)
KLEE: WARNING: killing 10537 states (over memory cap)
KLEE: WARNING: killing 10679 states (over memory cap)
KLEE: WARNING: killing 10666 states (over memory cap)
KLEE: WARNING: killing 10572 states (over memory cap)
KLEE: WARNING: killing 10795 states (over memory cap)
KLEE: WARNING: killing 10702 states (over memory cap)
KLEE: WARNING: killing 10851 states (over memory cap)
KLEE: WARNING: killing 10442 states (over memory cap)
KLEE: WARNING: killing 10198 states (over memory cap)
KLEE: WARNING: killing 10257 states (over memory cap)
KLEE: WARNING: killing 10797 states (over memory cap)
KLEE: WARNING: killing 10236 states (over memory cap)
KLEE: WARNING: killing 10226 states (over memory cap)
KLEE: WARNING: killing 9978 states (over memory cap)
KLEE: WARNING: killing 10271 states (over memory cap)
KLEE: WARNING: killing 10105 states (over memory cap)
KLEE: WARNING: killing 10089 states (over memory cap)
KLEE: WARNING: killing 10153 states (over memory cap)
KLEE: WARNING: killing 10372 states (over memory cap)
KLEE: WARNING: killing 10827 states (over memory cap)
KLEE: WARNING: killing 10122 states (over memory cap)
KLEE: WARNING: killing 10185 states (over memory cap)
KLEE: WARNING: killing 10555 states (over memory cap)
KLEE: WARNING: killing 11156 states (over memory cap)
KLEE: WARNING: killing 10612 states (over memory cap)
KLEE: WARNING: killing 9986 states (over memory cap)
KLEE: WARNING: killing 10588 states (over memory cap)
KLEE: WARNING: killing 10653 states (over memory cap)
KLEE: WARNING: killing 10872 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MvxB87/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:4372: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10933 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MvxB87/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:3987: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10231 states (over memory cap)
KLEE: WARNING: killing 10527 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 10047 states (over memory cap)
KLEE: WARNING: killing 10261 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10013 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MvxB87/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:3712: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10454 states (over memory cap)
KLEE: WARNING: killing 10743 states (over memory cap)
KLEE: WARNING: killing 10660 states (over memory cap)
KLEE: WARNING: killing 10265 states (over memory cap)
KLEE: WARNING: killing 10102 states (over memory cap)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9715 states (over memory cap)
KLEE: WARNING: killing 10678 states (over memory cap)
KLEE: WARNING: killing 10442 states (over memory cap)
KLEE: WARNING: killing 10580 states (over memory cap)
KLEE: WARNING: killing 11097 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MvxB87/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:4611: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10338 states (over memory cap)
KLEE: WARNING: killing 10547 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MvxB87/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:4504: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10165 states (over memory cap)
KLEE: WARNING: killing 10447 states (over memory cap)
KLEE: WARNING: killing 10214 states (over memory cap)
KLEE: WARNING: killing 10423 states (over memory cap)
KLEE: WARNING: killing 10258 states (over memory cap)
KLEE: WARNING: killing 10769 states (over memory cap)
KLEE: WARNING: killing 10828 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 9769 states (over memory cap)
KLEE: WARNING: killing 10499 states (over memory cap)
KLEE: WARNING: killing 10855 states (over memory cap)
KLEE: WARNING: killing 10473 states (over memory cap)
KLEE: WARNING: killing 10238 states (over memory cap)
KLEE: WARNING: killing 10815 states (over memory cap)
KLEE: WARNING: killing 10216 states (over memory cap)
KLEE: WARNING: killing 11015 states (over memory cap)
KLEE: WARNING: killing 10268 states (over memory cap)
KLEE: WARNING: killing 10622 states (over memory cap)
KLEE: WARNING: killing 10100 states (over memory cap)
KLEE: WARNING: killing 10307 states (over memory cap)
KLEE: WARNING: killing 10513 states (over memory cap)
KLEE: WARNING: killing 10793 states (over memory cap)
KLEE: WARNING: killing 10271 states (over memory cap)
KLEE: WARNING: killing 10191 states (over memory cap)
KLEE: WARNING: killing 10395 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 10509 states (over memory cap)
KLEE: WARNING: killing 10422 states (over memory cap)
KLEE: WARNING: killing 10340 states (over memory cap)
KLEE: WARNING: killing 10399 states (over memory cap)
KLEE: WARNING: killing 10747 states (over memory cap)
KLEE: WARNING: killing 10594 states (over memory cap)
KLEE: WARNING: killing 10224 states (over memory cap)
KLEE: WARNING: killing 10571 states (over memory cap)
KLEE: WARNING: killing 10270 states (over memory cap)
KLEE: WARNING: killing 10333 states (over memory cap)
KLEE: WARNING: killing 10324 states (over memory cap)
KLEE: WARNING: killing 10817 states (over memory cap)
KLEE: WARNING: killing 9944 states (over memory cap)
KLEE: WARNING: killing 10435 states (over memory cap)
KLEE: WARNING: killing 9994 states (over memory cap)
KLEE: WARNING: killing 10127 states (over memory cap)
KLEE: WARNING: killing 10545 states (over memory cap)
KLEE: WARNING: killing 10177 states (over memory cap)
KLEE: WARNING: killing 10951 states (over memory cap)
KLEE: WARNING: killing 10513 states (over memory cap)
KLEE: WARNING: killing 10360 states (over memory cap)
KLEE: WARNING: killing 10420 states (over memory cap)
KLEE: WARNING: killing 10623 states (over memory cap)
KLEE: WARNING: killing 10754 states (over memory cap)
KLEE: WARNING: killing 10109 states (over memory cap)
KLEE: WARNING: killing 10386 states (over memory cap)
KLEE: WARNING: killing 10940 states (over memory cap)
KLEE: WARNING: killing 10509 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 9995 states (over memory cap)
KLEE: WARNING: killing 10123 states (over memory cap)
KLEE: WARNING: killing 10252 states (over memory cap)
KLEE: WARNING: killing 10600 states (over memory cap)
KLEE: WARNING: killing 10448 states (over memory cap)
KLEE: WARNING: killing 10158 states (over memory cap)
KLEE: WARNING: killing 10425 states (over memory cap)
KLEE: WARNING: killing 10351 states (over memory cap)
KLEE: WARNING: killing 10338 states (over memory cap)
KLEE: WARNING: killing 10824 states (over memory cap)
KLEE: WARNING: killing 10465 states (over memory cap)
KLEE: WARNING: killing 10317 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 10496 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10411 states (over memory cap)
KLEE: WARNING: killing 9917 states (over memory cap)
KLEE: WARNING: killing 10250 states (over memory cap)
KLEE: WARNING: killing 10243 states (over memory cap)
KLEE: WARNING: killing 10161 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 10428 states (over memory cap)
KLEE: WARNING: killing 10281 states (over memory cap)
KLEE: WARNING: killing 10406 states (over memory cap)
KLEE: WARNING: killing 10122 states (over memory cap)
KLEE: WARNING: killing 10596 states (over memory cap)
KLEE: WARNING: killing 10725 states (over memory cap)
KLEE: WARNING: killing 10234 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: WARNING: killing 10427 states (over memory cap)
KLEE: WARNING: killing 10345 states (over memory cap)
KLEE: WARNING: killing 10269 states (over memory cap)
KLEE: WARNING: killing 10327 states (over memory cap)
KLEE: WARNING: killing 9974 states (over memory cap)
KLEE: WARNING: killing 10450 states (over memory cap)
KLEE: WARNING: killing 10236 states (over memory cap)
KLEE: WARNING: killing 10019 states (over memory cap)
KLEE: WARNING: killing 10418 states (over memory cap)
KLEE: WARNING: killing 10612 states (over memory cap)
KLEE: WARNING: killing 9926 states (over memory cap)
KLEE: WARNING: killing 10394 states (over memory cap)
KLEE: WARNING: killing 10658 states (over memory cap)
KLEE: WARNING: killing 10448 states (over memory cap)
KLEE: WARNING: killing 10438 states (over memory cap)
KLEE: WARNING: killing 10498 states (over memory cap)
