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-mutex__drivers-media-usb-pwc-pwc_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.: 299 284 2593 14964
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.577301979065
Removed calls to 'vfree' (function is undefined)
Defining function vb2_plane_vaddr as symbolic
Defining function printk as symbolic
Defining function vzalloc as symbolic
Removed calls to 'vb2_buffer_done' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function usb_ifnum_to_if as symbolic
Defining function usb_altnum_to_altsetting as symbolic
Defining function usb_set_interface as symbolic
Defining function usb_alloc_urb as symbolic
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Defining function usb_alloc_coherent as symbolic
Removed calls to 'v4l2_get_timestamp' (function is undefined)
Defining function usb_submit_urb as symbolic
Removed calls to 'input_event' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function usb_control_msg as symbolic
Defining function vb2_fop_mmap as symbolic
Defining function vb2_fop_poll as symbolic
Defining function vb2_fop_read as symbolic
Defining function video_ioctl2 as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Defining function vb2_ioctl_reqbufs as symbolic
Defining function vb2_ioctl_querybuf as symbolic
Defining function vb2_ioctl_qbuf as symbolic
Defining function vb2_ioctl_dqbuf as symbolic
Defining function vb2_ioctl_streamon as symbolic
Defining function vb2_ioctl_streamoff as symbolic
Defining function v4l2_ctrl_log_status as symbolic
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Defining function video_devdata as symbolic
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (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 'video_unregister_device' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_device_disconnect' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Defining function v4l2_device_put as symbolic
Defining function usb_string as symbolic
Defining function vb2_queue_init as symbolic
Removed calls to 'v4l2_ctrl_auto_cluster' (function is undefined)
Removed calls to 'v4l2_ctrl_cluster' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function input_allocate_device as symbolic
Defining function strlcat as symbolic
Defining function input_register_device as symbolic
Defining function __video_register_device as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_get_name as symbolic
Defining function v4l2_ctrl_new_custom as symbolic
Defining function v4l2_ctrl_new_std_menu as symbolic
Defining function v4l2_fh_open as symbolic
Defining function vb2_fop_release as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'vb2_ops_wait_finish' (function is undefined)
Removed calls to 'vb2_ops_wait_prepare' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'video_device_release_empty' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  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: 0.558999061584
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 365 279 1350 8448
INFO: Starting verification
KLEE: WARNING ONCE: function "usb_pwc_probe" has inline asm
KLEE: WARNING: undefined reference to function: vb2_ops_wait_finish
KLEE: WARNING: undefined reference to function: vb2_ops_wait_prepare
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fa759a5-887f-4fff-96ea-5f85349ae48c/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: ERROR: /tmp/symbiotic-ja1fzT/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-usb-pwc-pwc_true-unreach-call.cil.c:6993: 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 15477 states (over memory cap)
KLEE: WARNING: killing 16250 states (over memory cap)
KLEE: WARNING: killing 15909 states (over memory cap)
KLEE: WARNING: killing 15162 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 16146 states (over memory cap)
KLEE: WARNING: killing 15959 states (over memory cap)
KLEE: WARNING: killing 16311 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: WARNING: killing 16210 states (over memory cap)
KLEE: WARNING: killing 16423 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 16192 states (over memory cap)
KLEE: WARNING: killing 16939 states (over memory cap)
KLEE: WARNING: killing 16758 states (over memory cap)
KLEE: WARNING: killing 16847 states (over memory cap)
KLEE: WARNING: killing 17602 states (over memory cap)
KLEE: WARNING: killing 17287 states (over memory cap)
KLEE: WARNING: killing 17243 states (over memory cap)
KLEE: WARNING: killing 17196 states (over memory cap)
KLEE: WARNING: killing 17153 states (over memory cap)
KLEE: WARNING: killing 16849 states (over memory cap)
KLEE: WARNING: killing 17072 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ja1fzT/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-usb-pwc-pwc_true-unreach-call.cil.c:8298: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16891 states (over memory cap)
KLEE: WARNING: killing 16334 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ja1fzT/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-usb-pwc-pwc_true-unreach-call.cil.c:6858: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16672 states (over memory cap)
KLEE: WARNING: killing 17016 states (over memory cap)
KLEE: WARNING: killing 16464 states (over memory cap)
KLEE: WARNING: killing 17068 states (over memory cap)
KLEE: WARNING: killing 16128 states (over memory cap)
KLEE: WARNING: killing 16345 states (over memory cap)
KLEE: WARNING: killing 16313 states (over memory cap)
KLEE: WARNING: killing 16142 states (over memory cap)
KLEE: WARNING: killing 15983 states (over memory cap)
KLEE: WARNING: killing 16578 states (over memory cap)
KLEE: WARNING: killing 16160 states (over memory cap)
KLEE: WARNING: killing 16374 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ja1fzT/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-usb-pwc-pwc_true-unreach-call.cil.c:6893: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16596 states (over memory cap)
KLEE: WARNING: killing 16298 states (over memory cap)
KLEE: WARNING: killing 15890 states (over memory cap)
KLEE: WARNING: killing 15979 states (over memory cap)
KLEE: WARNING: killing 15937 states (over memory cap)
KLEE: WARNING: killing 16160 states (over memory cap)
KLEE: WARNING: killing 16493 states (over memory cap)
KLEE: WARNING: killing 16466 states (over memory cap)
KLEE: WARNING: killing 16803 states (over memory cap)
KLEE: WARNING: killing 16393 states (over memory cap)
KLEE: WARNING: killing 16231 states (over memory cap)
KLEE: WARNING: killing 16570 states (over memory cap)
KLEE: WARNING: killing 16417 states (over memory cap)
KLEE: WARNING: killing 16145 states (over memory cap)
KLEE: WARNING: killing 16113 states (over memory cap)
KLEE: WARNING: killing 16322 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 16261 states (over memory cap)
KLEE: WARNING: killing 16343 states (over memory cap)
KLEE: WARNING: killing 16429 states (over memory cap)
KLEE: WARNING: killing 16034 states (over memory cap)
KLEE: WARNING: killing 15994 states (over memory cap)
KLEE: WARNING: killing 16444 states (over memory cap)
KLEE: WARNING: killing 16294 states (over memory cap)
KLEE: WARNING: killing 16510 states (over memory cap)
KLEE: WARNING: killing 16592 states (over memory cap)
KLEE: WARNING: killing 15964 states (over memory cap)
KLEE: WARNING: killing 15940 states (over memory cap)
KLEE: WARNING: killing 15549 states (over memory cap)
KLEE: WARNING: killing 15996 states (over memory cap)
KLEE: WARNING: killing 16084 states (over memory cap)
KLEE: WARNING: killing 16412 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 16347 states (over memory cap)
KLEE: WARNING: killing 16202 states (over memory cap)
KLEE: WARNING: killing 15929 states (over memory cap)
KLEE: WARNING: killing 16266 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: WARNING: killing 16092 states (over memory cap)
KLEE: WARNING: killing 16407 states (over memory cap)
KLEE: WARNING: killing 16610 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
KLEE: WARNING: killing 16056 states (over memory cap)
KLEE: WARNING: killing 16028 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 15854 states (over memory cap)
KLEE: WARNING: killing 15946 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ja1fzT/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-usb-pwc-pwc_true-unreach-call.cil.c:6943: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16022 states (over memory cap)
KLEE: WARNING: killing 15874 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ja1fzT/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-usb-pwc-pwc_true-unreach-call.cil.c:11976: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16075 states (over memory cap)
