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-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-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.: 1344 715 7457 45474
Removed infinite loop in v4l2_norm_to_name
Removed infinite loop in arch_local_save_flags
Removed infinite loop in v4l2_event_subscribed
Removed infinite loop in v4l2_subdev_init
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.43903493881
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Defining function printk as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function cdev_alloc as symbolic
Defining function cdev_add as symbolic
Defining function dev_set_name as symbolic
Defining function device_register as symbolic
Removed calls to 'media_device_unregister_entity' (function is undefined)
Defining function media_device_register_entity as symbolic
Defining function __bitmap_andnot as symbolic
Defining function find_first_zero_bit as symbolic
Defining function find_next_zero_bit as symbolic
Removed calls to 'device_unregister' (function is undefined)
Defining function strlcpy as symbolic
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function _copy_from_user as symbolic
Defining function get_device as symbolic
Defining function snprintf as symbolic
Removed calls to 'put_device' (function is undefined)
Removed calls to 'i2c_unregister_device' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'media_entity_remove_links' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function try_module_get as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to 'ktime_get_ts64' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'media_entity_put' (function is undefined)
Defining function media_entity_get as symbolic
Defining function capable as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'clk_put' (function is undefined)
Defining function clk_get as symbolic
Removed calls to 'clk_unprepare' (function is undefined)
Defining function clk_prepare as symbolic
Defining function clk_enable as symbolic
Defining function clk_get_rate as symbolic
Defining function clk_round_rate as symbolic
Defining function clk_set_rate as symbolic
Defining function kstrdup as symbolic
Removed calls to 'dev_err' (function is undefined)
Defining function i2c_verify_client as symbolic
Removed calls to 'device_release_driver' (function is undefined)
Defining function device_attach as symbolic
Defining function mutex_trylock as symbolic
Defining function copy_in_user as symbolic
Defining function compat_put_timespec as symbolic
Defining function compat_alloc_user_space as symbolic
Defining function of_graph_parse_endpoint as symbolic
Defining function of_get_property as symbolic
Defining function of_property_read_u32_array as symbolic
Defining function of_find_property as symbolic
Defining function of_prop_next_u32 as symbolic
Defining function of_property_read_u64_array as symbolic
Removed calls to 'of_node_put' (function is undefined)
Defining function of_get_parent as symbolic
Defining function of_get_next_parent as symbolic
Defining function strcasecmp as symbolic
Defining function of_parse_phandle as symbolic
Defining function no_llseek as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function sprintf as symbolic
Defining function kstrtou16 as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'class_unregister' (function is undefined)
Removed calls to 'unregister_chrdev_region' (function is undefined)
Removed calls to 'trace_seq_printf' (function is undefined)
Defining function register_chrdev_region as symbolic
Defining function __class_register as symbolic
Defining function ldv_setup_4 as symbolic
Defining function ldv_release_4 as symbolic
Defining function trace_raw_output_prep as symbolic
Defining function trace_print_flags_seq as symbolic
Defining function trace_print_symbols_seq as symbolic
Defining function ldv_release_2 as symbolic
Defining function trace_event_raw_init as symbolic
Defining function trace_event_reg as symbolic
Defining function trace_define_field as symbolic
Defining function ldv_release_3 as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  __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.36210680008
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1550 633 4460 26317
INFO: Starting verification
KLEE: WARNING ONCE: function "v4l2_prio_change" has inline asm
KLEE: WARNING ONCE: function "v4l2_prio_open" has inline asm
KLEE: WARNING ONCE: function "v4l2_prio_close" has inline asm
KLEE: WARNING ONCE: function "__video_register_device" has inline asm
KLEE: WARNING ONCE: function "v4l2_device_release" has inline asm
KLEE: WARNING ONCE: function "v4l2_device_put" has inline asm
KLEE: WARNING ONCE: function "video_unregister_device" has inline asm
KLEE: WARNING ONCE: function "v4l2_norm_to_name" has inline asm
KLEE: WARNING ONCE: function "video_usercopy" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "__video_do_ioctl" has inline asm
KLEE: WARNING ONCE: function "v4l2_device_set_name" has inline asm
KLEE: WARNING ONCE: function "v4l2_fh_init" has inline asm
KLEE: WARNING ONCE: function "v4l2_fh_add" has inline asm
KLEE: WARNING ONCE: function "v4l2_fh_del" has inline asm
KLEE: WARNING ONCE: function "v4l2_event_subscribed" has inline asm
KLEE: WARNING ONCE: function "v4l2_ctrl_activate" has inline asm
KLEE: WARNING ONCE: function "v4l2_ctrl_grab" has inline asm
KLEE: WARNING ONCE: function "v4l2_subdev_init" has inline asm
KLEE: WARNING ONCE: function "v4l2_clk_get" has inline asm
KLEE: WARNING ONCE: function "v4l2_clk_put" has inline asm
KLEE: WARNING ONCE: function "v4l2_compat_ioctl32" has inline asm
KLEE: WARNING ONCE: function "__get_v4l2_format32" has inline asm
KLEE: WARNING ONCE: function "__put_v4l2_format32" has inline asm
KLEE: WARNING ONCE: function "v4l2_ioctl_get_lock" has inline asm
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_fd46c51f-77ea-40bd-b07e-cb4619e96b35/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16827 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17859 states (over memory cap)
KLEE: WARNING: killing 17642 states (over memory cap)
KLEE: WARNING: killing 16685 states (over memory cap)
KLEE: WARNING: killing 17383 states (over memory cap)
KLEE: WARNING: killing 18702 states (over memory cap)
KLEE: WARNING: killing 17701 states (over memory cap)
KLEE: WARNING: killing 17049 states (over memory cap)
KLEE: WARNING: killing 18312 states (over memory cap)
KLEE: WARNING: killing 19349 states (over memory cap)
KLEE: WARNING: killing 18712 states (over memory cap)
KLEE: WARNING: killing 18908 states (over memory cap)
KLEE: WARNING: killing 20227 states (over memory cap)
KLEE: WARNING: killing 19259 states (over memory cap)
KLEE: WARNING: killing 19563 states (over memory cap)
KLEE: WARNING: killing 19433 states (over memory cap)
KLEE: WARNING: killing 19130 states (over memory cap)
KLEE: WARNING: killing 19442 states (over memory cap)
KLEE: WARNING: killing 18638 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:22179: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:6941: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:6464: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:7022: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18667 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:6905: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:7057: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19028 states (over memory cap)
KLEE: WARNING: killing 18614 states (over memory cap)
KLEE: WARNING: killing 18306 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:6447: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18886 states (over memory cap)
KLEE: WARNING: killing 18809 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:23868: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19373 states (over memory cap)
KLEE: WARNING: killing 18910 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:23838: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:23000: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:22147: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19165 states (over memory cap)
KLEE: WARNING: killing 19473 states (over memory cap)
KLEE: WARNING: killing 19508 states (over memory cap)
KLEE: WARNING: killing 18279 states (over memory cap)
KLEE: WARNING: killing 19687 states (over memory cap)
KLEE: WARNING: killing 18401 states (over memory cap)
KLEE: WARNING: killing 19041 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:6486: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19781 states (over memory cap)
KLEE: WARNING: killing 19219 states (over memory cap)
KLEE: WARNING: killing 18594 states (over memory cap)
KLEE: WARNING: killing 19225 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-04tJCP/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point_false-unreach-call.cil.out.c:23277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18445 states (over memory cap)
KLEE: WARNING: killing 18854 states (over memory cap)
KLEE: WARNING: killing 19649 states (over memory cap)
KLEE: WARNING: killing 18877 states (over memory cap)
KLEE: WARNING: killing 19282 states (over memory cap)
KLEE: WARNING: killing 19269 states (over memory cap)
KLEE: WARNING: killing 18706 states (over memory cap)
KLEE: WARNING: killing 19224 states (over memory cap)
KLEE: WARNING: killing 18445 states (over memory cap)
KLEE: WARNING: killing 19179 states (over memory cap)
KLEE: WARNING: killing 19971 states (over memory cap)
KLEE: WARNING: killing 18654 states (over memory cap)
KLEE: WARNING: killing 18685 states (over memory cap)
KLEE: WARNING: killing 18775 states (over memory cap)
KLEE: WARNING: killing 18756 states (over memory cap)
KLEE: WARNING: killing 20133 states (over memory cap)
KLEE: WARNING: killing 18344 states (over memory cap)
KLEE: WARNING: killing 20207 states (over memory cap)
KLEE: WARNING: killing 19333 states (over memory cap)
KLEE: WARNING: killing 18826 states (over memory cap)
KLEE: WARNING: killing 18540 states (over memory cap)
KLEE: WARNING: killing 18948 states (over memory cap)
KLEE: WARNING: killing 19032 states (over memory cap)
KLEE: WARNING: killing 19017 states (over memory cap)
KLEE: WARNING: killing 19529 states (over memory cap)
KLEE: WARNING: killing 19079 states (over memory cap)
KLEE: WARNING: killing 19542 states (over memory cap)
KLEE: WARNING: killing 19149 states (over memory cap)
KLEE: WARNING: killing 18651 states (over memory cap)
KLEE: WARNING: killing 19436 states (over memory cap)
KLEE: WARNING: killing 19527 states (over memory cap)
KLEE: WARNING: killing 19082 states (over memory cap)
KLEE: WARNING: killing 18745 states (over memory cap)
KLEE: WARNING: killing 18570 states (over memory cap)
KLEE: WARNING: killing 18926 states (over memory cap)
KLEE: WARNING: killing 19385 states (over memory cap)
KLEE: WARNING: killing 19576 states (over memory cap)
KLEE: WARNING: killing 18563 states (over memory cap)
KLEE: WARNING: killing 18855 states (over memory cap)
KLEE: WARNING: killing 18733 states (over memory cap)
KLEE: WARNING: killing 18928 states (over memory cap)
KLEE: WARNING: killing 19856 states (over memory cap)
KLEE: WARNING: killing 18951 states (over memory cap)
KLEE: WARNING: killing 19342 states (over memory cap)
KLEE: WARNING: killing 18808 states (over memory cap)
KLEE: WARNING: killing 19315 states (over memory cap)
KLEE: WARNING: killing 18407 states (over memory cap)
KLEE: WARNING: killing 19543 states (over memory cap)
KLEE: WARNING: killing 18897 states (over memory cap)
KLEE: WARNING: killing 18778 states (over memory cap)
KLEE: WARNING: killing 18662 states (over memory cap)
KLEE: WARNING: killing 18589 states (over memory cap)
KLEE: WARNING: killing 17848 states (over memory cap)
KLEE: WARNING: killing 19184 states (over memory cap)
KLEE: WARNING: killing 18803 states (over memory cap)
KLEE: WARNING: killing 19412 states (over memory cap)
KLEE: WARNING: killing 18101 states (over memory cap)
KLEE: WARNING: killing 19950 states (over memory cap)
KLEE: WARNING: killing 18643 states (over memory cap)
KLEE: WARNING: killing 19925 states (over memory cap)
KLEE: WARNING: killing 19184 states (over memory cap)
KLEE: WARNING: killing 18544 states (over memory cap)
KLEE: WARNING: killing 19459 states (over memory cap)
KLEE: WARNING: killing 18980 states (over memory cap)
KLEE: WARNING: killing 19225 states (over memory cap)
KLEE: WARNING: killing 19257 states (over memory cap)
KLEE: WARNING: killing 18373 states (over memory cap)
KLEE: WARNING: killing 18761 states (over memory cap)
KLEE: WARNING: killing 18950 states (over memory cap)
KLEE: WARNING: killing 19444 states (over memory cap)
KLEE: WARNING: killing 19124 states (over memory cap)
KLEE: WARNING: killing 18699 states (over memory cap)
KLEE: WARNING: killing 19616 states (over memory cap)
KLEE: WARNING: killing 18362 states (over memory cap)
KLEE: WARNING: killing 19269 states (over memory cap)
KLEE: WARNING: killing 18945 states (over memory cap)
KLEE: WARNING: killing 19236 states (over memory cap)
KLEE: WARNING: killing 18615 states (over memory cap)
KLEE: WARNING: killing 18802 states (over memory cap)
KLEE: WARNING: killing 19294 states (over memory cap)
KLEE: WARNING: killing 18918 states (over memory cap)
KLEE: WARNING: killing 18804 states (over memory cap)
KLEE: WARNING: killing 18537 states (over memory cap)
KLEE: WARNING: killing 18781 states (over memory cap)
KLEE: WARNING: killing 19782 states (over memory cap)
KLEE: WARNING: killing 19411 states (over memory cap)
KLEE: WARNING: killing 18994 states (over memory cap)
KLEE: WARNING: killing 18360 states (over memory cap)
KLEE: WARNING: killing 18495 states (over memory cap)
KLEE: WARNING: killing 19183 states (over memory cap)
KLEE: WARNING: killing 19169 states (over memory cap)
KLEE: WARNING: killing 19255 states (over memory cap)
KLEE: WARNING: killing 19286 states (over memory cap)
KLEE: WARNING: killing 19979 states (over memory cap)
KLEE: WARNING: killing 18560 states (over memory cap)
