bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-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.: 886 752 6839 42177
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.4012761116
Removed calls to '__symbol_put' (function is undefined)
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function printk as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'v4l2_device_disconnect' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function kmemdup as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function usb_alloc_urb as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function scnprintf as symbolic
Removed calls to 'cx2341x_log_status' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function usb_submit_urb as symbolic
Defining function usb_unlink_urb as symbolic
Defining function hex_to_bin as symbolic
Defining function i2c_transfer as symbolic
Defining function request_firmware as symbolic
Defining function usb_lock_device_for_reset as symbolic
Defining function usb_reset_device as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function simple_strtol as symbolic
Defining function kthread_stop as symbolic
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_arg' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function cx2341x_update as symbolic
Removed calls to 'v4l_printk_ioctl' (function is undefined)
Defining function video_devdata as symbolic
Defining function v4l2_prio_check as symbolic
Defining function video_ioctl2 as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function strlcpy as symbolic
Defining function v4l2_prio_change as symbolic
Defining function v4l2_prio_max as symbolic
Defining function i2c_add_adapter as symbolic
Defining function i2c_new_device as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Removed calls to 'v4l2_prio_close' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function usb_clear_halt as symbolic
Defining function v4l2_i2c_new_subdev as symbolic
Removed calls to 'class_unregister' (function is undefined)
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncpy
  __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: 1.13083600998
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 795 469 3048 17557
INFO: Starting verification
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_5b9a1012-9ca4-4f88-b1e6-a697471f1d1a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10577 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16141 states (over memory cap)
KLEE: WARNING: killing 16093 states (over memory cap)
KLEE: WARNING: killing 15520 states (over memory cap)
KLEE: WARNING: killing 14945 states (over memory cap)
KLEE: WARNING: killing 14295 states (over memory cap)
KLEE: WARNING: killing 15019 states (over memory cap)
KLEE: WARNING: killing 14529 states (over memory cap)
KLEE: WARNING: killing 14571 states (over memory cap)
KLEE: WARNING: killing 14694 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 15311 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 16682 states (over memory cap)
KLEE: WARNING: killing 16583 states (over memory cap)
KLEE: WARNING: killing 16554 states (over memory cap)
KLEE: WARNING: killing 16974 states (over memory cap)
KLEE: WARNING: killing 16582 states (over memory cap)
KLEE: WARNING: killing 16785 states (over memory cap)
KLEE: WARNING: killing 17284 states (over memory cap)
KLEE: WARNING: killing 17119 states (over memory cap)
KLEE: WARNING: killing 16358 states (over memory cap)
KLEE: WARNING: killing 17070 states (over memory cap)
KLEE: WARNING: killing 16613 states (over memory cap)
KLEE: WARNING: killing 17029 states (over memory cap)
KLEE: WARNING: killing 16194 states (over memory cap)
KLEE: WARNING: killing 16022 states (over memory cap)
KLEE: WARNING: killing 15853 states (over memory cap)
KLEE: WARNING: killing 16197 states (over memory cap)
KLEE: WARNING: killing 16324 states (over memory cap)
KLEE: WARNING: killing 16297 states (over memory cap)
KLEE: WARNING: killing 16420 states (over memory cap)
KLEE: WARNING: killing 16036 states (over memory cap)
KLEE: WARNING: killing 16594 states (over memory cap)
KLEE: WARNING: killing 16422 states (over memory cap)
KLEE: WARNING: killing 16257 states (over memory cap)
KLEE: WARNING: killing 16820 states (over memory cap)
KLEE: WARNING: killing 15776 states (over memory cap)
KLEE: WARNING: killing 16986 states (over memory cap)
KLEE: WARNING: killing 16901 states (over memory cap)
KLEE: WARNING: killing 16732 states (over memory cap)
KLEE: WARNING: killing 17216 states (over memory cap)
KLEE: WARNING: killing 16833 states (over memory cap)
KLEE: WARNING: killing 16167 states (over memory cap)
KLEE: WARNING: killing 16364 states (over memory cap)
KLEE: WARNING: killing 16914 states (over memory cap)
KLEE: WARNING: killing 16468 states (over memory cap)
KLEE: WARNING: killing 16731 states (over memory cap)
KLEE: WARNING: killing 16925 states (over memory cap)
KLEE: WARNING: killing 15975 states (over memory cap)
KLEE: WARNING: killing 16382 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 16622 states (over memory cap)
KLEE: WARNING: killing 16890 states (over memory cap)
KLEE: WARNING: killing 17369 states (over memory cap)
KLEE: WARNING: killing 16710 states (over memory cap)
KLEE: WARNING: killing 16768 states (over memory cap)
KLEE: WARNING: killing 16109 states (over memory cap)
KLEE: WARNING: killing 16582 states (over memory cap)
KLEE: WARNING: killing 16274 states (over memory cap)
KLEE: WARNING: killing 16683 states (over memory cap)
KLEE: WARNING: killing 16528 states (over memory cap)
KLEE: WARNING: killing 16931 states (over memory cap)
KLEE: WARNING: killing 16988 states (over memory cap)
KLEE: WARNING: killing 16968 states (over memory cap)
KLEE: WARNING: killing 17021 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 16010 states (over memory cap)
KLEE: WARNING: killing 16205 states (over memory cap)
KLEE: WARNING: killing 16251 states (over memory cap)
KLEE: WARNING: killing 16162 states (over memory cap)
KLEE: WARNING: killing 16706 states (over memory cap)
KLEE: WARNING: killing 16616 states (over memory cap)
KLEE: WARNING: killing 16738 states (over memory cap)
KLEE: WARNING: killing 16518 states (over memory cap)
KLEE: WARNING: killing 16493 states (over memory cap)
KLEE: WARNING: killing 16412 states (over memory cap)
KLEE: WARNING: killing 15554 states (over memory cap)
KLEE: WARNING: killing 16932 states (over memory cap)
KLEE: WARNING: killing 16501 states (over memory cap)
KLEE: WARNING: killing 16759 states (over memory cap)
KLEE: WARNING: killing 16959 states (over memory cap)
KLEE: WARNING: killing 16870 states (over memory cap)
KLEE: WARNING: killing 16583 states (over memory cap)
KLEE: WARNING: killing 16354 states (over memory cap)
KLEE: WARNING: killing 16476 states (over memory cap)
KLEE: WARNING: killing 16320 states (over memory cap)
KLEE: WARNING: killing 16791 states (over memory cap)
KLEE: WARNING: killing 16086 states (over memory cap)
KLEE: WARNING: killing 16267 states (over memory cap)
KLEE: WARNING: killing 17006 states (over memory cap)
KLEE: WARNING: killing 16582 states (over memory cap)
KLEE: WARNING: killing 16909 states (over memory cap)
KLEE: WARNING: killing 16622 states (over memory cap)
KLEE: WARNING: killing 16813 states (over memory cap)
KLEE: WARNING: killing 15563 states (over memory cap)
KLEE: WARNING: killing 15952 states (over memory cap)
KLEE: WARNING: killing 16899 states (over memory cap)
KLEE: WARNING: killing 17154 states (over memory cap)
KLEE: WARNING: killing 16736 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 16294 states (over memory cap)
KLEE: WARNING: killing 15865 states (over memory cap)
KLEE: WARNING: killing 16666 states (over memory cap)
KLEE: WARNING: killing 17330 states (over memory cap)
KLEE: WARNING: killing 15957 states (over memory cap)
KLEE: WARNING: killing 17160 states (over memory cap)
KLEE: WARNING: killing 17017 states (over memory cap)
KLEE: WARNING: killing 16663 states (over memory cap)
KLEE: WARNING: killing 16171 states (over memory cap)
KLEE: WARNING: killing 16160 states (over memory cap)
KLEE: WARNING: killing 16745 states (over memory cap)
KLEE: WARNING: killing 16604 states (over memory cap)
KLEE: WARNING: killing 16523 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 16827 states (over memory cap)
KLEE: WARNING: killing 16876 states (over memory cap)
KLEE: WARNING: killing 16391 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25057: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16512 states (over memory cap)
KLEE: WARNING: killing 16226 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25420: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16607 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25143: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25372: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16935 states (over memory cap)
KLEE: WARNING: killing 16517 states (over memory cap)
KLEE: WARNING: killing 17175 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25153: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25328: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16895 states (over memory cap)
KLEE: WARNING: killing 16685 states (over memory cap)
KLEE: WARNING: killing 16200 states (over memory cap)
KLEE: WARNING: killing 16318 states (over memory cap)
KLEE: WARNING: killing 16634 states (over memory cap)
KLEE: WARNING: killing 16555 states (over memory cap)
KLEE: WARNING: killing 16465 states (over memory cap)
KLEE: WARNING: killing 16781 states (over memory cap)
KLEE: WARNING: killing 17173 states (over memory cap)
KLEE: WARNING: killing 16163 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:9458: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:24908: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:24958: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16741 states (over memory cap)
KLEE: WARNING: killing 17058 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:21820: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17176 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:22147: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16827 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:21664: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16553 states (over memory cap)
KLEE: WARNING: killing 16471 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:24918: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16393 states (over memory cap)
KLEE: WARNING: killing 17037 states (over memory cap)
KLEE: WARNING: killing 16760 states (over memory cap)
KLEE: WARNING: killing 17081 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XcmBVk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--pvrusb2--pvrusb2.ko-entry_point_true-unreach-call.cil.out.c:25318: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16605 states (over memory cap)
KLEE: WARNING: killing 16258 states (over memory cap)
KLEE: WARNING: killing 16233 states (over memory cap)
KLEE: WARNING: killing 16418 states (over memory cap)
KLEE: WARNING: killing 16332 states (over memory cap)
