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-kernel-locking-mutex__drivers-media-radio-radio-si476x_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.: 250 307 2418 11800
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.475616931915
Defining function default_llseek as symbolic
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function __kfifo_to_user as symbolic
Defining function dev_warn as symbolic
Defining function video_devdata as symbolic
Defining function v4l2_ctrl_poll as symbolic
Defining function simple_read_from_buffer as symbolic
Defining function video_ioctl2 as symbolic
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function __platform_driver_register as symbolic
Defining function si476x_core_has_diversity as symbolic
Removed calls to 'regcache_cache_only' (function is undefined)
Defining function regmap_update_bits as symbolic
Defining function regmap_write as symbolic
Defining function si476x_core_is_in_am_receiver_mode as symbolic
Defining function si476x_core_cmd_fm_rds_status as symbolic
Defining function regmap_read as symbolic
Defining function si476x_core_is_a_secondary_tuner as symbolic
Defining function strlcpy as symbolic
Defining function si476x_core_has_am as symbolic
Defining function si476x_core_is_a_primary_tuner as symbolic
Defining function snprintf as symbolic
Defining function si476x_core_stop as symbolic
Defining function si476x_core_start as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function regcache_sync_region as symbolic
Defining function si476x_core_cmd_fm_phase_diversity as symbolic
Defining function si476x_core_cmd_fm_tune_freq as symbolic
Defining function si476x_core_cmd_fm_seek_start as symbolic
Defining function si476x_core_cmd_fm_rsq_status as symbolic
Defining function si476x_core_cmd_fm_rds_blockcount as symbolic
Defining function si476x_core_cmd_fm_phase_div_status as symbolic
Defining function si476x_core_cmd_fm_acf_status as symbolic
Defining function si476x_core_cmd_agc_status as symbolic
Defining function si476x_core_cmd_am_tune_freq as symbolic
Defining function si476x_core_cmd_am_seek_start as symbolic
Defining function si476x_core_cmd_am_rsq_status as symbolic
Defining function si476x_core_cmd_am_acf_status as symbolic
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Defining function v4l2_device_set_name as symbolic
Defining function v4l2_device_register as symbolic
Defining function dev_err as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std_menu as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function __video_register_device as symbolic
Defining function v4l2_ctrl_new_custom as symbolic
Defining function devm_kmalloc as symbolic
Defining function si476x_core_set_power_state as symbolic
Defining function v4l2_fh_release as symbolic
Defining function v4l2_fh_is_singular as symbolic
Defining function v4l2_fh_open as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Defining function simple_open as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'video_device_release_empty' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  __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.527983903885
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 320 325 1211 7436
INFO: Starting verification
KLEE: WARNING ONCE: function "si476x_radio_probe" has inline asm
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_8a667f4b-c7ee-4db9-af1a-fb5d852e871d/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 24478 states (over memory cap)
KLEE: WARNING: killing 17663 states (over memory cap)
KLEE: WARNING: killing 17144 states (over memory cap)
KLEE: WARNING: killing 16638 states (over memory cap)
KLEE: WARNING: killing 16130 states (over memory cap)
KLEE: WARNING: killing 16554 states (over memory cap)
KLEE: WARNING: killing 16834 states (over memory cap)
KLEE: WARNING: killing 16799 states (over memory cap)
KLEE: WARNING: killing 16466 states (over memory cap)
KLEE: WARNING: killing 16133 states (over memory cap)
KLEE: WARNING: killing 15487 states (over memory cap)
KLEE: WARNING: killing 16690 states (over memory cap)
KLEE: WARNING: killing 15898 states (over memory cap)
KLEE: WARNING: killing 15717 states (over memory cap)
KLEE: WARNING: killing 16760 states (over memory cap)
KLEE: WARNING: killing 16275 states (over memory cap)
KLEE: WARNING: killing 16559 states (over memory cap)
KLEE: WARNING: killing 15616 states (over memory cap)
KLEE: WARNING: killing 17417 states (over memory cap)
KLEE: WARNING: killing 16942 states (over memory cap)
KLEE: WARNING: killing 16758 states (over memory cap)
KLEE: WARNING: killing 17184 states (over memory cap)
KLEE: WARNING: killing 17312 states (over memory cap)
KLEE: WARNING: killing 18937 states (over memory cap)
KLEE: WARNING: killing 17701 states (over memory cap)
KLEE: WARNING: killing 18424 states (over memory cap)
KLEE: WARNING: killing 18396 states (over memory cap)
KLEE: WARNING: killing 18518 states (over memory cap)
KLEE: WARNING: killing 18790 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ObnaVW/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-radio-radio-si476x_true-unreach-call.cil.c:7250: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18158 states (over memory cap)
KLEE: WARNING: killing 19628 states (over memory cap)
KLEE: WARNING: killing 19156 states (over memory cap)
KLEE: WARNING: killing 18979 states (over memory cap)
KLEE: WARNING: killing 19256 states (over memory cap)
KLEE: WARNING: killing 19079 states (over memory cap)
KLEE: WARNING: killing 19792 states (over memory cap)
KLEE: WARNING: killing 19175 states (over memory cap)
KLEE: WARNING: killing 19307 states (over memory cap)
KLEE: WARNING: killing 19724 states (over memory cap)
KLEE: WARNING: killing 18957 states (over memory cap)
KLEE: WARNING: killing 18930 states (over memory cap)
KLEE: WARNING: killing 19053 states (over memory cap)
KLEE: WARNING: killing 19622 states (over memory cap)
KLEE: WARNING: killing 18710 states (over memory cap)
KLEE: WARNING: killing 19281 states (over memory cap)
KLEE: WARNING: killing 17941 states (over memory cap)
KLEE: WARNING: killing 17910 states (over memory cap)
KLEE: WARNING: killing 17744 states (over memory cap)
KLEE: WARNING: killing 18596 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ObnaVW/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-radio-radio-si476x_true-unreach-call.cil.c:13914: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18421 states (over memory cap)
KLEE: WARNING: killing 17820 states (over memory cap)
KLEE: WARNING: killing 18383 states (over memory cap)
KLEE: WARNING: killing 17634 states (over memory cap)
KLEE: WARNING: killing 18045 states (over memory cap)
KLEE: WARNING: killing 18316 states (over memory cap)
KLEE: WARNING: killing 17574 states (over memory cap)
KLEE: WARNING: killing 18127 states (over memory cap)
KLEE: WARNING: killing 17531 states (over memory cap)
KLEE: WARNING: killing 17504 states (over memory cap)
KLEE: WARNING: killing 17620 states (over memory cap)
KLEE: WARNING: killing 17464 states (over memory cap)
KLEE: WARNING: killing 18456 states (over memory cap)
KLEE: WARNING: killing 17564 states (over memory cap)
KLEE: WARNING: killing 17981 states (over memory cap)
KLEE: WARNING: killing 17821 states (over memory cap)
KLEE: WARNING: killing 18804 states (over memory cap)
KLEE: WARNING: killing 17924 states (over memory cap)
KLEE: WARNING: killing 17910 states (over memory cap)
KLEE: WARNING: killing 17886 states (over memory cap)
KLEE: WARNING: killing 18443 states (over memory cap)
KLEE: WARNING: killing 18001 states (over memory cap)
KLEE: WARNING: killing 17971 states (over memory cap)
KLEE: WARNING: killing 17665 states (over memory cap)
KLEE: WARNING: killing 17795 states (over memory cap)
KLEE: WARNING: killing 18193 states (over memory cap)
KLEE: WARNING: killing 17748 states (over memory cap)
KLEE: WARNING: killing 18300 states (over memory cap)
KLEE: WARNING: killing 17006 states (over memory cap)
KLEE: WARNING: killing 17691 states (over memory cap)
KLEE: WARNING: killing 18095 states (over memory cap)
KLEE: WARNING: killing 17937 states (over memory cap)
KLEE: WARNING: killing 18202 states (over memory cap)
KLEE: WARNING: killing 18044 states (over memory cap)
KLEE: WARNING: killing 18593 states (over memory cap)
KLEE: WARNING: killing 18153 states (over memory cap)
KLEE: WARNING: killing 17989 states (over memory cap)
KLEE: WARNING: killing 18532 states (over memory cap)
KLEE: WARNING: killing 17680 states (over memory cap)
KLEE: WARNING: killing 19200 states (over memory cap)
KLEE: WARNING: killing 17639 states (over memory cap)
KLEE: WARNING: killing 17753 states (over memory cap)
KLEE: WARNING: killing 18161 states (over memory cap)
KLEE: WARNING: killing 18144 states (over memory cap)
KLEE: WARNING: killing 17699 states (over memory cap)
KLEE: WARNING: killing 18519 states (over memory cap)
KLEE: WARNING: killing 18366 states (over memory cap)
KLEE: WARNING: killing 18340 states (over memory cap)
KLEE: WARNING: killing 17486 states (over memory cap)
KLEE: WARNING: killing 17320 states (over memory cap)
KLEE: WARNING: killing 18132 states (over memory cap)
KLEE: WARNING: killing 18119 states (over memory cap)
KLEE: WARNING: killing 18797 states (over memory cap)
KLEE: WARNING: killing 17670 states (over memory cap)
KLEE: WARNING: killing 17094 states (over memory cap)
KLEE: WARNING: killing 18456 states (over memory cap)
KLEE: WARNING: killing 18171 states (over memory cap)
KLEE: WARNING: killing 18145 states (over memory cap)
KLEE: WARNING: killing 17298 states (over memory cap)
KLEE: WARNING: killing 18386 states (over memory cap)
KLEE: WARNING: killing 17819 states (over memory cap)
KLEE: WARNING: killing 18351 states (over memory cap)
KLEE: WARNING: killing 17234 states (over memory cap)
KLEE: WARNING: killing 17896 states (over memory cap)
KLEE: WARNING: killing 17055 states (over memory cap)
KLEE: WARNING: killing 17590 states (over memory cap)
KLEE: WARNING: killing 17972 states (over memory cap)
KLEE: WARNING: killing 17412 states (over memory cap)
KLEE: WARNING: killing 18766 states (over memory cap)
KLEE: WARNING: killing 18065 states (over memory cap)
KLEE: WARNING: killing 17776 states (over memory cap)
KLEE: WARNING: killing 18307 states (over memory cap)
KLEE: WARNING: killing 18012 states (over memory cap)
KLEE: WARNING: killing 18271 states (over memory cap)
KLEE: WARNING: killing 18394 states (over memory cap)
KLEE: WARNING: killing 17824 states (over memory cap)
KLEE: WARNING: killing 17666 states (over memory cap)
KLEE: WARNING: killing 16969 states (over memory cap)
