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--usb--stkwebcam--stkwebcam.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.: 111 137 1253 7457
Removed infinite loop in ldv_stop___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.368981838226
Defining function dmi_check_system as symbolic
Defining function printk as symbolic
Defining function usb_control_msg as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function video_ioctl2 as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Defining function v4l2_fh_release as symbolic
Removed calls to 'vfree' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function usb_set_interface as symbolic
Defining function video_devdata as symbolic
Defining function dev_get_drvdata as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function v4l2_fh_open as symbolic
Defining function remap_vmalloc_range as symbolic
Defining function v4l2_ctrl_poll as symbolic
Defining function autoremove_wake_function as symbolic
Defining function _copy_to_user as symbolic
Defining function vmalloc_user as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function __printk_ratelimit as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'v4l2_get_timestamp' (function is undefined)
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 snprintf as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function dev_err as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function usb_get_intf as symbolic
Defining function __video_register_device as symbolic
Defining function dev_set_drvdata as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_reset_resume_1 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function usb_register_driver as symbolic
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_size_t_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.401386976242
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 177 134 715 4566
INFO: Starting verification
KLEE: WARNING ONCE: function "v4l_stk_read" has inline asm
KLEE: WARNING ONCE: function "stk_start_stream" has inline asm
KLEE: WARNING ONCE: function "stk_isoc_handler" has inline asm
KLEE: WARNING ONCE: function "stk_vidioc_dqbuf" has inline asm
KLEE: WARNING ONCE: function "stk_camera_probe" has inline asm
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 6091 states (over memory cap)
KLEE: WARNING: killing 5741 states (over memory cap)
KLEE: WARNING: killing 5517 states (over memory cap)
KLEE: WARNING: killing 5200 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9e9c256d-a327-4f4d-867e-99b7e5daa978/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 5016 states (over memory cap)
KLEE: WARNING: killing 5114 states (over memory cap)
KLEE: WARNING: killing 5677 states (over memory cap)
KLEE: WARNING: killing 5372 states (over memory cap)
KLEE: WARNING: killing 5614 states (over memory cap)
KLEE: WARNING: killing 6773 states (over memory cap)
KLEE: WARNING: killing 6119 states (over memory cap)
KLEE: WARNING: killing 6943 states (over memory cap)
KLEE: WARNING: killing 7886 states (over memory cap)
KLEE: WARNING: killing 5964 states (over memory cap)
KLEE: WARNING: killing 5635 states (over memory cap)
KLEE: WARNING: killing 6037 states (over memory cap)
KLEE: WARNING: killing 5806 states (over memory cap)
KLEE: WARNING: killing 6534 states (over memory cap)
KLEE: WARNING: killing 6950 states (over memory cap)
KLEE: WARNING: killing 7315 states (over memory cap)
KLEE: WARNING: killing 7082 states (over memory cap)
KLEE: WARNING: killing 7334 states (over memory cap)
KLEE: WARNING: killing 7368 states (over memory cap)
KLEE: WARNING: killing 7678 states (over memory cap)
KLEE: WARNING: killing 8044 states (over memory cap)
KLEE: WARNING: killing 8583 states (over memory cap)
KLEE: WARNING: killing 8399 states (over memory cap)
KLEE: WARNING: killing 8659 states (over memory cap)
KLEE: WARNING: killing 8412 states (over memory cap)
KLEE: WARNING: killing 8611 states (over memory cap)
KLEE: WARNING: killing 8464 states (over memory cap)
KLEE: WARNING: killing 8604 states (over memory cap)
KLEE: WARNING: killing 8965 states (over memory cap)
KLEE: WARNING: killing 8928 states (over memory cap)
KLEE: WARNING: killing 8834 states (over memory cap)
KLEE: WARNING: killing 9085 states (over memory cap)
KLEE: WARNING: killing 8986 states (over memory cap)
KLEE: WARNING: killing 8825 states (over memory cap)
KLEE: WARNING: killing 9416 states (over memory cap)
KLEE: WARNING: killing 9661 states (over memory cap)
KLEE: WARNING: killing 9388 states (over memory cap)
KLEE: WARNING: killing 9516 states (over memory cap)
KLEE: WARNING: killing 9350 states (over memory cap)
KLEE: WARNING: killing 9767 states (over memory cap)
KLEE: WARNING: killing 9482 states (over memory cap)
KLEE: WARNING: killing 9725 states (over memory cap)
KLEE: WARNING: killing 9737 states (over memory cap)
KLEE: WARNING: killing 9624 states (over memory cap)
KLEE: WARNING: killing 9743 states (over memory cap)
KLEE: WARNING: killing 9456 states (over memory cap)
KLEE: WARNING: killing 9633 states (over memory cap)
KLEE: WARNING: killing 10224 states (over memory cap)
KLEE: WARNING: killing 9703 states (over memory cap)
KLEE: WARNING: killing 10056 states (over memory cap)
KLEE: WARNING: killing 10113 states (over memory cap)
KLEE: WARNING: killing 10112 states (over memory cap)
KLEE: WARNING: killing 10813 states (over memory cap)
KLEE: WARNING: killing 10872 states (over memory cap)
KLEE: WARNING: killing 11344 states (over memory cap)
KLEE: WARNING: killing 11340 states (over memory cap)
KLEE: WARNING: killing 5978 states (over memory cap)
KLEE: WARNING: killing 5979 states (over memory cap)
KLEE: WARNING: killing 5923 states (over memory cap)
KLEE: WARNING: killing 6153 states (over memory cap)
KLEE: WARNING: killing 6036 states (over memory cap)
KLEE: WARNING: killing 6270 states (over memory cap)
KLEE: WARNING: killing 6094 states (over memory cap)
KLEE: WARNING: killing 6560 states (over memory cap)
KLEE: WARNING: killing 6151 states (over memory cap)
KLEE: WARNING: killing 6266 states (over memory cap)
KLEE: WARNING: killing 6611 states (over memory cap)
KLEE: WARNING: killing 6612 states (over memory cap)
KLEE: WARNING: killing 7077 states (over memory cap)
KLEE: WARNING: killing 6668 states (over memory cap)
KLEE: WARNING: killing 7247 states (over memory cap)
KLEE: WARNING: killing 7773 states (over memory cap)
KLEE: WARNING: killing 7245 states (over memory cap)
KLEE: WARNING: killing 7184 states (over memory cap)
KLEE: WARNING: killing 7765 states (over memory cap)
KLEE: WARNING: killing 7994 states (over memory cap)
KLEE: WARNING: killing 7586 states (over memory cap)
KLEE: WARNING: killing 7929 states (over memory cap)
KLEE: WARNING: killing 8161 states (over memory cap)
KLEE: WARNING: killing 8218 states (over memory cap)
KLEE: WARNING: killing 9089 states (over memory cap)
KLEE: WARNING: killing 8737 states (over memory cap)
KLEE: WARNING: killing 8441 states (over memory cap)
KLEE: WARNING: killing 8904 states (over memory cap)
KLEE: WARNING: killing 9131 states (over memory cap)
KLEE: WARNING: killing 9069 states (over memory cap)
KLEE: WARNING: killing 8891 states (over memory cap)
