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-drivers-clk1__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.: 398 510 3350 19686
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.685100793839
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)
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.668660163879
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 498 454 1573 11467
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_bb5256c8-2e29-4493-83cb-57526b07f234/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 28074 states (over memory cap)
KLEE: WARNING: killing 26839 states (over memory cap)
KLEE: WARNING: killing 23966 states (over memory cap)
KLEE: WARNING: killing 24533 states (over memory cap)
KLEE: WARNING: killing 22564 states (over memory cap)
KLEE: WARNING: killing 21496 states (over memory cap)
KLEE: WARNING: killing 21440 states (over memory cap)
KLEE: WARNING: killing 22024 states (over memory cap)
KLEE: WARNING: killing 22233 states (over memory cap)
KLEE: WARNING: killing 22314 states (over memory cap)
KLEE: WARNING: killing 21764 states (over memory cap)
KLEE: WARNING: killing 22610 states (over memory cap)
KLEE: WARNING: killing 22563 states (over memory cap)
KLEE: WARNING: killing 22657 states (over memory cap)
KLEE: WARNING: killing 22872 states (over memory cap)
KLEE: WARNING: killing 23325 states (over memory cap)
KLEE: WARNING: killing 22790 states (over memory cap)
KLEE: WARNING: killing 23493 states (over memory cap)
KLEE: WARNING: killing 24562 states (over memory cap)
KLEE: WARNING: killing 25144 states (over memory cap)
KLEE: WARNING: killing 26577 states (over memory cap)
KLEE: WARNING: killing 25551 states (over memory cap)
KLEE: WARNING: killing 27114 states (over memory cap)
KLEE: WARNING: killing 25733 states (over memory cap)
KLEE: WARNING: killing 28269 states (over memory cap)
KLEE: WARNING: killing 28366 states (over memory cap)
KLEE: WARNING: killing 26252 states (over memory cap)
KLEE: WARNING: killing 25840 states (over memory cap)
KLEE: WARNING: killing 27272 states (over memory cap)
KLEE: WARNING: killing 27612 states (over memory cap)
KLEE: WARNING: killing 25512 states (over memory cap)
KLEE: WARNING: killing 26450 states (over memory cap)
KLEE: WARNING: killing 25319 states (over memory cap)
KLEE: WARNING: killing 25409 states (over memory cap)
KLEE: WARNING: killing 24051 states (over memory cap)
KLEE: WARNING: killing 24374 states (over memory cap)
KLEE: WARNING: killing 25918 states (over memory cap)
KLEE: WARNING: killing 24798 states (over memory cap)
KLEE: WARNING: killing 25613 states (over memory cap)
KLEE: WARNING: killing 24622 states (over memory cap)
KLEE: WARNING: killing 25183 states (over memory cap)
KLEE: WARNING: killing 23473 states (over memory cap)
KLEE: WARNING: killing 25728 states (over memory cap)
KLEE: WARNING: killing 24746 states (over memory cap)
KLEE: WARNING: killing 24715 states (over memory cap)
KLEE: WARNING: killing 24444 states (over memory cap)
KLEE: WARNING: killing 24647 states (over memory cap)
KLEE: WARNING: killing 24978 states (over memory cap)
KLEE: WARNING: killing 24470 states (over memory cap)
KLEE: WARNING: killing 26467 states (over memory cap)
KLEE: WARNING: killing 25369 states (over memory cap)
KLEE: WARNING: killing 25213 states (over memory cap)
KLEE: WARNING: killing 25539 states (over memory cap)
KLEE: WARNING: killing 24809 states (over memory cap)
KLEE: WARNING: killing 24662 states (over memory cap)
KLEE: WARNING: killing 25337 states (over memory cap)
KLEE: WARNING: killing 24962 states (over memory cap)
KLEE: WARNING: killing 25282 states (over memory cap)
KLEE: WARNING: killing 25259 states (over memory cap)
KLEE: WARNING: killing 24171 states (over memory cap)
KLEE: WARNING: killing 26025 states (over memory cap)
KLEE: WARNING: killing 24118 states (over memory cap)
KLEE: WARNING: killing 24674 states (over memory cap)
KLEE: WARNING: killing 25583 states (over memory cap)
KLEE: WARNING: killing 24752 states (over memory cap)
KLEE: WARNING: killing 25429 states (over memory cap)
KLEE: WARNING: killing 26109 states (over memory cap)
KLEE: WARNING: killing 24668 states (over memory cap)
KLEE: WARNING: killing 24417 states (over memory cap)
KLEE: WARNING: killing 24613 states (over memory cap)
KLEE: WARNING: killing 25504 states (over memory cap)
KLEE: WARNING: killing 25131 states (over memory cap)
KLEE: WARNING: killing 24524 states (over memory cap)
KLEE: WARNING: killing 25433 states (over memory cap)
KLEE: WARNING: killing 26104 states (over memory cap)
KLEE: WARNING: killing 25612 states (over memory cap)
KLEE: WARNING: killing 25596 states (over memory cap)
KLEE: WARNING: killing 26483 states (over memory cap)
KLEE: WARNING: killing 24615 states (over memory cap)
KLEE: WARNING: killing 24705 states (over memory cap)
KLEE: WARNING: killing 25707 states (over memory cap)
KLEE: WARNING: killing 23383 states (over memory cap)
KLEE: WARNING: killing 25315 states (over memory cap)
KLEE: WARNING: killing 24373 states (over memory cap)
KLEE: WARNING: killing 24571 states (over memory cap)
KLEE: WARNING: killing 25457 states (over memory cap)
KLEE: WARNING: killing 24175 states (over memory cap)
KLEE: WARNING: killing 26435 states (over memory cap)
KLEE: WARNING: killing 25045 states (over memory cap)
KLEE: WARNING: killing 25022 states (over memory cap)
KLEE: WARNING: killing 25455 states (over memory cap)
KLEE: WARNING: killing 24623 states (over memory cap)
KLEE: WARNING: killing 24945 states (over memory cap)
KLEE: WARNING: killing 24794 states (over memory cap)
KLEE: WARNING: killing 24533 states (over memory cap)
KLEE: WARNING: killing 26105 states (over memory cap)
KLEE: WARNING: killing 25967 states (over memory cap)
KLEE: WARNING: killing 23895 states (over memory cap)
KLEE: WARNING: killing 24322 states (over memory cap)
KLEE: WARNING: killing 26670 states (over memory cap)
KLEE: WARNING: killing 25057 states (over memory cap)
KLEE: WARNING: killing 24135 states (over memory cap)
KLEE: WARNING: killing 25232 states (over memory cap)
KLEE: WARNING: killing 25090 states (over memory cap)
KLEE: WARNING: killing 26202 states (over memory cap)
KLEE: WARNING: killing 26168 states (over memory cap)
KLEE: WARNING: killing 23794 states (over memory cap)
KLEE: WARNING: killing 25558 states (over memory cap)
KLEE: WARNING: killing 24963 states (over memory cap)
KLEE: WARNING: killing 25162 states (over memory cap)
KLEE: WARNING: killing 25815 states (over memory cap)
KLEE: WARNING: killing 26015 states (over memory cap)
KLEE: WARNING: killing 24316 states (over memory cap)
KLEE: WARNING: killing 25303 states (over memory cap)
KLEE: WARNING: killing 24036 states (over memory cap)
KLEE: WARNING: killing 24785 states (over memory cap)
KLEE: WARNING: killing 24421 states (over memory cap)
KLEE: WARNING: killing 25281 states (over memory cap)
KLEE: WARNING: killing 24367 states (over memory cap)
KLEE: WARNING: killing 24683 states (over memory cap)
KLEE: WARNING: killing 25314 states (over memory cap)
KLEE: WARNING: killing 24402 states (over memory cap)
KLEE: WARNING: killing 25374 states (over memory cap)
KLEE: WARNING: killing 26223 states (over memory cap)
KLEE: WARNING: killing 25212 states (over memory cap)
KLEE: WARNING: killing 24292 states (over memory cap)
KLEE: WARNING: killing 24699 states (over memory cap)
KLEE: WARNING: killing 24464 states (over memory cap)
KLEE: WARNING: killing 26086 states (over memory cap)
KLEE: WARNING: killing 24086 states (over memory cap)
KLEE: WARNING: killing 24721 states (over memory cap)
KLEE: WARNING: killing 24578 states (over memory cap)
KLEE: WARNING: killing 25545 states (over memory cap)
KLEE: WARNING: killing 25964 states (over memory cap)
KLEE: WARNING: killing 26483 states (over memory cap)
KLEE: WARNING: killing 24504 states (over memory cap)
KLEE: WARNING: killing 24578 states (over memory cap)
KLEE: WARNING: killing 26398 states (over memory cap)
KLEE: WARNING: killing 24531 states (over memory cap)
KLEE: WARNING: killing 24609 states (over memory cap)
KLEE: WARNING: killing 25247 states (over memory cap)
KLEE: WARNING: killing 25004 states (over memory cap)
KLEE: WARNING: killing 25520 states (over memory cap)
KLEE: WARNING: killing 24409 states (over memory cap)
KLEE: WARNING: killing 24926 states (over memory cap)
KLEE: WARNING: killing 24567 states (over memory cap)
KLEE: WARNING: killing 24550 states (over memory cap)
KLEE: WARNING: killing 24950 states (over memory cap)
KLEE: WARNING: killing 25573 states (over memory cap)
KLEE: WARNING: killing 25446 states (over memory cap)
KLEE: WARNING: killing 24881 states (over memory cap)
KLEE: WARNING: killing 26587 states (over memory cap)
KLEE: WARNING: killing 25053 states (over memory cap)
KLEE: WARNING: killing 24707 states (over memory cap)
KLEE: WARNING: killing 23729 states (over memory cap)
KLEE: WARNING: killing 24443 states (over memory cap)
KLEE: WARNING: killing 24521 states (over memory cap)
KLEE: WARNING: killing 24924 states (over memory cap)
KLEE: WARNING: killing 25552 states (over memory cap)
KLEE: WARNING: killing 25429 states (over memory cap)
KLEE: WARNING: killing 25293 states (over memory cap)
KLEE: WARNING: killing 25792 states (over memory cap)
KLEE: WARNING: killing 25774 states (over memory cap)
KLEE: WARNING: killing 25015 states (over memory cap)
KLEE: WARNING: killing 25198 states (over memory cap)
