bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_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.: 182 171 1323 8499
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.360067844391
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 'ldv_initialize' (function is undefined)
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
  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.36527299881
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 226 169 809 4734
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_a3e5312b-e0fc-46c6-9ed6-c52dc30b37c5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:6618: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO42[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4391: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4428: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4341: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4367: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4367: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4344: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4004: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:6314: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4012: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4214: 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 16412 states (over memory cap)
KLEE: WARNING: killing 9889 states (over memory cap)
KLEE: WARNING: killing 17843 states (over memory cap)
KLEE: WARNING: killing 9924 states (over memory cap)
KLEE: WARNING: killing 17926 states (over memory cap)
KLEE: WARNING: killing 9490 states (over memory cap)
KLEE: WARNING: killing 18011 states (over memory cap)
KLEE: WARNING: killing 9717 states (over memory cap)
KLEE: WARNING: killing 18107 states (over memory cap)
KLEE: WARNING: killing 9852 states (over memory cap)
KLEE: WARNING: killing 9648 states (over memory cap)
KLEE: WARNING: killing 9542 states (over memory cap)
KLEE: WARNING: killing 9340 states (over memory cap)
KLEE: WARNING: killing 9603 states (over memory cap)
KLEE: WARNING: killing 9958 states (over memory cap)
KLEE: WARNING: killing 10223 states (over memory cap)
KLEE: WARNING: killing 9747 states (over memory cap)
KLEE: WARNING: killing 10010 states (over memory cap)
KLEE: WARNING: killing 10365 states (over memory cap)
KLEE: WARNING: killing 10257 states (over memory cap)
KLEE: WARNING: killing 10062 states (over memory cap)
KLEE: WARNING: killing 10048 states (over memory cap)
KLEE: WARNING: killing 10311 states (over memory cap)
KLEE: WARNING: killing 10023 states (over memory cap)
KLEE: WARNING: killing 10377 states (over memory cap)
KLEE: WARNING: killing 10273 states (over memory cap)
KLEE: WARNING: killing 10258 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 10143 states (over memory cap)
KLEE: WARNING: killing 9763 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 10284 states (over memory cap)
KLEE: WARNING: killing 10635 states (over memory cap)
KLEE: WARNING: killing 10079 states (over memory cap)
KLEE: WARNING: killing 9521 states (over memory cap)
KLEE: WARNING: killing 9594 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-E_xRVT/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4222: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10302 states (over memory cap)
KLEE: WARNING: killing 9839 states (over memory cap)
KLEE: WARNING: killing 9825 states (over memory cap)
KLEE: WARNING: killing 10078 states (over memory cap)
KLEE: WARNING: killing 10068 states (over memory cap)
KLEE: WARNING: killing 10229 states (over memory cap)
KLEE: WARNING: killing 9948 states (over memory cap)
KLEE: WARNING: killing 10027 states (over memory cap)
KLEE: WARNING: killing 10098 states (over memory cap)
KLEE: WARNING: killing 9822 states (over memory cap)
KLEE: WARNING: killing 10168 states (over memory cap)
KLEE: WARNING: killing 10417 states (over memory cap)
KLEE: WARNING: killing 10230 states (over memory cap)
KLEE: WARNING: killing 10482 states (over memory cap)
KLEE: WARNING: killing 10387 states (over memory cap)
KLEE: WARNING: killing 10105 states (over memory cap)
KLEE: WARNING: killing 9828 states (over memory cap)
KLEE: WARNING: killing 10347 states (over memory cap)
KLEE: WARNING: killing 10425 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10311 states (over memory cap)
KLEE: WARNING: killing 10218 states (over memory cap)
KLEE: WARNING: killing 10294 states (over memory cap)
KLEE: WARNING: killing 9757 states (over memory cap)
KLEE: WARNING: killing 10274 states (over memory cap)
KLEE: WARNING: killing 10260 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 10845 states (over memory cap)
KLEE: WARNING: killing 9702 states (over memory cap)
KLEE: WARNING: killing 10125 states (over memory cap)
KLEE: WARNING: killing 9680 states (over memory cap)
KLEE: WARNING: killing 10446 states (over memory cap)
KLEE: WARNING: killing 10349 states (over memory cap)
KLEE: WARNING: killing 9906 states (over memory cap)
KLEE: WARNING: killing 10153 states (over memory cap)
KLEE: WARNING: killing 9795 states (over memory cap)
KLEE: WARNING: killing 10304 states (over memory cap)
KLEE: WARNING: killing 9860 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 10099 states (over memory cap)
KLEE: WARNING: killing 10261 states (over memory cap)
KLEE: WARNING: killing 10246 states (over memory cap)
KLEE: WARNING: killing 10239 states (over memory cap)
KLEE: WARNING: killing 10314 states (over memory cap)
KLEE: WARNING: killing 10048 states (over memory cap)
KLEE: WARNING: killing 9775 states (over memory cap)
KLEE: WARNING: killing 10108 states (over memory cap)
KLEE: WARNING: killing 10354 states (over memory cap)
KLEE: WARNING: killing 10515 states (over memory cap)
KLEE: WARNING: killing 9994 states (over memory cap)
KLEE: WARNING: killing 9984 states (over memory cap)
KLEE: WARNING: killing 9631 states (over memory cap)
KLEE: WARNING: killing 10046 states (over memory cap)
KLEE: WARNING: killing 9862 states (over memory cap)
KLEE: WARNING: killing 10195 states (over memory cap)
KLEE: WARNING: killing 10351 states (over memory cap)
KLEE: WARNING: killing 10171 states (over memory cap)
KLEE: WARNING: killing 10076 states (over memory cap)
KLEE: WARNING: killing 10319 states (over memory cap)
KLEE: WARNING: killing 10139 states (over memory cap)
KLEE: WARNING: killing 10218 states (over memory cap)
KLEE: WARNING: killing 10042 states (over memory cap)
KLEE: WARNING: killing 10450 states (over memory cap)
KLEE: WARNING: killing 9850 states (over memory cap)
KLEE: WARNING: killing 10009 states (over memory cap)
KLEE: WARNING: killing 10421 states (over memory cap)
KLEE: WARNING: killing 10074 states (over memory cap)
