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-soc_camera-sh_mobile_ceu_camera_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.: 165 300 2319 12776
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.475231170654
Removed calls to 'iowrite32' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function dev_warn as symbolic
Defining function ioread32 as symbolic
Defining function __pm_runtime_resume as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'vb2_buffer_done' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function __pm_runtime_idle as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function soc_mbus_get_fmtdesc as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function soc_camera_client_g_rect as symbolic
Defining function dev_err as symbolic
Defining function soc_mbus_config_compatible as symbolic
Defining function vb2_queue_init as symbolic
Defining function vb2_poll as symbolic
Defining function strlcpy as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function soc_camera_client_s_crop as symbolic
Removed calls to 'soc_camera_calc_client_output' (function is undefined)
Defining function soc_camera_xlate_by_fourcc as symbolic
Defining function soc_camera_client_scale as symbolic
Defining function wait_for_completion_interruptible as symbolic
Removed calls to 'complete' (function is undefined)
Defining function vb2_plane_cookie as symbolic
Removed calls to 'v4l_bound_align_image' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function __request_module as symbolic
Defining function __platform_driver_register as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'v4l2_get_timestamp' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function soc_mbus_bytes_per_line as symbolic
Defining function soc_mbus_image_size as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'pm_runtime_enable' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'soc_camera_host_unregister' (function is undefined)
Removed calls to 'platform_device_del' (function is undefined)
Removed calls to 'platform_device_put' (function is undefined)
Removed calls to 'vb2_dma_contig_cleanup_ctx' (function is undefined)
Removed calls to '__pm_runtime_disable' (function is undefined)
Defining function platform_get_resource as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Defining function platform_get_irq as symbolic
Defining function devm_ioremap_resource as symbolic
Defining function vb2_dma_contig_init_ctx as symbolic
Defining function platform_device_alloc as symbolic
Defining function platform_device_add_data as symbolic
Defining function platform_device_add as symbolic
Defining function bus_register_notifier as symbolic
Defining function bus_unregister_notifier as symbolic
Defining function try_module_get as symbolic
Defining function soc_camera_host_register as symbolic
Defining function v4l2_device_register_subdev as symbolic
Defining function devm_request_threaded_irq as symbolic
Defining function devm_kmalloc as symbolic
Defining function _dev_info as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'soc_camera_lock' (function is undefined)
Removed calls to 'soc_camera_unlock' (function is undefined)
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 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strncmp
  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.465310811996
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 220 292 1100 7218
INFO: Starting verification
KLEE: WARNING ONCE: function "sh_mobile_ceu_set_bus_param" has inline asm
KLEE: WARNING: undefined reference to function: soc_camera_lock
KLEE: WARNING: undefined reference to function: soc_camera_unlock
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_c07bb3f6-a97d-41ab-854b-cbf775ada194/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 15000 states (over memory cap)
KLEE: WARNING: killing 21874 states (over memory cap)
KLEE: WARNING: killing 21897 states (over memory cap)
KLEE: WARNING: killing 20948 states (over memory cap)
KLEE: WARNING: killing 21857 states (over memory cap)
KLEE: WARNING: killing 22400 states (over memory cap)
KLEE: WARNING: killing 21591 states (over memory cap)
KLEE: WARNING: killing 21528 states (over memory cap)
KLEE: WARNING: killing 12293 states (over memory cap)
KLEE: WARNING: killing 21790 states (over memory cap)
KLEE: WARNING: killing 22565 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 23300 states (over memory cap)
KLEE: WARNING: killing 12738 states (over memory cap)
KLEE: WARNING: killing 12477 states (over memory cap)
KLEE: WARNING: killing 12219 states (over memory cap)
KLEE: WARNING: killing 12201 states (over memory cap)
KLEE: WARNING: killing 12183 states (over memory cap)
KLEE: WARNING: killing 12403 states (over memory cap)
KLEE: WARNING: killing 11910 states (over memory cap)
KLEE: WARNING: killing 12718 states (over memory cap)
KLEE: WARNING: killing 11993 states (over memory cap)
KLEE: WARNING: killing 12799 states (over memory cap)
KLEE: WARNING: killing 12073 states (over memory cap)
KLEE: WARNING: killing 12059 states (over memory cap)
KLEE: WARNING: killing 12633 states (over memory cap)
KLEE: WARNING: killing 12500 states (over memory cap)
KLEE: WARNING: killing 12602 states (over memory cap)
KLEE: WARNING: killing 12118 states (over memory cap)
KLEE: WARNING: killing 12568 states (over memory cap)
KLEE: WARNING: killing 12088 states (over memory cap)
KLEE: WARNING: killing 12071 states (over memory cap)
KLEE: WARNING: killing 12289 states (over memory cap)
KLEE: WARNING: killing 12627 states (over memory cap)
KLEE: WARNING: killing 12492 states (over memory cap)
KLEE: WARNING: killing 11897 states (over memory cap)
KLEE: WARNING: killing 11647 states (over memory cap)
KLEE: WARNING: killing 22737 states (over memory cap)
KLEE: WARNING: killing 12539 states (over memory cap)
KLEE: WARNING: killing 11601 states (over memory cap)
KLEE: WARNING: killing 11813 states (over memory cap)
KLEE: WARNING: killing 22845 states (over memory cap)
KLEE: WARNING: killing 11885 states (over memory cap)
KLEE: WARNING: killing 22649 states (over memory cap)
KLEE: WARNING: killing 12068 states (over memory cap)
KLEE: WARNING: killing 12055 states (over memory cap)
KLEE: WARNING: killing 22195 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-KrY3F2/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-soc_camera-sh_mobile_ceu_camera_true-unreach-call.cil.c:11623: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12351 states (over memory cap)
KLEE: WARNING: killing 11776 states (over memory cap)
KLEE: WARNING: killing 12099 states (over memory cap)
KLEE: WARNING: killing 11742 states (over memory cap)
KLEE: WARNING: killing 11387 states (over memory cap)
KLEE: WARNING: killing 11604 states (over memory cap)
KLEE: WARNING: killing 11928 states (over memory cap)
KLEE: WARNING: killing 11579 states (over memory cap)
KLEE: WARNING: killing 11898 states (over memory cap)
KLEE: WARNING: killing 12228 states (over memory cap)
KLEE: WARNING: killing 11649 states (over memory cap)
KLEE: WARNING: killing 11971 states (over memory cap)
KLEE: WARNING: killing 11734 states (over memory cap)
KLEE: WARNING: killing 11835 states (over memory cap)
KLEE: WARNING: killing 12277 states (over memory cap)
KLEE: WARNING: killing 11591 states (over memory cap)
KLEE: WARNING: killing 11909 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 12444 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 11753 states (over memory cap)
KLEE: WARNING: killing 12299 states (over memory cap)
KLEE: WARNING: killing 11722 states (over memory cap)
KLEE: WARNING: killing 22383 states (over memory cap)
KLEE: WARNING: killing 12579 states (over memory cap)
KLEE: WARNING: killing 11461 states (over memory cap)
KLEE: WARNING: killing 12440 states (over memory cap)
KLEE: WARNING: killing 12101 states (over memory cap)
KLEE: WARNING: killing 11753 states (over memory cap)
KLEE: WARNING: killing 11740 states (over memory cap)
KLEE: WARNING: killing 11618 states (over memory cap)
KLEE: WARNING: killing 11496 states (over memory cap)
KLEE: WARNING: killing 11810 states (over memory cap)
KLEE: WARNING: killing 11802 states (over memory cap)
KLEE: WARNING: killing 11571 states (over memory cap)
KLEE: WARNING: killing 11338 states (over memory cap)
KLEE: WARNING: killing 12089 states (over memory cap)
KLEE: WARNING: killing 11533 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 11834 states (over memory cap)
KLEE: WARNING: killing 12264 states (over memory cap)
KLEE: WARNING: killing 12032 states (over memory cap)
KLEE: WARNING: killing 11692 states (over memory cap)
KLEE: WARNING: killing 12114 states (over memory cap)
KLEE: WARNING: killing 11774 states (over memory cap)
KLEE: WARNING: killing 11438 states (over memory cap)
KLEE: WARNING: killing 11315 states (over memory cap)
KLEE: WARNING: killing 11305 states (over memory cap)
KLEE: WARNING: killing 11296 states (over memory cap)
KLEE: WARNING: killing 11499 states (over memory cap)
KLEE: WARNING: killing 11814 states (over memory cap)
KLEE: WARNING: killing 12133 states (over memory cap)
KLEE: WARNING: killing 12009 states (over memory cap)
KLEE: WARNING: killing 11997 states (over memory cap)
KLEE: WARNING: killing 11991 states (over memory cap)
KLEE: WARNING: killing 11544 states (over memory cap)
KLEE: WARNING: killing 11749 states (over memory cap)
KLEE: WARNING: killing 11304 states (over memory cap)
KLEE: WARNING: killing 11939 states (over memory cap)
KLEE: WARNING: killing 12361 states (over memory cap)
KLEE: WARNING: killing 11706 states (over memory cap)
KLEE: WARNING: killing 11690 states (over memory cap)
KLEE: WARNING: killing 11786 states (over memory cap)
KLEE: WARNING: killing 11567 states (over memory cap)
KLEE: WARNING: killing 11550 states (over memory cap)
KLEE: WARNING: killing 11752 states (over memory cap)
KLEE: WARNING: killing 12164 states (over memory cap)
KLEE: WARNING: killing 12154 states (over memory cap)
KLEE: WARNING: killing 11719 states (over memory cap)
KLEE: WARNING: killing 12029 states (over memory cap)
KLEE: WARNING: killing 12122 states (over memory cap)
KLEE: WARNING: killing 11793 states (over memory cap)
KLEE: WARNING: killing 11996 states (over memory cap)
KLEE: WARNING: killing 11879 states (over memory cap)
KLEE: WARNING: killing 11657 states (over memory cap)
KLEE: WARNING: killing 11433 states (over memory cap)
KLEE: WARNING: killing 11951 states (over memory cap)
KLEE: WARNING: killing 11728 states (over memory cap)
KLEE: WARNING: killing 11717 states (over memory cap)
KLEE: WARNING: killing 11072 states (over memory cap)
KLEE: WARNING: killing 12013 states (over memory cap)
KLEE: WARNING: killing 11788 states (over memory cap)
KLEE: WARNING: killing 12201 states (over memory cap)
KLEE: WARNING: killing 11981 states (over memory cap)
KLEE: WARNING: killing 11441 states (over memory cap)
KLEE: WARNING: killing 11330 states (over memory cap)
KLEE: WARNING: killing 12049 states (over memory cap)
KLEE: WARNING: killing 11726 states (over memory cap)
KLEE: WARNING: killing 12233 states (over memory cap)
KLEE: WARNING: killing 11912 states (over memory cap)
KLEE: WARNING: killing 11899 states (over memory cap)
KLEE: WARNING: killing 11788 states (over memory cap)
KLEE: WARNING: killing 11987 states (over memory cap)
KLEE: WARNING: killing 12084 states (over memory cap)
KLEE: WARNING: killing 11966 states (over memory cap)
KLEE: WARNING: killing 11543 states (over memory cap)
KLEE: WARNING: killing 11529 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 11823 states (over memory cap)
KLEE: WARNING: killing 12015 states (over memory cap)
KLEE: WARNING: killing 11901 states (over memory cap)
KLEE: WARNING: killing 11887 states (over memory cap)
KLEE: WARNING: killing 12088 states (over memory cap)
KLEE: WARNING: killing 11663 states (over memory cap)
KLEE: WARNING: killing 11756 states (over memory cap)
KLEE: WARNING: killing 11535 states (over memory cap)
KLEE: WARNING: killing 11727 states (over memory cap)
KLEE: WARNING: killing 11617 states (over memory cap)
KLEE: WARNING: killing 11711 states (over memory cap)
KLEE: WARNING: killing 11393 states (over memory cap)
KLEE: WARNING: killing 11587 states (over memory cap)
KLEE: WARNING: killing 11475 states (over memory cap)
KLEE: WARNING: killing 11261 states (over memory cap)
KLEE: WARNING: killing 11454 states (over memory cap)
KLEE: WARNING: killing 11451 states (over memory cap)
KLEE: WARNING: killing 11743 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 11935 states (over memory cap)
KLEE: WARNING: killing 11819 states (over memory cap)
KLEE: WARNING: killing 12016 states (over memory cap)
KLEE: WARNING: killing 11493 states (over memory cap)
KLEE: WARNING: killing 11585 states (over memory cap)
KLEE: WARNING: killing 11878 states (over memory cap)
KLEE: WARNING: killing 12177 states (over memory cap)
KLEE: WARNING: killing 12164 states (over memory cap)
KLEE: WARNING: killing 11750 states (over memory cap)
KLEE: WARNING: killing 11330 states (over memory cap)
KLEE: WARNING: killing 12129 states (over memory cap)
KLEE: WARNING: killing 11618 states (over memory cap)
KLEE: WARNING: killing 11706 states (over memory cap)
KLEE: WARNING: killing 11796 states (over memory cap)
KLEE: WARNING: killing 11993 states (over memory cap)
KLEE: WARNING: killing 12078 states (over memory cap)
KLEE: WARNING: killing 11866 states (over memory cap)
KLEE: WARNING: killing 11755 states (over memory cap)
KLEE: WARNING: killing 11546 states (over memory cap)
KLEE: WARNING: killing 11631 states (over memory cap)
KLEE: WARNING: killing 12024 states (over memory cap)
KLEE: WARNING: killing 12119 states (over memory cap)
KLEE: WARNING: killing 11805 states (over memory cap)
KLEE: WARNING: killing 11693 states (over memory cap)
KLEE: WARNING: killing 11084 states (over memory cap)
KLEE: WARNING: killing 12070 states (over memory cap)
KLEE: WARNING: killing 12061 states (over memory cap)
KLEE: WARNING: killing 11956 states (over memory cap)
KLEE: WARNING: killing 11746 states (over memory cap)
KLEE: WARNING: killing 11432 states (over memory cap)
KLEE: WARNING: killing 12020 states (over memory cap)
KLEE: WARNING: killing 11015 states (over memory cap)
KLEE: WARNING: killing 11700 states (over memory cap)
KLEE: WARNING: killing 11889 states (over memory cap)
KLEE: WARNING: killing 11880 states (over memory cap)
KLEE: WARNING: killing 11770 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 11453 states (over memory cap)
KLEE: WARNING: killing 11146 states (over memory cap)
KLEE: WARNING: killing 11631 states (over memory cap)
KLEE: WARNING: killing 11623 states (over memory cap)
KLEE: WARNING: killing 12210 states (over memory cap)
KLEE: WARNING: killing 11708 states (over memory cap)
KLEE: WARNING: killing 11696 states (over memory cap)
KLEE: WARNING: killing 11391 states (over memory cap)
KLEE: WARNING: killing 11383 states (over memory cap)
KLEE: WARNING: killing 11663 states (over memory cap)
KLEE: WARNING: killing 11455 states (over memory cap)
KLEE: WARNING: killing 11642 states (over memory cap)
