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--gspca--gspca_main.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.: 114 138 1599 9712
Removed infinite loop in ldv_stop___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.386394023895
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function video_ioctl2 as symbolic
Removed calls to 'module_put' (function is undefined)
Defining function printk as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Removed calls to 'vfree' (function is undefined)
Defining function v4l2_fh_release as symbolic
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Defining function usb_ifnum_to_if as symbolic
Defining function usb_alloc_coherent as symbolic
Defining function usb_set_interface as symbolic
Defining function video_devdata as symbolic
Defining function dev_get_drvdata as symbolic
Defining function try_module_get as symbolic
Defining function v4l2_fh_open as symbolic
Defining function vmalloc_to_page as symbolic
Defining function vm_insert_page as symbolic
Defining function v4l2_ctrl_poll as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function usb_clear_halt as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Defining function vmalloc_32 as symbolic
Defining function ktime_get as symbolic
Defining function ns_to_timeval as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'input_free_device' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function __video_register_device as symbolic
Defining function input_allocate_device as symbolic
Defining function strlcat as symbolic
Defining function input_register_device as symbolic
Defining function dev_set_drvdata as symbolic
Removed calls to 'v4l2_device_disconnect' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Defining function v4l2_device_put as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'video_device_release_empty' (function is undefined)
Defining function ldv_probe_1 as symbolic
Defining function v4l2_ctrl_g_ctrl as symbolic
Defining function v4l2_ctrl_s_ctrl as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  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.466552972794
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 202 145 937 6502
INFO: Starting verification
KLEE: WARNING ONCE: function "dev_open" has inline asm
KLEE: WARNING ONCE: function "dev_close" has inline asm
KLEE: WARNING ONCE: function "vidioc_dqbuf" has inline asm
KLEE: WARNING ONCE: function "gspca_dev_probe2" has inline asm
KLEE: WARNING: undefined reference to function: video_device_release_empty
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 5636 states (over memory cap)
KLEE: WARNING: killing 5313 states (over memory cap)
KLEE: WARNING: killing 5057 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_0fb3ba6d-cc3b-4f36-9a52-8b4d343cb1c5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 5027 states (over memory cap)
KLEE: WARNING: killing 4852 states (over memory cap)
KLEE: WARNING: killing 5423 states (over memory cap)
KLEE: WARNING: killing 5813 states (over memory cap)
KLEE: WARNING: killing 6209 states (over memory cap)
KLEE: WARNING: killing 5107 states (over memory cap)
KLEE: WARNING: killing 5747 states (over memory cap)
KLEE: WARNING: killing 6486 states (over memory cap)
KLEE: WARNING: killing 7039 states (over memory cap)
KLEE: WARNING: killing 5053 states (over memory cap)
KLEE: WARNING: killing 5258 states (over memory cap)
KLEE: WARNING: killing 5464 states (over memory cap)
KLEE: WARNING: killing 5472 states (over memory cap)
KLEE: WARNING: killing 5628 states (over memory cap)
KLEE: WARNING: killing 5934 states (over memory cap)
KLEE: WARNING: killing 5893 states (over memory cap)
KLEE: WARNING: killing 5950 states (over memory cap)
KLEE: WARNING: killing 6157 states (over memory cap)
KLEE: WARNING: killing 6364 states (over memory cap)
KLEE: WARNING: killing 6320 states (over memory cap)
KLEE: WARNING: killing 6728 states (over memory cap)
KLEE: WARNING: killing 6489 states (over memory cap)
KLEE: WARNING: killing 6649 states (over memory cap)
KLEE: WARNING: killing 6908 states (over memory cap)
KLEE: WARNING: killing 7168 states (over memory cap)
KLEE: WARNING: killing 6925 states (over memory cap)
KLEE: WARNING: killing 6930 states (over memory cap)
KLEE: WARNING: killing 6941 states (over memory cap)
KLEE: WARNING: killing 7149 states (over memory cap)
KLEE: WARNING: killing 7103 states (over memory cap)
KLEE: WARNING: killing 6651 states (over memory cap)
KLEE: WARNING: killing 7059 states (over memory cap)
KLEE: WARNING: killing 7112 states (over memory cap)
KLEE: WARNING: killing 7065 states (over memory cap)
KLEE: WARNING: killing 7170 states (over memory cap)
KLEE: WARNING: killing 7326 states (over memory cap)
KLEE: WARNING: killing 7732 states (over memory cap)
KLEE: WARNING: killing 7436 states (over memory cap)
KLEE: WARNING: killing 7288 states (over memory cap)
KLEE: WARNING: killing 7292 states (over memory cap)
KLEE: WARNING: killing 7597 states (over memory cap)
KLEE: WARNING: killing 7605 states (over memory cap)
KLEE: WARNING: killing 7657 states (over memory cap)
KLEE: WARNING: killing 7459 states (over memory cap)
KLEE: WARNING: killing 7565 states (over memory cap)
KLEE: WARNING: killing 7262 states (over memory cap)
KLEE: WARNING: killing 7214 states (over memory cap)
KLEE: WARNING: killing 7669 states (over memory cap)
KLEE: WARNING: killing 7416 states (over memory cap)
KLEE: WARNING: killing 7620 states (over memory cap)
KLEE: WARNING: killing 7569 states (over memory cap)
KLEE: WARNING: killing 7466 states (over memory cap)
KLEE: WARNING: killing 7715 states (over memory cap)
KLEE: WARNING: killing 7663 states (over memory cap)
KLEE: WARNING: killing 7815 states (over memory cap)
KLEE: WARNING: killing 8019 states (over memory cap)
KLEE: WARNING: killing 7915 states (over memory cap)
KLEE: WARNING: killing 8321 states (over memory cap)
KLEE: WARNING: killing 8167 states (over memory cap)
KLEE: WARNING: killing 8365 states (over memory cap)
KLEE: WARNING: killing 9068 states (over memory cap)
