bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-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.: 189 130 1275 8798
Removed infinite loop in ldv_stop___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.382676839828
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (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 'mutex_unlock' (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)
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 mod_timer as symbolic
Defining function rc_g_keycode_from_table as symbolic
Defining function del_timer_sync as symbolic
Defining function usb_ifnum_to_if as symbolic
Defining function sysfs_create_group as symbolic
Defining function _dev_info as symbolic
Defining function dev_err as symbolic
Defining function usb_register_dev 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 dev_set_drvdata 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 ___ratelimit as symbolic
Defining function wait_for_completion_interruptible as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function schedule_timeout as symbolic
Defining function dev_get_drvdata 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
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.39518904686
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 247 128 682 5227
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_d63ab089-8e74-4982-8e37-49e91c43d95a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Jze4_0/linux-3.12-rc1.tar.xz-144_2a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:7322: 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 12519 states (over memory cap)
KLEE: WARNING: killing 10383 states (over memory cap)
KLEE: WARNING: killing 9519 states (over memory cap)
KLEE: WARNING: killing 9578 states (over memory cap)
KLEE: WARNING: killing 9223 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9674 states (over memory cap)
KLEE: WARNING: killing 9901 states (over memory cap)
KLEE: WARNING: killing 9718 states (over memory cap)
KLEE: WARNING: killing 9204 states (over memory cap)
KLEE: WARNING: killing 9677 states (over memory cap)
KLEE: WARNING: killing 9740 states (over memory cap)
KLEE: WARNING: killing 9642 states (over memory cap)
KLEE: WARNING: killing 9957 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 10254 states (over memory cap)
KLEE: WARNING: killing 10972 states (over memory cap)
KLEE: WARNING: killing 10715 states (over memory cap)
KLEE: WARNING: killing 10703 states (over memory cap)
KLEE: WARNING: killing 10447 states (over memory cap)
KLEE: WARNING: killing 10999 states (over memory cap)
KLEE: WARNING: killing 10663 states (over memory cap)
KLEE: WARNING: killing 10571 states (over memory cap)
KLEE: WARNING: killing 10800 states (over memory cap)
KLEE: WARNING: killing 10386 states (over memory cap)
KLEE: WARNING: killing 10454 states (over memory cap)
KLEE: WARNING: killing 10277 states (over memory cap)
KLEE: WARNING: killing 10099 states (over memory cap)
KLEE: WARNING: killing 10568 states (over memory cap)
KLEE: WARNING: killing 10075 states (over memory cap)
KLEE: WARNING: killing 10300 states (over memory cap)
KLEE: WARNING: killing 9805 states (over memory cap)
KLEE: WARNING: killing 10516 states (over memory cap)
KLEE: WARNING: killing 10100 states (over memory cap)
KLEE: WARNING: killing 10330 states (over memory cap)
KLEE: WARNING: killing 9835 states (over memory cap)
KLEE: WARNING: killing 10461 states (over memory cap)
KLEE: WARNING: killing 10288 states (over memory cap)
KLEE: WARNING: killing 9955 states (over memory cap)
KLEE: WARNING: killing 10105 states (over memory cap)
KLEE: WARNING: killing 10169 states (over memory cap)
KLEE: WARNING: killing 10313 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 9974 states (over memory cap)
KLEE: WARNING: killing 10359 states (over memory cap)
KLEE: WARNING: killing 10426 states (over memory cap)
KLEE: WARNING: killing 10569 states (over memory cap)
KLEE: WARNING: killing 10319 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10536 states (over memory cap)
KLEE: WARNING: killing 10682 states (over memory cap)
KLEE: WARNING: killing 10826 states (over memory cap)
KLEE: WARNING: killing 10656 states (over memory cap)
KLEE: WARNING: killing 10650 states (over memory cap)
KLEE: WARNING: killing 10558 states (over memory cap)
KLEE: WARNING: killing 10314 states (over memory cap)
KLEE: WARNING: killing 10846 states (over memory cap)
KLEE: WARNING: killing 10760 states (over memory cap)
KLEE: WARNING: killing 10746 states (over memory cap)
KLEE: WARNING: killing 9960 states (over memory cap)
KLEE: WARNING: killing 10490 states (over memory cap)
KLEE: WARNING: killing 10480 states (over memory cap)
KLEE: WARNING: killing 9849 states (over memory cap)
KLEE: WARNING: killing 10301 states (over memory cap)
KLEE: WARNING: killing 10676 states (over memory cap)
KLEE: WARNING: killing 10508 states (over memory cap)
KLEE: WARNING: killing 10418 states (over memory cap)
KLEE: WARNING: killing 10716 states (over memory cap)
KLEE: WARNING: killing 10471 states (over memory cap)
KLEE: WARNING: killing 10461 states (over memory cap)
KLEE: WARNING: killing 10220 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Jze4_0/linux-3.12-rc1.tar.xz-144_2a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:3926: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10488 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 9690 states (over memory cap)
KLEE: WARNING: killing 10667 states (over memory cap)
KLEE: WARNING: killing 10351 states (over memory cap)
KLEE: WARNING: killing 10566 states (over memory cap)
KLEE: WARNING: killing 10327 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Jze4_0/linux-3.12-rc1.tar.xz-144_2a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:4889: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10315 states (over memory cap)
KLEE: WARNING: killing 10604 states (over memory cap)
KLEE: WARNING: killing 10217 states (over memory cap)
KLEE: WARNING: killing 10732 states (over memory cap)
KLEE: WARNING: killing 10573 states (over memory cap)
KLEE: WARNING: killing 10635 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10537 states (over memory cap)
KLEE: WARNING: killing 10071 states (over memory cap)
KLEE: WARNING: killing 10437 states (over memory cap)
KLEE: WARNING: killing 10205 states (over memory cap)
KLEE: WARNING: killing 10343 states (over memory cap)
KLEE: WARNING: killing 10707 states (over memory cap)
KLEE: WARNING: killing 10619 states (over memory cap)
KLEE: WARNING: killing 10613 states (over memory cap)
KLEE: WARNING: killing 10375 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 10504 states (over memory cap)
KLEE: WARNING: killing 10420 states (over memory cap)
KLEE: WARNING: killing 10336 states (over memory cap)
KLEE: WARNING: killing 10172 states (over memory cap)
KLEE: WARNING: killing 10233 states (over memory cap)
KLEE: WARNING: killing 10375 states (over memory cap)
KLEE: WARNING: killing 10439 states (over memory cap)
KLEE: WARNING: killing 9979 states (over memory cap)
KLEE: WARNING: killing 10927 states (over memory cap)
KLEE: WARNING: killing 10256 states (over memory cap)
KLEE: WARNING: killing 10618 states (over memory cap)
KLEE: WARNING: killing 10384 states (over memory cap)
KLEE: WARNING: killing 10074 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 10422 states (over memory cap)
KLEE: WARNING: killing 10266 states (over memory cap)
KLEE: WARNING: killing 10474 states (over memory cap)
KLEE: WARNING: killing 10242 states (over memory cap)
KLEE: WARNING: killing 10599 states (over memory cap)
KLEE: WARNING: killing 10664 states (over memory cap)
KLEE: WARNING: killing 10217 states (over memory cap)
KLEE: WARNING: killing 10060 states (over memory cap)
KLEE: WARNING: killing 10560 states (over memory cap)
KLEE: WARNING: killing 10404 states (over memory cap)
KLEE: WARNING: killing 10248 states (over memory cap)
KLEE: WARNING: killing 10676 states (over memory cap)
KLEE: WARNING: killing 10520 states (over memory cap)
KLEE: WARNING: killing 10513 states (over memory cap)
KLEE: WARNING: killing 10505 states (over memory cap)
KLEE: WARNING: killing 10206 states (over memory cap)
KLEE: WARNING: killing 10489 states (over memory cap)
KLEE: WARNING: killing 10191 states (over memory cap)
KLEE: WARNING: killing 10111 states (over memory cap)
KLEE: WARNING: killing 10316 states (over memory cap)
KLEE: WARNING: killing 10522 states (over memory cap)
KLEE: WARNING: killing 10366 states (over memory cap)
KLEE: WARNING: killing 10216 states (over memory cap)
KLEE: WARNING: killing 10275 states (over memory cap)
KLEE: WARNING: killing 10339 states (over memory cap)
KLEE: WARNING: killing 10760 states (over memory cap)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 9954 states (over memory cap)
KLEE: WARNING: killing 10374 states (over memory cap)
KLEE: WARNING: killing 10221 states (over memory cap)
KLEE: WARNING: killing 10212 states (over memory cap)
KLEE: WARNING: killing 10848 states (over memory cap)
KLEE: WARNING: killing 9910 states (over memory cap)
KLEE: WARNING: killing 10395 states (over memory cap)
KLEE: WARNING: killing 10458 states (over memory cap)
KLEE: WARNING: killing 10739 states (over memory cap)
KLEE: WARNING: killing 10732 states (over memory cap)
KLEE: WARNING: killing 10658 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 10640 states (over memory cap)
KLEE: WARNING: killing 10484 states (over memory cap)
KLEE: WARNING: killing 10195 states (over memory cap)
KLEE: WARNING: killing 10755 states (over memory cap)
KLEE: WARNING: killing 10961 states (over memory cap)
KLEE: WARNING: killing 9605 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Jze4_0/linux-3.12-rc1.tar.xz-144_2a-drivers--media--rc--imon.ko-entry_point_false-unreach-call.cil.out.c:7027: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10096 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 10076 states (over memory cap)
KLEE: WARNING: killing 9993 states (over memory cap)
KLEE: WARNING: killing 10551 states (over memory cap)
KLEE: WARNING: killing 10331 states (over memory cap)
KLEE: WARNING: killing 10535 states (over memory cap)
KLEE: WARNING: killing 10600 states (over memory cap)
KLEE: WARNING: killing 10520 states (over memory cap)
KLEE: WARNING: killing 9877 states (over memory cap)
KLEE: WARNING: killing 10500 states (over memory cap)
KLEE: WARNING: killing 10209 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 10544 states (over memory cap)
KLEE: WARNING: killing 10467 states (over memory cap)
KLEE: WARNING: killing 10249 states (over memory cap)
KLEE: WARNING: killing 10382 states (over memory cap)
KLEE: WARNING: killing 10377 states (over memory cap)
KLEE: WARNING: killing 10712 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 9941 states (over memory cap)
KLEE: WARNING: killing 10350 states (over memory cap)
KLEE: WARNING: killing 10619 states (over memory cap)
KLEE: WARNING: killing 10402 states (over memory cap)
KLEE: WARNING: killing 10674 states (over memory cap)
KLEE: WARNING: killing 10527 states (over memory cap)
