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-usb-dev__drivers-media-platform-vsp1-vsp1_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.: 396 521 3395 19917
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.70636510849
Removed calls to 'iowrite32' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'v4l2_get_timestamp' (function is undefined)
Removed calls to 'vb2_buffer_done' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function ioread32 as symbolic
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function __platform_driver_register as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'clk_disable' (function is undefined)
Removed calls to 'clk_unprepare' (function is undefined)
Defining function clk_prepare as symbolic
Defining function clk_enable as symbolic
Defining function v4l2_subdev_link_validate as symbolic
Defining function vb2_plane_cookie as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'media_entity_pipeline_stop' (function is undefined)
Defining function dev_err as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function vb2_fop_mmap as symbolic
Defining function vb2_fop_poll as symbolic
Defining function video_ioctl2 as symbolic
Defining function vb2_ioctl_create_bufs as symbolic
Defining function vb2_ioctl_dqbuf as symbolic
Defining function vb2_ioctl_prepare_buf as symbolic
Defining function vb2_ioctl_qbuf as symbolic
Defining function vb2_ioctl_querybuf as symbolic
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Defining function vb2_ioctl_reqbufs as symbolic
Defining function vb2_ioctl_streamoff as symbolic
Removed calls to 'media_entity_graph_walk_start' (function is undefined)
Defining function media_entity_pipeline_start as symbolic
Defining function vb2_streamon as symbolic
Defining function media_entity_graph_walk_next as symbolic
Defining function media_entity_remote_pad as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'media_device_unregister' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'media_entity_cleanup' (function is undefined)
Defining function platform_get_resource as symbolic
Defining function devm_ioremap_resource as symbolic
Defining function devm_clk_get as symbolic
Defining function media_device_register as symbolic
Defining function v4l2_device_register as symbolic
Removed calls to 'v4l2_subdev_init' (function is undefined)
Defining function media_entity_create_link as symbolic
Defining function v4l2_device_register_subdev_nodes as symbolic
Defining function v4l2_device_register_subdev as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'vb2_dma_contig_cleanup_ctx' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Defining function media_entity_init as symbolic
Defining function vb2_dma_contig_init_ctx as symbolic
Defining function vb2_queue_init as symbolic
Defining function __video_register_device as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_custom as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Defining function devm_request_threaded_irq as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
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 'vb2_queue_release' (function is undefined)
Defining function v4l2_fh_release as symbolic
Defining function video_devdata as symbolic
Removed calls to 'usleep_range' (function is undefined)
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_pre_probe' (function is undefined)
Removed calls to 'vb2_ops_wait_finish' (function is undefined)
Removed calls to 'vb2_ops_wait_prepare' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  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.679730892181
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 496 469 1601 11556
INFO: Starting verification
KLEE: WARNING ONCE: function "vsp1_rwpf_get_selection" has inline asm
KLEE: WARNING ONCE: function "vsp1_rwpf_set_selection" has inline asm
KLEE: WARNING ONCE: function "vsp1_rwpf_enum_frame_size" has inline asm
KLEE: WARNING ONCE: function "vsp1_entity_get_pad_format" has inline asm
KLEE: WARNING ONCE: function "vsp1_rwpf_set_format" has inline asm
KLEE: WARNING ONCE: function "hsit_enum_frame_size" has inline asm
KLEE: WARNING ONCE: function "hsit_set_format" has inline asm
KLEE: WARNING ONCE: function "lif_enum_frame_size" has inline asm
KLEE: WARNING ONCE: function "lif_enum_mbus_code" has inline asm
KLEE: WARNING ONCE: function "lif_set_format" has inline asm
KLEE: WARNING ONCE: function "lut_enum_frame_size" has inline asm
KLEE: WARNING ONCE: function "lut_enum_mbus_code" has inline asm
KLEE: WARNING ONCE: function "lut_set_format" has inline asm
KLEE: WARNING ONCE: function "sru_enum_frame_size" has inline asm
KLEE: WARNING ONCE: function "sru_enum_mbus_code" has inline asm
KLEE: WARNING ONCE: function "sru_set_format" has inline asm
KLEE: WARNING ONCE: function "sru_try_format" has inline asm
KLEE: WARNING ONCE: function "uds_enum_frame_size" has inline asm
KLEE: WARNING ONCE: function "uds_enum_mbus_code" has inline asm
KLEE: WARNING ONCE: function "uds_set_format" has inline asm
KLEE: WARNING ONCE: function "uds_try_format" 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_325b4380-acc7-4fba-ad40-1f9afd0e79da/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: killing 26104 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 26272 states (over memory cap)
KLEE: WARNING: killing 24409 states (over memory cap)
KLEE: WARNING: killing 22828 states (over memory cap)
KLEE: WARNING: killing 22767 states (over memory cap)
KLEE: WARNING: killing 22832 states (over memory cap)
KLEE: WARNING: killing 22151 states (over memory cap)
KLEE: WARNING: killing 21973 states (over memory cap)
KLEE: WARNING: killing 21050 states (over memory cap)
KLEE: WARNING: killing 22257 states (over memory cap)
KLEE: WARNING: killing 21346 states (over memory cap)
KLEE: WARNING: killing 22056 states (over memory cap)
KLEE: WARNING: killing 23748 states (over memory cap)
KLEE: WARNING: killing 23969 states (over memory cap)
KLEE: WARNING: killing 23057 states (over memory cap)
KLEE: WARNING: killing 22634 states (over memory cap)
KLEE: WARNING: killing 23468 states (over memory cap)
KLEE: WARNING: killing 25155 states (over memory cap)
KLEE: WARNING: killing 24501 states (over memory cap)
KLEE: WARNING: killing 24952 states (over memory cap)
KLEE: WARNING: killing 25287 states (over memory cap)
KLEE: WARNING: killing 27097 states (over memory cap)
KLEE: WARNING: killing 26195 states (over memory cap)
KLEE: WARNING: killing 27752 states (over memory cap)
KLEE: WARNING: killing 27229 states (over memory cap)
KLEE: WARNING: killing 27061 states (over memory cap)
KLEE: WARNING: killing 26417 states (over memory cap)
KLEE: WARNING: killing 27849 states (over memory cap)
KLEE: WARNING: killing 26592 states (over memory cap)
KLEE: WARNING: killing 25357 states (over memory cap)
KLEE: WARNING: killing 27021 states (over memory cap)
KLEE: WARNING: killing 27839 states (over memory cap)
KLEE: WARNING: killing 25510 states (over memory cap)
KLEE: WARNING: killing 25599 states (over memory cap)
KLEE: WARNING: killing 25320 states (over memory cap)
KLEE: WARNING: killing 25162 states (over memory cap)
KLEE: WARNING: killing 24412 states (over memory cap)
KLEE: WARNING: killing 24382 states (over memory cap)
KLEE: WARNING: killing 23993 states (over memory cap)
KLEE: WARNING: killing 25400 states (over memory cap)
KLEE: WARNING: killing 24520 states (over memory cap)
KLEE: WARNING: killing 24741 states (over memory cap)
KLEE: WARNING: killing 24225 states (over memory cap)
KLEE: WARNING: killing 24919 states (over memory cap)
KLEE: WARNING: killing 24999 states (over memory cap)
KLEE: WARNING: killing 23780 states (over memory cap)
KLEE: WARNING: killing 24580 states (over memory cap)
KLEE: WARNING: killing 24082 states (over memory cap)
KLEE: WARNING: killing 24405 states (over memory cap)
KLEE: WARNING: killing 25331 states (over memory cap)
KLEE: WARNING: killing 24940 states (over memory cap)
KLEE: WARNING: killing 24201 states (over memory cap)
KLEE: WARNING: killing 25713 states (over memory cap)
KLEE: WARNING: killing 25104 states (over memory cap)
KLEE: WARNING: killing 24478 states (over memory cap)
KLEE: WARNING: killing 26459 states (over memory cap)
KLEE: WARNING: killing 25965 states (over memory cap)
KLEE: WARNING: killing 24523 states (over memory cap)
KLEE: WARNING: killing 24373 states (over memory cap)
KLEE: WARNING: killing 24460 states (over memory cap)
KLEE: WARNING: killing 25493 states (over memory cap)
KLEE: WARNING: killing 25465 states (over memory cap)
KLEE: WARNING: killing 26260 states (over memory cap)
KLEE: WARNING: killing 25655 states (over memory cap)
KLEE: WARNING: killing 24575 states (over memory cap)
KLEE: WARNING: killing 25833 states (over memory cap)
KLEE: WARNING: killing 24766 states (over memory cap)
KLEE: WARNING: killing 24495 states (over memory cap)
KLEE: WARNING: killing 25403 states (over memory cap)
KLEE: WARNING: killing 24327 states (over memory cap)
KLEE: WARNING: killing 24649 states (over memory cap)
KLEE: WARNING: killing 25082 states (over memory cap)
KLEE: WARNING: killing 24938 states (over memory cap)
KLEE: WARNING: killing 26995 states (over memory cap)
KLEE: WARNING: killing 25939 states (over memory cap)
KLEE: WARNING: killing 25686 states (over memory cap)
KLEE: WARNING: killing 23920 states (over memory cap)
KLEE: WARNING: killing 24236 states (over memory cap)
KLEE: WARNING: killing 24332 states (over memory cap)
KLEE: WARNING: killing 25342 states (over memory cap)
KLEE: WARNING: killing 25092 states (over memory cap)
KLEE: WARNING: killing 25062 states (over memory cap)
KLEE: WARNING: killing 24119 states (over memory cap)
KLEE: WARNING: killing 24326 states (over memory cap)
KLEE: WARNING: killing 25777 states (over memory cap)
KLEE: WARNING: killing 25409 states (over memory cap)
KLEE: WARNING: killing 24476 states (over memory cap)
KLEE: WARNING: killing 24218 states (over memory cap)
KLEE: WARNING: killing 25779 states (over memory cap)
KLEE: WARNING: killing 25297 states (over memory cap)
KLEE: WARNING: killing 25841 states (over memory cap)
KLEE: WARNING: killing 24915 states (over memory cap)
KLEE: WARNING: killing 26032 states (over memory cap)
KLEE: WARNING: killing 24864 states (over memory cap)
KLEE: WARNING: killing 26197 states (over memory cap)
KLEE: WARNING: killing 25274 states (over memory cap)
KLEE: WARNING: killing 24787 states (over memory cap)
KLEE: WARNING: killing 25428 states (over memory cap)
KLEE: WARNING: killing 25071 states (over memory cap)
KLEE: WARNING: killing 25493 states (over memory cap)
KLEE: WARNING: killing 25242 states (over memory cap)
KLEE: WARNING: killing 25564 states (over memory cap)
KLEE: WARNING: killing 24178 states (over memory cap)
KLEE: WARNING: killing 24603 states (over memory cap)
KLEE: WARNING: killing 24792 states (over memory cap)
KLEE: WARNING: killing 24538 states (over memory cap)
KLEE: WARNING: killing 24065 states (over memory cap)
KLEE: WARNING: killing 25500 states (over memory cap)
KLEE: WARNING: killing 24906 states (over memory cap)
KLEE: WARNING: killing 24100 states (over memory cap)
KLEE: WARNING: killing 23849 states (over memory cap)
KLEE: WARNING: killing 26388 states (over memory cap)
KLEE: WARNING: killing 26367 states (over memory cap)
KLEE: WARNING: killing 25781 states (over memory cap)
KLEE: WARNING: killing 26097 states (over memory cap)
KLEE: WARNING: killing 24730 states (over memory cap)
KLEE: WARNING: killing 24373 states (over memory cap)
KLEE: WARNING: killing 24560 states (over memory cap)
KLEE: WARNING: killing 25190 states (over memory cap)
KLEE: WARNING: killing 25064 states (over memory cap)
KLEE: WARNING: killing 25477 states (over memory cap)
KLEE: WARNING: killing 25123 states (over memory cap)
KLEE: WARNING: killing 26646 states (over memory cap)
KLEE: WARNING: killing 25958 states (over memory cap)
KLEE: WARNING: killing 24605 states (over memory cap)
KLEE: WARNING: killing 25130 states (over memory cap)
KLEE: WARNING: killing 24435 states (over memory cap)
KLEE: WARNING: killing 25512 states (over memory cap)
KLEE: WARNING: killing 25046 states (over memory cap)
KLEE: WARNING: killing 25131 states (over memory cap)
KLEE: WARNING: killing 25438 states (over memory cap)
KLEE: WARNING: killing 25305 states (over memory cap)
KLEE: WARNING: killing 25934 states (over memory cap)
KLEE: WARNING: killing 24376 states (over memory cap)
KLEE: WARNING: killing 24903 states (over memory cap)
KLEE: WARNING: killing 24876 states (over memory cap)
KLEE: WARNING: killing 25498 states (over memory cap)
KLEE: WARNING: killing 24276 states (over memory cap)
KLEE: WARNING: killing 24901 states (over memory cap)
KLEE: WARNING: killing 25424 states (over memory cap)
KLEE: WARNING: killing 25949 states (over memory cap)
KLEE: WARNING: killing 24406 states (over memory cap)
KLEE: WARNING: killing 25026 states (over memory cap)
KLEE: WARNING: killing 25323 states (over memory cap)
KLEE: WARNING: killing 26064 states (over memory cap)
KLEE: WARNING: killing 26360 states (over memory cap)
KLEE: WARNING: killing 24185 states (over memory cap)
KLEE: WARNING: killing 24909 states (over memory cap)
KLEE: WARNING: killing 25211 states (over memory cap)
KLEE: WARNING: killing 24654 states (over memory cap)
KLEE: WARNING: killing 24094 states (over memory cap)
KLEE: WARNING: killing 25249 states (over memory cap)
KLEE: WARNING: killing 25765 states (over memory cap)
KLEE: WARNING: killing 26163 states (over memory cap)
KLEE: WARNING: killing 25083 states (over memory cap)
KLEE: WARNING: killing 23982 states (over memory cap)
KLEE: WARNING: killing 25561 states (over memory cap)
KLEE: WARNING: killing 23509 states (over memory cap)
KLEE: WARNING: killing 25085 states (over memory cap)
KLEE: WARNING: killing 24103 states (over memory cap)
KLEE: WARNING: killing 25258 states (over memory cap)
KLEE: WARNING: killing 24596 states (over memory cap)
KLEE: WARNING: killing 25748 states (over memory cap)
KLEE: WARNING: killing 23915 states (over memory cap)
KLEE: WARNING: killing 26327 states (over memory cap)
KLEE: WARNING: killing 24613 states (over memory cap)
KLEE: WARNING: killing 23525 states (over memory cap)
KLEE: WARNING: killing 24866 states (over memory cap)
KLEE: WARNING: killing 24744 states (over memory cap)
KLEE: WARNING: killing 25985 states (over memory cap)
KLEE: WARNING: killing 24587 states (over memory cap)
KLEE: WARNING: killing 25835 states (over memory cap)
KLEE: WARNING: killing 25708 states (over memory cap)
KLEE: WARNING: killing 25163 states (over memory cap)
KLEE: WARNING: killing 26196 states (over memory cap)
KLEE: WARNING: killing 25537 states (over memory cap)
KLEE: WARNING: killing 24570 states (over memory cap)
KLEE: WARNING: killing 25278 states (over memory cap)
KLEE: WARNING: killing 24620 states (over memory cap)
KLEE: WARNING: killing 24806 states (over memory cap)
