bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-usb-uvc-uvcvideo_true-unreach-call.cil.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.: 328 458 5269 30964
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.06380796432
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'usb_driver_release_interface' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'usb_put_intf' (function is undefined)
Removed calls to 'v4l2_prio_init' (function is undefined)
Removed calls to 'video_device_release' (function is undefined)
Removed calls to 'usb_enable_autosuspend' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function printk as symbolic
Defining function usb_set_interface as symbolic
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function usb_submit_urb as symbolic
Removed calls to 'ktime_get_ts' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Defining function usb_alloc_urb as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'vb2_buffer_done' (function is undefined)
Defining function usb_alloc_coherent as symbolic
Defining function vb2_streamon as symbolic
Defining function vb2_streamoff as symbolic
Defining function usb_control_msg as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Defining function debugfs_create_dir as symbolic
Defining function sprintf as symbolic
Defining function strncasecmp as symbolic
Defining function strcasecmp as symbolic
Removed calls to 'set_normalized_timespec' (function is undefined)
Defining function vb2_plane_vaddr as symbolic
Removed calls to 'v4l_printk_ioctl' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'usb_autopm_put_interface' (function is undefined)
Removed calls to 'v4l2_fh_init' (function is undefined)
Removed calls to 'v4l2_fh_add' (function is undefined)
Removed calls to 'v4l2_fh_del' (function is undefined)
Removed calls to 'v4l2_fh_exit' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'vb2_queue_release' (function is undefined)
Defining function usb_autopm_get_interface as symbolic
Defining function video_devdata as symbolic
Defining function vb2_mmap as symbolic
Defining function copy_in_user as symbolic
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Defining function copy_user_enhanced_fast_string as symbolic
Defining function __clear_user as symbolic
Defining function compat_alloc_user_space as symbolic
Defining function video_usercopy as symbolic
Defining function strlcpy as symbolic
Defining function v4l2_prio_max as symbolic
Defining function v4l2_prio_check as symbolic
Defining function v4l2_prio_change as symbolic
Defining function v4l2_event_subscribe as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Defining function v4l2_event_dequeue as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function usb_match_one_id as symbolic
Defining function kmemdup as symbolic
Defining function vb2_dqbuf as symbolic
Defining function vb2_qbuf as symbolic
Defining function vb2_querybuf as symbolic
Defining function vb2_reqbufs as symbolic
Removed calls to 'v4l2_event_queue_fh' (function is undefined)
Defining function snprintf as symbolic
Defining function vb2_poll as symbolic
Defining function no_llseek as symbolic
Defining function scnprintf as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Removed calls to 'media_entity_cleanup' (function is undefined)
Defining function usb_get_dev as symbolic
Defining function usb_get_intf as symbolic
Defining function media_device_register as symbolic
Defining function v4l2_device_register as symbolic
Removed calls to 'input_free_device' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Defining function input_allocate_device as symbolic
Defining function strlcat as symbolic
Defining function input_register_device as symbolic
Removed calls to 'v4l2_subdev_init' (function is undefined)
Defining function media_entity_create_link as symbolic
Defining function v4l2_device_register_subdev as symbolic
Defining function media_entity_init as symbolic
Defining function video_device_alloc as symbolic
Defining function __video_register_device as symbolic
Defining function debugfs_create_file as symbolic
Removed calls to 'getnstimeofday' (function is undefined)
Defining function usb_get_current_frame_number as symbolic
Defining function vb2_queue_init as symbolic
Defining function memweight as symbolic
Defining function usb_ifnum_to_if as symbolic
Defining function usb_string as symbolic
Defining function usb_driver_claim_interface as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'v4l2_ctrl_merge' (function is undefined)
Removed calls to 'v4l2_ctrl_replace' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  __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: 1.14372611046
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 474 388 2501 16414
INFO: Starting verification
KLEE: WARNING ONCE: function "uvc_probe" has inline asm
KLEE: WARNING ONCE: function "uvc_v4l2_compat_ioctl32" has inline asm
KLEE: WARNING ONCE: function "uvc_v4l2_release" has inline asm
KLEE: WARNING ONCE: function "uvc_v4l2_do_ioctl" has inline asm
KLEE: WARNING ONCE: function "uvc_acquire_privileges" has inline asm
KLEE: WARNING ONCE: function "uvc_ctrl_add_mapping" has inline asm
KLEE: WARNING ONCE: function "uvc_unregister_video" has inline asm
KLEE: WARNING ONCE: function "uvc_status_init" has inline asm
KLEE: WARNING: undefined reference to function: v4l2_ctrl_merge
KLEE: WARNING: undefined reference to function: v4l2_ctrl_replace
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_f78425ad-f506-4569-9021-98c3299ff86d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17675 states (over memory cap)
KLEE: WARNING: killing 11652 states (over memory cap)
KLEE: WARNING: killing 11356 states (over memory cap)
KLEE: WARNING: killing 10874 states (over memory cap)
KLEE: WARNING: killing 10854 states (over memory cap)
KLEE: WARNING: killing 10469 states (over memory cap)
KLEE: WARNING: killing 10451 states (over memory cap)
KLEE: WARNING: killing 10526 states (over memory cap)
KLEE: WARNING: killing 9963 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10918 states (over memory cap)
KLEE: WARNING: killing 10807 states (over memory cap)
KLEE: WARNING: killing 10704 states (over memory cap)
KLEE: WARNING: killing 11138 states (over memory cap)
KLEE: WARNING: killing 10851 states (over memory cap)
KLEE: WARNING: killing 11372 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 11882 states (over memory cap)
KLEE: WARNING: killing 11873 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 11838 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 12701 states (over memory cap)
KLEE: WARNING: killing 11887 states (over memory cap)
KLEE: WARNING: killing 12317 states (over memory cap)
KLEE: WARNING: killing 12836 states (over memory cap)
KLEE: WARNING: killing 12374 states (over memory cap)
KLEE: WARNING: killing 12097 states (over memory cap)
KLEE: WARNING: killing 11816 states (over memory cap)
KLEE: WARNING: killing 12153 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 11684 states (over memory cap)
KLEE: WARNING: killing 11848 states (over memory cap)
KLEE: WARNING: killing 11746 states (over memory cap)
KLEE: WARNING: killing 12349 states (over memory cap)
KLEE: WARNING: killing 11194 states (over memory cap)
KLEE: WARNING: killing 11533 states (over memory cap)
KLEE: WARNING: killing 11693 states (over memory cap)
KLEE: WARNING: killing 12031 states (over memory cap)
KLEE: WARNING: killing 11664 states (over memory cap)
KLEE: WARNING: killing 11567 states (over memory cap)
KLEE: WARNING: killing 11729 states (over memory cap)
KLEE: WARNING: killing 11360 states (over memory cap)
KLEE: WARNING: killing 11955 states (over memory cap)
KLEE: WARNING: killing 11685 states (over memory cap)
KLEE: WARNING: killing 11757 states (over memory cap)
KLEE: WARNING: killing 11566 states (over memory cap)
KLEE: WARNING: killing 11559 states (over memory cap)
KLEE: WARNING: killing 12328 states (over memory cap)
KLEE: WARNING: killing 11705 states (over memory cap)
KLEE: WARNING: killing 12300 states (over memory cap)
KLEE: WARNING: killing 12032 states (over memory cap)
KLEE: WARNING: killing 12449 states (over memory cap)
KLEE: WARNING: killing 11916 states (over memory cap)
KLEE: WARNING: killing 11471 states (over memory cap)
KLEE: WARNING: killing 11722 states (over memory cap)
KLEE: WARNING: killing 11450 states (over memory cap)
KLEE: WARNING: killing 11608 states (over memory cap)
KLEE: WARNING: killing 11770 states (over memory cap)
KLEE: WARNING: killing 12015 states (over memory cap)
KLEE: WARNING: killing 11832 states (over memory cap)
KLEE: WARNING: killing 11646 states (over memory cap)
KLEE: WARNING: killing 11892 states (over memory cap)
KLEE: WARNING: killing 12564 states (over memory cap)
KLEE: WARNING: killing 12039 states (over memory cap)
KLEE: WARNING: killing 11599 states (over memory cap)
KLEE: WARNING: killing 12098 states (over memory cap)
KLEE: WARNING: killing 12168 states (over memory cap)
KLEE: WARNING: killing 11812 states (over memory cap)
KLEE: WARNING: killing 12057 states (over memory cap)
KLEE: WARNING: killing 11456 states (over memory cap)
KLEE: WARNING: killing 11022 states (over memory cap)
KLEE: WARNING: killing 12109 states (over memory cap)
KLEE: WARNING: killing 11680 states (over memory cap)
KLEE: WARNING: killing 12172 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 11892 states (over memory cap)
KLEE: WARNING: killing 11628 states (over memory cap)
KLEE: WARNING: killing 11619 states (over memory cap)
KLEE: WARNING: killing 11603 states (over memory cap)
KLEE: WARNING: killing 11423 states (over memory cap)
KLEE: WARNING: killing 11916 states (over memory cap)
KLEE: WARNING: killing 11907 states (over memory cap)
KLEE: WARNING: killing 12149 states (over memory cap)
KLEE: WARNING: killing 11886 states (over memory cap)
KLEE: WARNING: killing 12122 states (over memory cap)
KLEE: WARNING: killing 11860 states (over memory cap)
KLEE: WARNING: killing 12015 states (over memory cap)
KLEE: WARNING: killing 11841 states (over memory cap)
KLEE: WARNING: killing 11661 states (over memory cap)
KLEE: WARNING: killing 12238 states (over memory cap)
KLEE: WARNING: killing 11806 states (over memory cap)
KLEE: WARNING: killing 11632 states (over memory cap)
KLEE: WARNING: killing 11621 states (over memory cap)
KLEE: WARNING: killing 11525 states (over memory cap)
KLEE: WARNING: killing 12010 states (over memory cap)
KLEE: WARNING: killing 11996 states (over memory cap)
KLEE: WARNING: killing 11494 states (over memory cap)
KLEE: WARNING: killing 11813 states (over memory cap)
KLEE: WARNING: killing 11802 states (over memory cap)
KLEE: WARNING: killing 11623 states (over memory cap)
KLEE: WARNING: killing 12353 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TvMFJG/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-usb-uvc-uvcvideo_true-unreach-call.cil.c:22366: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11351 states (over memory cap)
KLEE: WARNING: killing 12085 states (over memory cap)
KLEE: WARNING: killing 11992 states (over memory cap)
KLEE: WARNING: killing 11648 states (over memory cap)
KLEE: WARNING: killing 11639 states (over memory cap)
KLEE: WARNING: killing 11463 states (over memory cap)
KLEE: WARNING: killing 11941 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 11674 states (over memory cap)
KLEE: WARNING: killing 11418 states (over memory cap)
KLEE: WARNING: killing 12224 states (over memory cap)
KLEE: WARNING: killing 11482 states (over memory cap)
KLEE: WARNING: killing 11959 states (over memory cap)
KLEE: WARNING: killing 11382 states (over memory cap)
KLEE: WARNING: killing 11609 states (over memory cap)
KLEE: WARNING: killing 11927 states (over memory cap)
KLEE: WARNING: killing 11510 states (over memory cap)
KLEE: WARNING: killing 11824 states (over memory cap)
KLEE: WARNING: killing 12379 states (over memory cap)
KLEE: WARNING: killing 11561 states (over memory cap)
KLEE: WARNING: killing 11714 states (over memory cap)
KLEE: WARNING: killing 12107 states (over memory cap)
KLEE: WARNING: killing 11697 states (over memory cap)
KLEE: WARNING: killing 11683 states (over memory cap)
KLEE: WARNING: killing 11593 states (over memory cap)
KLEE: WARNING: killing 11502 states (over memory cap)
KLEE: WARNING: killing 11572 states (over memory cap)
KLEE: WARNING: killing 11560 states (over memory cap)
KLEE: WARNING: killing 11470 states (over memory cap)
KLEE: WARNING: killing 11622 states (over memory cap)
KLEE: WARNING: killing 11529 states (over memory cap)
KLEE: WARNING: killing 11921 states (over memory cap)
KLEE: WARNING: killing 11915 states (over memory cap)
KLEE: WARNING: killing 12224 states (over memory cap)
KLEE: WARNING: killing 11650 states (over memory cap)
KLEE: WARNING: killing 12285 states (over memory cap)
KLEE: WARNING: killing 11795 states (over memory cap)
KLEE: WARNING: killing 11784 states (over memory cap)
KLEE: WARNING: killing 12015 states (over memory cap)
KLEE: WARNING: killing 12005 states (over memory cap)
KLEE: WARNING: killing 11515 states (over memory cap)
KLEE: WARNING: killing 11980 states (over memory cap)
KLEE: WARNING: killing 11652 states (over memory cap)
KLEE: WARNING: killing 11247 states (over memory cap)
KLEE: WARNING: killing 12031 states (over memory cap)
KLEE: WARNING: killing 11626 states (over memory cap)
KLEE: WARNING: killing 11775 states (over memory cap)
KLEE: WARNING: killing 12160 states (over memory cap)
KLEE: WARNING: killing 11596 states (over memory cap)
KLEE: WARNING: killing 11823 states (over memory cap)
KLEE: WARNING: killing 11495 states (over memory cap)
KLEE: WARNING: killing 11724 states (over memory cap)
KLEE: WARNING: killing 11788 states (over memory cap)
KLEE: WARNING: killing 11701 states (over memory cap)
KLEE: WARNING: killing 11768 states (over memory cap)
KLEE: WARNING: killing 11366 states (over memory cap)
KLEE: WARNING: killing 11595 states (over memory cap)
KLEE: WARNING: killing 11583 states (over memory cap)
KLEE: WARNING: killing 11416 states (over memory cap)
KLEE: WARNING: killing 11718 states (over memory cap)
KLEE: WARNING: killing 12334 states (over memory cap)
KLEE: WARNING: killing 11384 states (over memory cap)
KLEE: WARNING: killing 11608 states (over memory cap)
KLEE: WARNING: killing 11601 states (over memory cap)
KLEE: WARNING: killing 11982 states (over memory cap)
KLEE: WARNING: killing 11816 states (over memory cap)
