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-spinlock__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.: 404 588 3589 20810
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.722773075104
Removed calls to 'iowrite32' (function is undefined)
Removed calls to '__ldv_spin_lock' (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 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_initialize' (function is undefined)
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.711940050125
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 502 527 1788 12324
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_86c37e18-e7b6-4b08-9bd5-61871cb9a9cf/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 24772 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 24692 states (over memory cap)
KLEE: WARNING: killing 23839 states (over memory cap)
KLEE: WARNING: killing 23647 states (over memory cap)
KLEE: WARNING: killing 22435 states (over memory cap)
KLEE: WARNING: killing 23021 states (over memory cap)
KLEE: WARNING: killing 21431 states (over memory cap)
KLEE: WARNING: killing 22528 states (over memory cap)
KLEE: WARNING: killing 22359 states (over memory cap)
KLEE: WARNING: killing 22699 states (over memory cap)
KLEE: WARNING: killing 22021 states (over memory cap)
KLEE: WARNING: killing 21475 states (over memory cap)
KLEE: WARNING: killing 22576 states (over memory cap)
KLEE: WARNING: killing 22922 states (over memory cap)
KLEE: WARNING: killing 22755 states (over memory cap)
KLEE: WARNING: killing 22961 states (over memory cap)
KLEE: WARNING: killing 23682 states (over memory cap)
KLEE: WARNING: killing 24147 states (over memory cap)
KLEE: WARNING: killing 24852 states (over memory cap)
KLEE: WARNING: killing 24307 states (over memory cap)
KLEE: WARNING: killing 24267 states (over memory cap)
KLEE: WARNING: killing 25221 states (over memory cap)
KLEE: WARNING: killing 25676 states (over memory cap)
KLEE: WARNING: killing 27383 states (over memory cap)
KLEE: WARNING: killing 26351 states (over memory cap)
KLEE: WARNING: killing 27188 states (over memory cap)
KLEE: WARNING: killing 27772 states (over memory cap)
KLEE: WARNING: killing 26757 states (over memory cap)
KLEE: WARNING: killing 26101 states (over memory cap)
KLEE: WARNING: killing 27427 states (over memory cap)
KLEE: WARNING: killing 26901 states (over memory cap)
KLEE: WARNING: killing 26871 states (over memory cap)
KLEE: WARNING: killing 26586 states (over memory cap)
KLEE: WARNING: killing 25090 states (over memory cap)
KLEE: WARNING: killing 25061 states (over memory cap)
KLEE: WARNING: killing 24784 states (over memory cap)
KLEE: WARNING: killing 24136 states (over memory cap)
KLEE: WARNING: killing 25704 states (over memory cap)
KLEE: WARNING: killing 24200 states (over memory cap)
KLEE: WARNING: killing 24176 states (over memory cap)
KLEE: WARNING: killing 24262 states (over memory cap)
KLEE: WARNING: killing 25940 states (over memory cap)
KLEE: WARNING: killing 23967 states (over memory cap)
KLEE: WARNING: killing 23936 states (over memory cap)
KLEE: WARNING: killing 24750 states (over memory cap)
KLEE: WARNING: killing 23878 states (over memory cap)
KLEE: WARNING: killing 24444 states (over memory cap)
KLEE: WARNING: killing 23947 states (over memory cap)
KLEE: WARNING: killing 25955 states (over memory cap)
KLEE: WARNING: killing 25328 states (over memory cap)
KLEE: WARNING: killing 24699 states (over memory cap)
KLEE: WARNING: killing 25265 states (over memory cap)
KLEE: WARNING: killing 24032 states (over memory cap)
KLEE: WARNING: killing 25202 states (over memory cap)
KLEE: WARNING: killing 25905 states (over memory cap)
KLEE: WARNING: killing 25519 states (over memory cap)
KLEE: WARNING: killing 25617 states (over memory cap)
KLEE: WARNING: killing 25350 states (over memory cap)
KLEE: WARNING: killing 24606 states (over memory cap)
KLEE: WARNING: killing 25172 states (over memory cap)
KLEE: WARNING: killing 24898 states (over memory cap)
KLEE: WARNING: killing 25707 states (over memory cap)
KLEE: WARNING: killing 24380 states (over memory cap)
KLEE: WARNING: killing 24702 states (over memory cap)
KLEE: WARNING: killing 25981 states (over memory cap)
KLEE: WARNING: killing 25240 states (over memory cap)
KLEE: WARNING: killing 26401 states (over memory cap)
KLEE: WARNING: killing 25198 states (over memory cap)
KLEE: WARNING: killing 25645 states (over memory cap)
KLEE: WARNING: killing 24671 states (over memory cap)
KLEE: WARNING: killing 24996 states (over memory cap)
KLEE: WARNING: killing 24843 states (over memory cap)
KLEE: WARNING: killing 25293 states (over memory cap)
KLEE: WARNING: killing 24671 states (over memory cap)
KLEE: WARNING: killing 25709 states (over memory cap)
KLEE: WARNING: killing 25568 states (over memory cap)
KLEE: WARNING: killing 25544 states (over memory cap)
KLEE: WARNING: killing 24107 states (over memory cap)
KLEE: WARNING: killing 25478 states (over memory cap)
KLEE: WARNING: killing 25339 states (over memory cap)
KLEE: WARNING: killing 25185 states (over memory cap)
KLEE: WARNING: killing 25510 states (over memory cap)
KLEE: WARNING: killing 25366 states (over memory cap)
KLEE: WARNING: killing 23943 states (over memory cap)
KLEE: WARNING: killing 24507 states (over memory cap)
KLEE: WARNING: killing 25404 states (over memory cap)
KLEE: WARNING: killing 23986 states (over memory cap)
KLEE: WARNING: killing 24763 states (over memory cap)
KLEE: WARNING: killing 24861 states (over memory cap)
KLEE: WARNING: killing 25644 states (over memory cap)
KLEE: WARNING: killing 24701 states (over memory cap)
KLEE: WARNING: killing 25707 states (over memory cap)
KLEE: WARNING: killing 25568 states (over memory cap)
KLEE: WARNING: killing 24393 states (over memory cap)
KLEE: WARNING: killing 26321 states (over memory cap)
KLEE: WARNING: killing 25033 states (over memory cap)
KLEE: WARNING: killing 24892 states (over memory cap)
KLEE: WARNING: killing 24287 states (over memory cap)
KLEE: WARNING: killing 24730 states (over memory cap)
KLEE: WARNING: killing 24810 states (over memory cap)
KLEE: WARNING: killing 24671 states (over memory cap)
KLEE: WARNING: killing 25789 states (over memory cap)
KLEE: WARNING: killing 26094 states (over memory cap)
KLEE: WARNING: killing 24816 states (over memory cap)
KLEE: WARNING: killing 24902 states (over memory cap)
KLEE: WARNING: killing 26244 states (over memory cap)
KLEE: WARNING: killing 23947 states (over memory cap)
KLEE: WARNING: killing 24595 states (over memory cap)
KLEE: WARNING: killing 25022 states (over memory cap)
KLEE: WARNING: killing 24198 states (over memory cap)
KLEE: WARNING: killing 26101 states (over memory cap)
KLEE: WARNING: killing 25840 states (over memory cap)
KLEE: WARNING: killing 24127 states (over memory cap)
KLEE: WARNING: killing 25456 states (over memory cap)
KLEE: WARNING: killing 25655 states (over memory cap)
KLEE: WARNING: killing 24841 states (over memory cap)
KLEE: WARNING: killing 24931 states (over memory cap)
KLEE: WARNING: killing 24115 states (over memory cap)
KLEE: WARNING: killing 24987 states (over memory cap)
KLEE: WARNING: killing 25180 states (over memory cap)
KLEE: WARNING: killing 24703 states (over memory cap)
KLEE: WARNING: killing 23999 states (over memory cap)
KLEE: WARNING: killing 25766 states (over memory cap)
KLEE: WARNING: killing 25629 states (over memory cap)
KLEE: WARNING: killing 26164 states (over memory cap)
KLEE: WARNING: killing 24903 states (over memory cap)
KLEE: WARNING: killing 26219 states (over memory cap)
KLEE: WARNING: killing 25856 states (over memory cap)
KLEE: WARNING: killing 26166 states (over memory cap)
KLEE: WARNING: killing 24148 states (over memory cap)
KLEE: WARNING: killing 24116 states (over memory cap)
KLEE: WARNING: killing 25972 states (over memory cap)
KLEE: WARNING: killing 24290 states (over memory cap)
KLEE: WARNING: killing 25491 states (over memory cap)
KLEE: WARNING: killing 24019 states (over memory cap)
KLEE: WARNING: killing 24890 states (over memory cap)
KLEE: WARNING: killing 25307 states (over memory cap)
KLEE: WARNING: killing 25052 states (over memory cap)
KLEE: WARNING: killing 24145 states (over memory cap)
KLEE: WARNING: killing 25339 states (over memory cap)
KLEE: WARNING: killing 24431 states (over memory cap)
KLEE: WARNING: killing 24398 states (over memory cap)
KLEE: WARNING: killing 26909 states (over memory cap)
KLEE: WARNING: killing 25125 states (over memory cap)
KLEE: WARNING: killing 24886 states (over memory cap)
KLEE: WARNING: killing 25402 states (over memory cap)
KLEE: WARNING: killing 23842 states (over memory cap)
KLEE: WARNING: killing 23497 states (over memory cap)
KLEE: WARNING: killing 25437 states (over memory cap)
KLEE: WARNING: killing 25638 states (over memory cap)
KLEE: WARNING: killing 25715 states (over memory cap)
KLEE: WARNING: killing 24716 states (over memory cap)
KLEE: WARNING: killing 24355 states (over memory cap)
KLEE: WARNING: killing 24886 states (over memory cap)
KLEE: WARNING: killing 23559 states (over memory cap)
KLEE: WARNING: killing 25149 states (over memory cap)
KLEE: WARNING: killing 25131 states (over memory cap)
KLEE: WARNING: killing 25319 states (over memory cap)
KLEE: WARNING: killing 24541 states (over memory cap)
KLEE: WARNING: killing 23660 states (over memory cap)
KLEE: WARNING: killing 24816 states (over memory cap)
KLEE: WARNING: killing 25660 states (over memory cap)
KLEE: WARNING: killing 25432 states (over memory cap)
KLEE: WARNING: killing 25943 states (over memory cap)
KLEE: WARNING: killing 26016 states (over memory cap)
