bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.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.: 280 337 3936 26947
Removed infinite loop in v4l2_subdev_get_try_crop
Removed infinite loop in v4l2_subdev_get_try_compose
Removed infinite loop in v4l2_subdev_get_try_format
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.980257987976
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'clk_put' (function is undefined)
Removed calls to 'pm_runtime_enable' (function is undefined)
Removed calls to 'clk_disable' (function is undefined)
Removed calls to 'v4l2_device_unregister_subdev' (function is undefined)
Removed calls to 'media_entity_cleanup' (function is undefined)
Removed calls to '__pm_runtime_disable' (function is undefined)
Removed calls to 'vb2_dma_contig_cleanup_ctx' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'clk_unprepare' (function is undefined)
Defining function __pm_runtime_set_status as symbolic
Defining function platform_get_resource as symbolic
Defining function devm_ioremap_resource as symbolic
Defining function clk_set_rate as symbolic
Defining function clk_enable as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'v4l2_subdev_init' (function is undefined)
Defining function vb2_dma_contig_init_ctx as symbolic
Defining function snprintf as symbolic
Defining function media_entity_init as symbolic
Defining function devm_request_threaded_irq as symbolic
Defining function v4l2_m2m_get_curr_priv as symbolic
Removed calls to 'vb2_buffer_done' (function is undefined)
Removed calls to 'v4l2_m2m_job_finish' (function is undefined)
Removed calls to 'getnstimeofday64' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function vb2_plane_vaddr as symbolic
Defining function v4l2_m2m_buf_remove as symbolic
Defining function clk_get as symbolic
Defining function clk_prepare as symbolic
Defining function syscon_regmap_lookup_by_phandle as symbolic
Defining function of_match_node as symbolic
Defining function of_property_read_u32_array as symbolic
Defining function of_alias_get_id as symbolic
Defining function of_find_property as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Defining function vb2_plane_cookie as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'usleep_range' (function is undefined)
Defining function regmap_read as symbolic
Defining function regmap_update_bits as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function v4l2_m2m_fop_poll as symbolic
Defining function video_ioctl2 as symbolic
Defining function v4l2_m2m_fop_mmap as symbolic
Removed calls to 'v4l2_fh_init' (function is undefined)
Removed calls to 'v4l2_fh_add' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'v4l2_m2m_ctx_release' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_fh_del' (function is undefined)
Removed calls to 'v4l2_fh_exit' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Removed calls to 'v4l2_ctrl_cluster' (function is undefined)
Defining function v4l2_m2m_ctx_init as symbolic
Defining function vb2_queue_init as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_new_std_menu as symbolic
Defining function video_devdata as symbolic
Removed calls to '__fimc_vidioc_querycap' (function is undefined)
Defining function v4l2_m2m_ioctl_reqbufs as symbolic
Defining function v4l2_m2m_ioctl_querybuf as symbolic
Defining function v4l2_m2m_ioctl_qbuf as symbolic
Defining function v4l2_m2m_ioctl_expbuf as symbolic
Defining function v4l2_m2m_ioctl_dqbuf as symbolic
Defining function v4l2_m2m_ioctl_streamon as symbolic
Defining function v4l2_m2m_ioctl_streamoff as symbolic
Removed calls to 'v4l_bound_align_image' (function is undefined)
Defining function v4l2_m2m_get_vq as symbolic
Defining function v4l2_m2m_next_buf as symbolic
Removed calls to 'v4l2_m2m_buf_queue' (function is undefined)
Defining function __pm_runtime_idle as symbolic
Defining function __pm_runtime_resume as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'v4l2_ctrl_activate' (function is undefined)
Defining function fimc_find_remote_sensor as symbolic
Defining function v4l2_ctrl_add_handler as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'v4l2_m2m_release' (function is undefined)
Defining function __video_register_device as symbolic
Defining function v4l2_m2m_init as symbolic
Defining function vb2_fop_poll as symbolic
Defining function vb2_fop_mmap as symbolic
Removed calls to 'media_entity_pipeline_stop' (function is undefined)
Defining function _vb2_fop_release as symbolic
Defining function v4l2_fh_is_singular as symbolic
Defining function v4l2_fh_open as symbolic
Defining function v4l2_fh_release as symbolic
Defining function media_entity_remote_pad as symbolic
Defining function vb2_ioctl_querybuf as symbolic
Defining function vb2_ioctl_qbuf as symbolic
Defining function vb2_ioctl_expbuf as symbolic
Defining function vb2_ioctl_dqbuf as symbolic
Defining function vb2_ioctl_create_bufs as symbolic
Defining function vb2_ioctl_prepare_buf as symbolic
Defining function strlcpy as symbolic
Defining function vb2_ioctl_streamoff as symbolic
Defining function media_entity_pipeline_start as symbolic
Defining function vb2_ioctl_streamon as symbolic
Defining function vb2_ioctl_reqbufs as symbolic
Removed calls to 'put_device' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'media_device_unregister' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'v4l2_async_notifier_unregister' (function is undefined)
Removed calls to 'of_clk_del_provider' (function is undefined)
Removed calls to 'clk_unregister' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function __media_device_register as symbolic
Defining function device_create_file as symbolic
Defining function v4l2_async_notifier_register as symbolic
Defining function v4l2_device_register_subdev_nodes as symbolic
Defining function media_entity_create_link as symbolic
Defining function __clk_get_name as symbolic
Defining function clk_register as symbolic
Defining function of_clk_src_onecell_get as symbolic
Defining function of_clk_add_provider as symbolic
Defining function of_property_read_string_helper as symbolic
Defining function of_get_next_available_child as symbolic
Defining function strcasecmp as symbolic
Defining function of_get_next_child as symbolic
Removed calls to 'of_node_put' (function is undefined)
Defining function of_get_child_by_name as symbolic
Defining function v4l2_of_parse_endpoint as symbolic
Defining function of_graph_get_remote_port_parent as symbolic
Defining function of_get_parent as symbolic
Defining function of_find_device_by_node as symbolic
Defining function v4l2_device_register_subdev as symbolic
Defining function devm_pinctrl_get as symbolic
Defining function pinctrl_lookup_state as symbolic
Defining function of_device_is_available as symbolic
Removed calls to 'media_entity_graph_walk_start' (function is undefined)
Defining function media_entity_graph_walk_next as symbolic
Defining function __platform_driver_register as symbolic
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function ldv_suspend_late_16 as symbolic
Defining function ldv_restore_early_16 as symbolic
Defining function ldv_resume_early_16 as symbolic
Defining function ldv_thaw_early_16 as symbolic
Defining function ldv_resume_noirq_16 as symbolic
Defining function ldv_freeze_noirq_16 as symbolic
Defining function ldv_prepare_16 as symbolic
Defining function ldv_freeze_late_16 as symbolic
Defining function ldv_thaw_noirq_16 as symbolic
Defining function ldv_poweroff_noirq_16 as symbolic
Defining function ldv_poweroff_late_16 as symbolic
Defining function ldv_restore_noirq_16 as symbolic
Defining function ldv_suspend_noirq_16 as symbolic
Defining function ldv_complete_16 as symbolic
Removed calls to 'vb2_ops_wait_prepare' (function is undefined)
Removed calls to 'vb2_ops_wait_finish' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Defining function __request_module as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strncpy
  __kmalloc
  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: 1.01039385796
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 445 322 2130 16602
INFO: Starting verification
KLEE: WARNING ONCE: function "fimc_s_ctrl" has inline asm
KLEE: WARNING ONCE: function "fimc_irq_handler" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_irq_handler" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_output_addr" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_camera_offset" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_prescaler" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_mainscaler" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_target_format" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_rotation" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_effect" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_out_dma" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_rgb_alpha" has inline asm
KLEE: WARNING ONCE: function "fimc_deactivate_capture" has inline asm
KLEE: WARNING ONCE: function "fimc_suspend" has inline asm
KLEE: WARNING ONCE: function "fimc_resume" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_reset" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_resume" has inline asm
KLEE: WARNING ONCE: function "fimc_m2m_resume" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_hw_init" has inline asm
KLEE: WARNING ONCE: function "buffer_queue" has inline asm
KLEE: WARNING ONCE: function "fimc_activate_capture" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_camera_polarity" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_camera_type" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_camera_source" has inline asm
KLEE: WARNING ONCE: function "fimc_m2m_suspend" has inline asm
KLEE: WARNING ONCE: function "fimc_stop_capture" has inline asm
KLEE: WARNING ONCE: function "fimc_m2m_open" has inline asm
KLEE: WARNING ONCE: function "fimc_m2m_release" has inline asm
KLEE: WARNING ONCE: function "fimc_m2m_s_crop" has inline asm
KLEE: WARNING ONCE: function "fimc_try_fmt_mplane" has inline asm
KLEE: WARNING ONCE: function "fimc_device_run" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_in_dma" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_input_addr" has inline asm
KLEE: WARNING ONCE: function "fimc_subdev_get_fmt" has inline asm
KLEE: WARNING ONCE: function "fimc_subdev_set_fmt" has inline asm
KLEE: WARNING ONCE: function "fimc_subdev_get_selection" has inline asm
KLEE: WARNING ONCE: function "fimc_subdev_set_selection" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_try_selection" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_try_format" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_mark_jpeg_xfer" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_open" has inline asm
KLEE: WARNING ONCE: function "fimc_capture_release" has inline asm
KLEE: WARNING ONCE: function "fimc_cap_s_selection" has inline asm
KLEE: WARNING ONCE: function "start_streaming___0" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_clear_irq" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_get_frame_index" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_en_lastirq" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_disable_capture" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_enable_scaler" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_enable_capture" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_input_path" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_set_output_path" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_activate_input_dma" has inline asm
KLEE: WARNING ONCE: function "fimc_hw_get_prev_frame_index" 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: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_3a09a37d-bd25-44d6-a5e8-867b6b44f37a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13085 states (over memory cap)
KLEE: WARNING: killing 21593 states (over memory cap)
KLEE: WARNING: killing 21680 states (over memory cap)
KLEE: WARNING: killing 20741 states (over memory cap)
KLEE: WARNING: killing 20690 states (over memory cap)
KLEE: WARNING: killing 20710 states (over memory cap)
KLEE: WARNING: killing 21172 states (over memory cap)
KLEE: WARNING: killing 20264 states (over memory cap)
KLEE: WARNING: killing 20872 states (over memory cap)
KLEE: WARNING: killing 20680 states (over memory cap)
KLEE: WARNING: killing 21008 states (over memory cap)
KLEE: WARNING: killing 21470 states (over memory cap)
KLEE: WARNING: killing 22299 states (over memory cap)
KLEE: WARNING: killing 24277 states (over memory cap)
KLEE: WARNING: killing 22956 states (over memory cap)
KLEE: WARNING: killing 25144 states (over memory cap)
KLEE: WARNING: killing 23120 states (over memory cap)
KLEE: WARNING: killing 23529 states (over memory cap)
KLEE: WARNING: killing 23363 states (over memory cap)
KLEE: WARNING: killing 22839 states (over memory cap)
KLEE: WARNING: killing 22244 states (over memory cap)
KLEE: WARNING: killing 21647 states (over memory cap)
KLEE: WARNING: killing 21966 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:17708: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:17725: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:10099: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:9871: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:17604: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 21793 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:17631: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:5880: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:5865: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:16108: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:16212: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23593 states (over memory cap)
KLEE: WARNING: killing 21588 states (over memory cap)
KLEE: WARNING: killing 21336 states (over memory cap)
KLEE: WARNING: killing 22437 states (over memory cap)
KLEE: WARNING: killing 23603 states (over memory cap)
KLEE: WARNING: killing 22248 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:12436: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:12614: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:12384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22289 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:12670: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14346: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22750 states (over memory cap)
KLEE: WARNING: killing 22868 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14585: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23127 states (over memory cap)
KLEE: WARNING: killing 22880 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14511: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14412: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:5865: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22643 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:5865: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21986 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:10234: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:10045: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:11521: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23079 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:9912: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22504 states (over memory cap)
KLEE: WARNING: killing 22539 states (over memory cap)
KLEE: WARNING: killing 22791 states (over memory cap)
KLEE: WARNING: killing 21862 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:6910: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22878 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14192: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23340 states (over memory cap)
KLEE: WARNING: killing 21711 states (over memory cap)
KLEE: WARNING: killing 23143 states (over memory cap)
KLEE: WARNING: killing 22709 states (over memory cap)
KLEE: WARNING: killing 23098 states (over memory cap)
KLEE: WARNING: killing 22801 states (over memory cap)
KLEE: WARNING: killing 22436 states (over memory cap)
KLEE: WARNING: killing 23021 states (over memory cap)
KLEE: WARNING: killing 21288 states (over memory cap)
KLEE: WARNING: killing 22297 states (over memory cap)
KLEE: WARNING: killing 23300 states (over memory cap)
KLEE: WARNING: killing 22176 states (over memory cap)
KLEE: WARNING: killing 22492 states (over memory cap)
KLEE: WARNING: killing 23425 states (over memory cap)
KLEE: WARNING: killing 22658 states (over memory cap)
KLEE: WARNING: killing 23377 states (over memory cap)
KLEE: WARNING: killing 22128 states (over memory cap)
KLEE: WARNING: killing 22244 states (over memory cap)
KLEE: WARNING: killing 22892 states (over memory cap)
KLEE: WARNING: killing 23280 states (over memory cap)
KLEE: WARNING: killing 22916 states (over memory cap)
KLEE: WARNING: killing 22359 states (over memory cap)
KLEE: WARNING: killing 21924 states (over memory cap)
KLEE: WARNING: killing 22788 states (over memory cap)
KLEE: WARNING: killing 23229 states (over memory cap)
KLEE: WARNING: killing 21588 states (over memory cap)
KLEE: WARNING: killing 23054 states (over memory cap)
KLEE: WARNING: killing 22704 states (over memory cap)
KLEE: WARNING: killing 22407 states (over memory cap)
KLEE: WARNING: killing 21712 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:13522: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14015: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22688 states (over memory cap)
KLEE: WARNING: killing 23328 states (over memory cap)
KLEE: WARNING: killing 22033 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:13738: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22604 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:13213: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21916 states (over memory cap)
KLEE: WARNING: killing 23025 states (over memory cap)
KLEE: WARNING: killing 23345 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:13663: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14115: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22864 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:14047: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21428 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:11282: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22076 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:10466: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22920 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:11330: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22365 states (over memory cap)
KLEE: WARNING: killing 23278 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:10644: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:10284: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23716 states (over memory cap)
KLEE: WARNING: killing 22769 states (over memory cap)
KLEE: WARNING: killing 21749 states (over memory cap)
KLEE: WARNING: killing 22721 states (over memory cap)
KLEE: WARNING: killing 22966 states (over memory cap)
KLEE: WARNING: killing 20972 states (over memory cap)
KLEE: WARNING: killing 24180 states (over memory cap)
KLEE: WARNING: killing 21258 states (over memory cap)
KLEE: WARNING: killing 22746 states (over memory cap)
KLEE: WARNING: killing 23455 states (over memory cap)
KLEE: WARNING: killing 22648 states (over memory cap)
KLEE: WARNING: killing 21770 states (over memory cap)
KLEE: WARNING: killing 22473 states (over memory cap)
KLEE: WARNING: killing 22127 states (over memory cap)
KLEE: WARNING: killing 23154 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-s3TM8D/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c:13546: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23533 states (over memory cap)
KLEE: WARNING: killing 22330 states (over memory cap)
KLEE: WARNING: killing 21523 states (over memory cap)
KLEE: WARNING: killing 21763 states (over memory cap)
KLEE: WARNING: killing 22460 states (over memory cap)
KLEE: WARNING: killing 23026 states (over memory cap)
KLEE: WARNING: killing 22164 states (over memory cap)
KLEE: WARNING: killing 23051 states (over memory cap)
KLEE: WARNING: killing 22583 states (over memory cap)
KLEE: WARNING: killing 23548 states (over memory cap)
KLEE: WARNING: killing 22488 states (over memory cap)
KLEE: WARNING: killing 22144 states (over memory cap)
KLEE: WARNING: killing 23361 states (over memory cap)
KLEE: WARNING: killing 22112 states (over memory cap)
KLEE: WARNING: killing 22343 states (over memory cap)
KLEE: WARNING: killing 22391 states (over memory cap)
KLEE: WARNING: killing 21721 states (over memory cap)
KLEE: WARNING: killing 21181 states (over memory cap)
KLEE: WARNING: killing 23232 states (over memory cap)
KLEE: WARNING: killing 22636 states (over memory cap)
KLEE: WARNING: killing 22935 states (over memory cap)
KLEE: WARNING: killing 22794 states (over memory cap)
