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-kernel-locking-mutex__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.: 403 574 3533 20735
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.713447093964
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 '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.705806970596
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 503 504 1811 12282
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_ed971548-1ff4-4ed6-9d20-851825991498/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 29293 states (over memory cap)
KLEE: WARNING: killing 24656 states (over memory cap)
KLEE: WARNING: killing 24325 states (over memory cap)
KLEE: WARNING: killing 23121 states (over memory cap)
KLEE: WARNING: killing 22811 states (over memory cap)
KLEE: WARNING: killing 22749 states (over memory cap)
KLEE: WARNING: killing 21332 states (over memory cap)
KLEE: WARNING: killing 22271 states (over memory cap)
KLEE: WARNING: killing 20614 states (over memory cap)
KLEE: WARNING: killing 23057 states (over memory cap)
KLEE: WARNING: killing 22399 states (over memory cap)
KLEE: WARNING: killing 22236 states (over memory cap)
KLEE: WARNING: killing 21336 states (over memory cap)
KLEE: WARNING: killing 24865 states (over memory cap)
KLEE: WARNING: killing 23963 states (over memory cap)
KLEE: WARNING: killing 23799 states (over memory cap)
KLEE: WARNING: killing 23752 states (over memory cap)
KLEE: WARNING: killing 23587 states (over memory cap)
KLEE: WARNING: killing 25760 states (over memory cap)
KLEE: WARNING: killing 25473 states (over memory cap)
KLEE: WARNING: killing 24451 states (over memory cap)
KLEE: WARNING: killing 25273 states (over memory cap)
KLEE: WARNING: killing 27186 states (over memory cap)
KLEE: WARNING: killing 28478 states (over memory cap)
KLEE: WARNING: killing 27233 states (over memory cap)
KLEE: WARNING: killing 27445 states (over memory cap)
KLEE: WARNING: killing 27777 states (over memory cap)
KLEE: WARNING: killing 26652 states (over memory cap)
KLEE: WARNING: killing 26138 states (over memory cap)
KLEE: WARNING: killing 26343 states (over memory cap)
KLEE: WARNING: killing 24498 states (over memory cap)
KLEE: WARNING: killing 26635 states (over memory cap)
KLEE: WARNING: killing 25282 states (over memory cap)
KLEE: WARNING: killing 25254 states (over memory cap)
KLEE: WARNING: killing 24735 states (over memory cap)
KLEE: WARNING: killing 25311 states (over memory cap)
KLEE: WARNING: killing 23967 states (over memory cap)
KLEE: WARNING: killing 24059 states (over memory cap)
KLEE: WARNING: killing 24736 states (over memory cap)
KLEE: WARNING: killing 25657 states (over memory cap)
KLEE: WARNING: killing 24085 states (over memory cap)
KLEE: WARNING: killing 25603 states (over memory cap)
KLEE: WARNING: killing 24271 states (over memory cap)
KLEE: WARNING: killing 25430 states (over memory cap)
KLEE: WARNING: killing 24676 states (over memory cap)
KLEE: WARNING: killing 25718 states (over memory cap)
KLEE: WARNING: killing 24625 states (over memory cap)
KLEE: WARNING: killing 25656 states (over memory cap)
KLEE: WARNING: killing 23503 states (over memory cap)
KLEE: WARNING: killing 23584 states (over memory cap)
KLEE: WARNING: killing 24969 states (over memory cap)
KLEE: WARNING: killing 24355 states (over memory cap)
KLEE: WARNING: killing 24206 states (over memory cap)
KLEE: WARNING: killing 23482 states (over memory cap)
KLEE: WARNING: killing 25922 states (over memory cap)
KLEE: WARNING: killing 25892 states (over memory cap)
KLEE: WARNING: killing 25399 states (over memory cap)
KLEE: WARNING: killing 25130 states (over memory cap)
KLEE: WARNING: killing 24525 states (over memory cap)
KLEE: WARNING: killing 26947 states (over memory cap)
KLEE: WARNING: killing 25984 states (over memory cap)
KLEE: WARNING: killing 24909 states (over memory cap)
KLEE: WARNING: killing 24191 states (over memory cap)
KLEE: WARNING: killing 25560 states (over memory cap)
KLEE: WARNING: killing 25301 states (over memory cap)
KLEE: WARNING: killing 25034 states (over memory cap)
KLEE: WARNING: killing 24888 states (over memory cap)
KLEE: WARNING: killing 25093 states (over memory cap)
KLEE: WARNING: killing 24949 states (over memory cap)
KLEE: WARNING: killing 26306 states (over memory cap)
KLEE: WARNING: killing 23523 states (over memory cap)
KLEE: WARNING: killing 25331 states (over memory cap)
KLEE: WARNING: killing 24387 states (over memory cap)
KLEE: WARNING: killing 25966 states (over memory cap)
KLEE: WARNING: killing 24793 states (over memory cap)
KLEE: WARNING: killing 23847 states (over memory cap)
KLEE: WARNING: killing 25192 states (over memory cap)
KLEE: WARNING: killing 25057 states (over memory cap)
KLEE: WARNING: killing 24816 states (over memory cap)
KLEE: WARNING: killing 23986 states (over memory cap)
KLEE: WARNING: killing 24982 states (over memory cap)
KLEE: WARNING: killing 24035 states (over memory cap)
KLEE: WARNING: killing 25608 states (over memory cap)
KLEE: WARNING: killing 25358 states (over memory cap)
KLEE: WARNING: killing 27157 states (over memory cap)
KLEE: WARNING: killing 24857 states (over memory cap)
KLEE: WARNING: killing 24036 states (over memory cap)
KLEE: WARNING: killing 25822 states (over memory cap)
KLEE: WARNING: killing 25229 states (over memory cap)
KLEE: WARNING: killing 24859 states (over memory cap)
KLEE: WARNING: killing 23363 states (over memory cap)
KLEE: WARNING: killing 24247 states (over memory cap)
KLEE: WARNING: killing 24434 states (over memory cap)
KLEE: WARNING: killing 25421 states (over memory cap)
KLEE: WARNING: killing 25844 states (over memory cap)
KLEE: WARNING: killing 24929 states (over memory cap)
KLEE: WARNING: killing 25575 states (over memory cap)
KLEE: WARNING: killing 25649 states (over memory cap)
KLEE: WARNING: killing 24955 states (over memory cap)
KLEE: WARNING: killing 25936 states (over memory cap)
KLEE: WARNING: killing 25024 states (over memory cap)
KLEE: WARNING: killing 25895 states (over memory cap)
KLEE: WARNING: killing 25746 states (over memory cap)
KLEE: WARNING: killing 25058 states (over memory cap)
KLEE: WARNING: killing 25584 states (over memory cap)
KLEE: WARNING: killing 25782 states (over memory cap)
KLEE: WARNING: killing 24531 states (over memory cap)
KLEE: WARNING: killing 24383 states (over memory cap)
KLEE: WARNING: killing 24133 states (over memory cap)
KLEE: WARNING: killing 25775 states (over memory cap)
KLEE: WARNING: killing 24756 states (over memory cap)
KLEE: WARNING: killing 24938 states (over memory cap)
KLEE: WARNING: killing 24041 states (over memory cap)
KLEE: WARNING: killing 27322 states (over memory cap)
KLEE: WARNING: killing 24428 states (over memory cap)
KLEE: WARNING: killing 24190 states (over memory cap)
KLEE: WARNING: killing 25151 states (over memory cap)
KLEE: WARNING: killing 25136 states (over memory cap)
KLEE: WARNING: killing 25989 states (over memory cap)
KLEE: WARNING: killing 25956 states (over memory cap)
KLEE: WARNING: killing 24398 states (over memory cap)
KLEE: WARNING: killing 24814 states (over memory cap)
KLEE: WARNING: killing 25652 states (over memory cap)
KLEE: WARNING: killing 24538 states (over memory cap)
KLEE: WARNING: killing 23965 states (over memory cap)
KLEE: WARNING: killing 25571 states (over memory cap)
KLEE: WARNING: killing 25646 states (over memory cap)
KLEE: WARNING: killing 24749 states (over memory cap)
KLEE: WARNING: killing 23852 states (over memory cap)
KLEE: WARNING: killing 25245 states (over memory cap)
KLEE: WARNING: killing 24138 states (over memory cap)
KLEE: WARNING: killing 24547 states (over memory cap)
KLEE: WARNING: killing 25933 states (over memory cap)
KLEE: WARNING: killing 25591 states (over memory cap)
KLEE: WARNING: killing 25344 states (over memory cap)
KLEE: WARNING: killing 24884 states (over memory cap)
KLEE: WARNING: killing 24545 states (over memory cap)
KLEE: WARNING: killing 26787 states (over memory cap)
KLEE: WARNING: killing 25349 states (over memory cap)
KLEE: WARNING: killing 24461 states (over memory cap)
KLEE: WARNING: killing 25190 states (over memory cap)
KLEE: WARNING: killing 24630 states (over memory cap)
KLEE: WARNING: killing 27304 states (over memory cap)
KLEE: WARNING: killing 24372 states (over memory cap)
KLEE: WARNING: killing 24572 states (over memory cap)
KLEE: WARNING: killing 24865 states (over memory cap)
KLEE: WARNING: killing 24835 states (over memory cap)
KLEE: WARNING: killing 24927 states (over memory cap)
KLEE: WARNING: killing 24470 states (over memory cap)
KLEE: WARNING: killing 25094 states (over memory cap)
KLEE: WARNING: killing 23890 states (over memory cap)
KLEE: WARNING: killing 25245 states (over memory cap)
KLEE: WARNING: killing 25541 states (over memory cap)
KLEE: WARNING: killing 25948 states (over memory cap)
KLEE: WARNING: killing 24433 states (over memory cap)
KLEE: WARNING: killing 23460 states (over memory cap)
KLEE: WARNING: killing 24394 states (over memory cap)
KLEE: WARNING: killing 25000 states (over memory cap)
KLEE: WARNING: killing 24981 states (over memory cap)
KLEE: WARNING: killing 24950 states (over memory cap)
KLEE: WARNING: killing 25346 states (over memory cap)
KLEE: WARNING: killing 25539 states (over memory cap)
KLEE: WARNING: killing 24036 states (over memory cap)
KLEE: WARNING: killing 24743 states (over memory cap)
