bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-common-saa7146-saa7146_vv_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.: 426 333 3154 22814
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.747408866882
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'v4l2_video_std_frame_period' (function is undefined)
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function printk as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'video_device_release' (function is undefined)
Defining function video_device_alloc as symbolic
Defining function strlcpy as symbolic
Defining function __video_register_device as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Defining function video_devdata as symbolic
Defining function videobuf_mmap_mapper as symbolic
Defining function v4l2_ctrl_poll as symbolic
Defining function videobuf_poll_stream as symbolic
Defining function video_ioctl2 as symbolic
Removed calls to 'videobuf_queue_sg_init' (function is undefined)
Removed calls to 'videobuf_stop' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function videobuf_read_one as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'v4l2_get_timestamp' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function del_timer as symbolic
Removed calls to 'saa7146_pgtable_free' (function is undefined)
Defining function saa7146_pgtable_alloc as symbolic
Defining function videobuf_iolock as symbolic
Defining function mod_timer as symbolic
Defining function videobuf_to_dma as symbolic
Defining function saa7146_pgtable_build_single as symbolic
Defining function videobuf_waiton as symbolic
Defining function videobuf_dma_unmap as symbolic
Defining function videobuf_dma_free as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function videobuf_read_stream as symbolic
Removed calls to 'videobuf_queue_cancel' (function is undefined)
Defining function default_wake_function as symbolic
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 'module_put' (function is undefined)
Defining function try_module_get as symbolic
Defining function videobuf_streamoff as symbolic
Defining function videobuf_streamon as symbolic
Defining function capable as symbolic
Defining function videobuf_dqbuf as symbolic
Defining function videobuf_qbuf as symbolic
Defining function videobuf_querybuf as symbolic
Defining function videobuf_reqbufs as symbolic
Defining function _copy_from_user as symbolic
Defining function sprintf as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcpy
  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.666007041931
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 274 307 1238 9830
INFO: Starting verification
KLEE: WARNING ONCE: function "saa7146_vv_init" has inline asm
KLEE: WARNING ONCE: function "vv_callback" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "saa7146_register_device" has inline asm
KLEE: WARNING ONCE: function "saa7146_s_ctrl" has inline asm
KLEE: WARNING ONCE: function "saa7146_stop_preview" has inline asm
KLEE: WARNING ONCE: function "saa7146_start_preview" has inline asm
KLEE: WARNING ONCE: function "saa7146_enable_overlay" has inline asm
KLEE: WARNING ONCE: function "saa7146_set_window" has inline asm
KLEE: WARNING ONCE: function "saa7146_write_out_dma" has inline asm
KLEE: WARNING ONCE: function "fops_mmap" has inline asm
KLEE: WARNING ONCE: function "fops_write" has inline asm
KLEE: WARNING ONCE: function "video_begin" has inline asm
KLEE: WARNING ONCE: function "video_end" has inline asm
KLEE: WARNING ONCE: function "SAA7146_IER_DISABLE" has inline asm
KLEE: WARNING ONCE: function "saa7146_res_free" has inline asm
KLEE: WARNING ONCE: function "SAA7146_IER_ENABLE" has inline asm
KLEE: WARNING ONCE: function "saa7146_buffer_finish" has inline asm
KLEE: WARNING ONCE: function "saa7146_buffer_next" has inline asm
KLEE: WARNING ONCE: function "saa7146_dma_free" has inline asm
KLEE: WARNING ONCE: function "saa7146_set_capture" has inline asm
KLEE: WARNING ONCE: function "saa7146_buffer_queue" has inline asm
KLEE: WARNING ONCE: function "saa7146_set_hps_source_and_sync" has inline asm
KLEE: WARNING ONCE: function "vbi_open" has inline asm
KLEE: WARNING ONCE: function "vbi_close" has inline asm
KLEE: WARNING ONCE: function "vbi_stop" has inline asm
KLEE: WARNING ONCE: function "fops_read" has inline asm
KLEE: WARNING ONCE: function "buffer_activate___0" has inline asm
KLEE: WARNING ONCE: function "saa7146_disable_overlay" has inline asm
KLEE: WARNING: undefined reference to function: video_device_release
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_fb24f295-36fd-45ae-9a63-4433606f704f/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 21611 states (over memory cap)
KLEE: WARNING: killing 11373 states (over memory cap)
KLEE: WARNING: killing 21574 states (over memory cap)
KLEE: WARNING: killing 20151 states (over memory cap)
KLEE: WARNING: killing 19977 states (over memory cap)
KLEE: WARNING: killing 19578 states (over memory cap)
KLEE: WARNING: killing 21059 states (over memory cap)
KLEE: WARNING: killing 20883 states (over memory cap)
KLEE: WARNING: killing 10998 states (over memory cap)
KLEE: WARNING: killing 20882 states (over memory cap)
KLEE: WARNING: killing 11492 states (over memory cap)
KLEE: WARNING: killing 11361 states (over memory cap)
KLEE: WARNING: killing 11020 states (over memory cap)
KLEE: WARNING: killing 11214 states (over memory cap)
KLEE: WARNING: killing 11303 states (over memory cap)
KLEE: WARNING: killing 11394 states (over memory cap)
KLEE: WARNING: killing 11705 states (over memory cap)
KLEE: WARNING: killing 12334 states (over memory cap)
KLEE: WARNING: killing 11561 states (over memory cap)
KLEE: WARNING: killing 12084 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 11619 states (over memory cap)
KLEE: WARNING: killing 12030 states (over memory cap)
KLEE: WARNING: killing 12014 states (over memory cap)
KLEE: WARNING: killing 11787 states (over memory cap)
KLEE: WARNING: killing 11873 states (over memory cap)
KLEE: WARNING: killing 11326 states (over memory cap)
KLEE: WARNING: killing 11630 states (over memory cap)
KLEE: WARNING: killing 11509 states (over memory cap)
KLEE: WARNING: killing 11069 states (over memory cap)
KLEE: WARNING: killing 11476 states (over memory cap)
KLEE: WARNING: killing 11042 states (over memory cap)
KLEE: WARNING: killing 10709 states (over memory cap)
KLEE: WARNING: killing 10908 states (over memory cap)
KLEE: WARNING: killing 11104 states (over memory cap)
KLEE: WARNING: killing 11089 states (over memory cap)
KLEE: WARNING: killing 11283 states (over memory cap)
KLEE: WARNING: killing 10953 states (over memory cap)
KLEE: WARNING: killing 10944 states (over memory cap)
KLEE: WARNING: killing 11139 states (over memory cap)
KLEE: WARNING: killing 11232 states (over memory cap)
KLEE: WARNING: killing 11218 states (over memory cap)
KLEE: WARNING: killing 11199 states (over memory cap)
KLEE: WARNING: killing 10773 states (over memory cap)
KLEE: WARNING: killing 11068 states (over memory cap)
KLEE: WARNING: killing 10951 states (over memory cap)
KLEE: WARNING: killing 10830 states (over memory cap)
KLEE: WARNING: killing 11131 states (over memory cap)
KLEE: WARNING: killing 11531 states (over memory cap)
KLEE: WARNING: killing 11002 states (over memory cap)
KLEE: WARNING: killing 10986 states (over memory cap)
KLEE: WARNING: killing 11797 states (over memory cap)
KLEE: WARNING: killing 10961 states (over memory cap)
KLEE: WARNING: killing 11258 states (over memory cap)
KLEE: WARNING: killing 11247 states (over memory cap)
KLEE: WARNING: killing 11024 states (over memory cap)
KLEE: WARNING: killing 11120 states (over memory cap)
KLEE: WARNING: killing 10897 states (over memory cap)
KLEE: WARNING: killing 11193 states (over memory cap)
KLEE: WARNING: killing 11284 states (over memory cap)
KLEE: WARNING: killing 11167 states (over memory cap)
KLEE: WARNING: killing 10849 states (over memory cap)
KLEE: WARNING: killing 10835 states (over memory cap)
KLEE: WARNING: killing 11031 states (over memory cap)
KLEE: WARNING: killing 11218 states (over memory cap)
KLEE: WARNING: killing 10901 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 10981 states (over memory cap)
KLEE: WARNING: killing 10563 states (over memory cap)
KLEE: WARNING: killing 11360 states (over memory cap)
KLEE: WARNING: killing 11143 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10817 states (over memory cap)
KLEE: WARNING: killing 11108 states (over memory cap)
KLEE: WARNING: killing 11194 states (over memory cap)
KLEE: WARNING: killing 11088 states (over memory cap)
KLEE: WARNING: killing 10770 states (over memory cap)
KLEE: WARNING: killing 10962 states (over memory cap)
KLEE: WARNING: killing 11452 states (over memory cap)
KLEE: WARNING: killing 11139 states (over memory cap)
KLEE: WARNING: killing 11527 states (over memory cap)
KLEE: WARNING: killing 11514 states (over memory cap)
KLEE: WARNING: killing 10703 states (over memory cap)
KLEE: WARNING: killing 11289 states (over memory cap)
KLEE: WARNING: killing 11277 states (over memory cap)
KLEE: WARNING: killing 11459 states (over memory cap)
KLEE: WARNING: killing 11152 states (over memory cap)
KLEE: WARNING: killing 11042 states (over memory cap)
KLEE: WARNING: killing 11129 states (over memory cap)
KLEE: WARNING: killing 11121 states (over memory cap)
KLEE: WARNING: killing 10611 states (over memory cap)
KLEE: WARNING: killing 11293 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 11069 states (over memory cap)
KLEE: WARNING: killing 11161 states (over memory cap)
KLEE: WARNING: killing 11053 states (over memory cap)
KLEE: WARNING: killing 11143 states (over memory cap)
KLEE: WARNING: killing 11030 states (over memory cap)
KLEE: WARNING: killing 11311 states (over memory cap)
KLEE: WARNING: killing 11208 states (over memory cap)
KLEE: WARNING: killing 10903 states (over memory cap)
KLEE: WARNING: killing 11580 states (over memory cap)
KLEE: WARNING: killing 11082 states (over memory cap)
KLEE: WARNING: killing 10678 states (over memory cap)
KLEE: WARNING: killing 11052 states (over memory cap)
KLEE: WARNING: killing 11630 states (over memory cap)
KLEE: WARNING: killing 10935 states (over memory cap)
KLEE: WARNING: killing 10338 states (over memory cap)
KLEE: WARNING: killing 11399 states (over memory cap)
KLEE: WARNING: killing 11098 states (over memory cap)
KLEE: WARNING: killing 11768 states (over memory cap)
KLEE: WARNING: killing 11174 states (over memory cap)
KLEE: WARNING: killing 10965 states (over memory cap)
KLEE: WARNING: killing 10569 states (over memory cap)
KLEE: WARNING: killing 11237 states (over memory cap)
KLEE: WARNING: killing 11230 states (over memory cap)
KLEE: WARNING: killing 11021 states (over memory cap)
KLEE: WARNING: killing 11207 states (over memory cap)
KLEE: WARNING: killing 11099 states (over memory cap)
KLEE: WARNING: killing 10992 states (over memory cap)
KLEE: WARNING: killing 11077 states (over memory cap)
KLEE: WARNING: killing 11162 states (over memory cap)
KLEE: WARNING: killing 11253 states (over memory cap)
KLEE: WARNING: killing 11238 states (over memory cap)
KLEE: WARNING: killing 11036 states (over memory cap)
KLEE: WARNING: killing 11215 states (over memory cap)
KLEE: WARNING: killing 11202 states (over memory cap)
KLEE: WARNING: killing 11096 states (over memory cap)
KLEE: WARNING: killing 11086 states (over memory cap)
KLEE: WARNING: killing 10788 states (over memory cap)
KLEE: WARNING: killing 10590 states (over memory cap)
KLEE: WARNING: killing 11055 states (over memory cap)
KLEE: WARNING: killing 11137 states (over memory cap)
KLEE: WARNING: killing 10938 states (over memory cap)
KLEE: WARNING: killing 11212 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-QLF8vF/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-common-saa7146-saa7146_vv_true-unreach-call.cil.c:16961: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11203 states (over memory cap)
KLEE: WARNING: killing 11388 states (over memory cap)
KLEE: WARNING: killing 11089 states (over memory cap)
KLEE: WARNING: killing 11076 states (over memory cap)
KLEE: WARNING: killing 10876 states (over memory cap)
KLEE: WARNING: killing 10679 states (over memory cap)
KLEE: WARNING: killing 11045 states (over memory cap)
KLEE: WARNING: killing 11134 states (over memory cap)
KLEE: WARNING: killing 10930 states (over memory cap)
KLEE: WARNING: killing 11207 states (over memory cap)
KLEE: WARNING: killing 11194 states (over memory cap)
KLEE: WARNING: killing 10807 states (over memory cap)
KLEE: WARNING: killing 10796 states (over memory cap)
KLEE: WARNING: killing 10788 states (over memory cap)
KLEE: WARNING: killing 11340 states (over memory cap)
KLEE: WARNING: killing 10862 states (over memory cap)
KLEE: WARNING: killing 11415 states (over memory cap)
KLEE: WARNING: killing 11125 states (over memory cap)
KLEE: WARNING: killing 11298 states (over memory cap)
KLEE: WARNING: killing 11196 states (over memory cap)
KLEE: WARNING: killing 11186 states (over memory cap)
KLEE: WARNING: killing 11273 states (over memory cap)
KLEE: WARNING: killing 10795 states (over memory cap)
KLEE: WARNING: killing 11248 states (over memory cap)
KLEE: WARNING: killing 10867 states (over memory cap)
KLEE: WARNING: killing 10481 states (over memory cap)
KLEE: WARNING: killing 11122 states (over memory cap)
KLEE: WARNING: killing 11210 states (over memory cap)
KLEE: WARNING: killing 11108 states (over memory cap)
KLEE: WARNING: killing 10909 states (over memory cap)
KLEE: WARNING: killing 10718 states (over memory cap)
KLEE: WARNING: killing 10983 states (over memory cap)
KLEE: WARNING: killing 10698 states (over memory cap)
KLEE: WARNING: killing 10593 states (over memory cap)
KLEE: WARNING: killing 10956 states (over memory cap)
KLEE: WARNING: killing 11499 states (over memory cap)
KLEE: WARNING: killing 11032 states (over memory cap)
KLEE: WARNING: killing 10837 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-QLF8vF/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-common-saa7146-saa7146_vv_true-unreach-call.cil.c:13681: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11190 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-QLF8vF/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-common-saa7146-saa7146_vv_true-unreach-call.cil.c:13723: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10721 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-QLF8vF/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-common-saa7146-saa7146_vv_true-unreach-call.cil.c:13442: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11445 states (over memory cap)
