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-drivers-clk1__drivers-media-pci-zoran-zr36067_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.: 779 540 5311 32888
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.04191994667
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function PDE_DATA as symbolic
Defining function vmalloc as symbolic
Defining function printk as symbolic
Defining function strpbrk as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function atomic_dec_and_mutex_lock as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function remap_pfn_range as symbolic
Defining function video_ioctl2 as symbolic
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function snprintf as symbolic
Defining function get_zeroed_page as symbolic
Defining function capable as symbolic
Removed calls to 'v4l_bound_align_image' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'v4l2_get_timestamp' (function is undefined)
Defining function pci_bus_write_config_dword as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function video_devdata as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Defining function videocodec_detach as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_ioremap_bar as symbolic
Defining function v4l2_i2c_new_subdev as symbolic
Defining function __request_module as symbolic
Defining function videocodec_attach as symbolic
Defining function proc_create_data as symbolic
Defining function video_device_alloc as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function __video_register_device as symbolic
Defining function strlcpy as symbolic
Defining function i2c_bit_add_bus as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function request_threaded_irq as symbolic
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 'ldv_assert' (function is undefined)
Defining function strchr as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  strncmp
  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: 0.980426073074
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 855 521 2400 19613
INFO: Starting verification
KLEE: WARNING ONCE: function "zoran_write" has inline asm
KLEE: WARNING ONCE: function "zr36057_set_memgrab" has inline asm
KLEE: WARNING ONCE: function "v4l_fbuffer_free" has inline asm
KLEE: WARNING ONCE: function "jpg_fbuffer_free" has inline asm
KLEE: WARNING ONCE: function "zr36057_enable_jpg" has inline asm
KLEE: WARNING ONCE: function "set_videobus_dir" has inline asm
KLEE: WARNING ONCE: function "jpeg_codec_reset" has inline asm
KLEE: WARNING ONCE: function "jpeg_codec_sleep" has inline asm
KLEE: WARNING ONCE: function "zr36057_adjust_vfe" has inline asm
KLEE: WARNING ONCE: function "zr36057_set_jpg" has inline asm
KLEE: WARNING ONCE: function "post_office_wait" has inline asm
KLEE: WARNING ONCE: function "zr36057_set_vfe" has inline asm
KLEE: WARNING ONCE: function "zr36057_overlay" has inline asm
KLEE: WARNING ONCE: function "zoran_vm_open" has inline asm
KLEE: WARNING ONCE: function "zoran_dqbuf" has inline asm
KLEE: WARNING ONCE: function "zoran_overlay" has inline asm
KLEE: WARNING ONCE: function "wait_grab_pending" has inline asm
KLEE: WARNING ONCE: function "zoran_reqbufs" has inline asm
KLEE: WARNING ONCE: function "zoran_s_fmt_vid_overlay" has inline asm
KLEE: WARNING ONCE: function "zoran_s_std" has inline asm
KLEE: WARNING ONCE: function "jpeg_start" has inline asm
KLEE: WARNING ONCE: function "zr36016_write" has inline asm
KLEE: WARNING ONCE: function "zoran_irq" has inline asm
KLEE: WARNING ONCE: function "count_reset_interrupt" has inline asm
KLEE: WARNING ONCE: function "post_office_read" has inline asm
KLEE: WARNING ONCE: function "zoran_i2c_getscl" has inline asm
KLEE: WARNING ONCE: function "zoran_i2c_getsda" has inline asm
KLEE: WARNING ONCE: function "zoran_i2c_setscl" has inline asm
KLEE: WARNING ONCE: function "zoran_i2c_setsda" has inline asm
KLEE: WARNING ONCE: function "avs6eyes_init" has inline asm
KLEE: WARNING ONCE: function "dc10_init" has inline asm
KLEE: WARNING ONCE: function "lml33_init" has inline asm
KLEE: WARNING ONCE: function "zoran_show" has inline asm
KLEE: WARNING ONCE: function "zoran_open___0" has inline asm
KLEE: WARNING ONCE: function "zoran_close" has inline asm
KLEE: WARNING ONCE: function "zr36057_restart" has inline asm
KLEE: WARNING ONCE: function "zoran_init_hardware" has inline asm
KLEE: WARNING ONCE: function "zoran_probe" has inline asm
KLEE: WARNING ONCE: function "zoran_remove" has inline asm
KLEE: WARNING ONCE: function "zoran_subdev_notify" has inline asm
KLEE: WARNING ONCE: function "zr36060_read" has inline asm
KLEE: WARNING ONCE: function "zr36060_write" has inline asm
KLEE: WARNING ONCE: function "zr36050_read" has inline asm
KLEE: WARNING ONCE: function "zr36050_write" has inline asm
KLEE: WARNING ONCE: function "post_office_write" has inline asm
KLEE: WARNING ONCE: function "GPIO" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_4_7" has inline asm
KLEE: WARNING ONCE: function "ldv_base_instance_callback_3_24" has inline asm
KLEE: WARNING ONCE: function "ldv_base_instance_callback_3_27" has inline asm
KLEE: WARNING ONCE: function "ldv_base_instance_callback_3_30" has inline asm
KLEE: WARNING ONCE: function "ldv_base_instance_callback_3_9" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_i2c_algo_bit_data_base_instance_3" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_vm_operations_struct_dummy_resourceless_instance_4" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_1e5b5c09-1e1c-4d1b-b332-8a001d0f1e96/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 18671 states (over memory cap)
KLEE: WARNING: killing 14335 states (over memory cap)
KLEE: WARNING: killing 12664 states (over memory cap)
KLEE: WARNING: killing 12754 states (over memory cap)
KLEE: WARNING: killing 12596 states (over memory cap)
KLEE: WARNING: killing 12572 states (over memory cap)
KLEE: WARNING: killing 23737 states (over memory cap)
KLEE: WARNING: killing 23786 states (over memory cap)
KLEE: WARNING: killing 23861 states (over memory cap)
KLEE: WARNING: killing 13187 states (over memory cap)
KLEE: WARNING: killing 24416 states (over memory cap)
KLEE: WARNING: killing 14018 states (over memory cap)
KLEE: WARNING: killing 12646 states (over memory cap)
KLEE: WARNING: killing 13368 states (over memory cap)
KLEE: WARNING: killing 12979 states (over memory cap)
KLEE: WARNING: killing 12957 states (over memory cap)
KLEE: WARNING: killing 13798 states (over memory cap)
KLEE: WARNING: killing 14390 states (over memory cap)
KLEE: WARNING: killing 13146 states (over memory cap)
KLEE: WARNING: killing 13854 states (over memory cap)
KLEE: WARNING: killing 14080 states (over memory cap)
KLEE: WARNING: killing 14424 states (over memory cap)
KLEE: WARNING: killing 14395 states (over memory cap)
KLEE: WARNING: killing 14140 states (over memory cap)
KLEE: WARNING: killing 14972 states (over memory cap)
KLEE: WARNING: killing 14837 states (over memory cap)
KLEE: WARNING: killing 15184 states (over memory cap)
KLEE: WARNING: killing 15039 states (over memory cap)
KLEE: WARNING: killing 14899 states (over memory cap)
KLEE: WARNING: killing 15237 states (over memory cap)
KLEE: WARNING: killing 14236 states (over memory cap)
KLEE: WARNING: killing 14938 states (over memory cap)
KLEE: WARNING: killing 14797 states (over memory cap)
KLEE: WARNING: killing 14537 states (over memory cap)
KLEE: WARNING: killing 13551 states (over memory cap)
KLEE: WARNING: killing 14252 states (over memory cap)
KLEE: WARNING: killing 13519 states (over memory cap)
KLEE: WARNING: killing 14097 states (over memory cap)
KLEE: WARNING: killing 14075 states (over memory cap)
KLEE: WARNING: killing 13224 states (over memory cap)
KLEE: WARNING: killing 13686 states (over memory cap)
KLEE: WARNING: killing 13672 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13996 states (over memory cap)
KLEE: WARNING: killing 13626 states (over memory cap)
KLEE: WARNING: killing 13725 states (over memory cap)
KLEE: WARNING: killing 13833 states (over memory cap)
KLEE: WARNING: killing 13344 states (over memory cap)
KLEE: WARNING: killing 13922 states (over memory cap)
KLEE: WARNING: killing 13430 states (over memory cap)
KLEE: WARNING: killing 13426 states (over memory cap)
KLEE: WARNING: killing 13755 states (over memory cap)
KLEE: WARNING: killing 13625 states (over memory cap)
KLEE: WARNING: killing 13489 states (over memory cap)
KLEE: WARNING: killing 13474 states (over memory cap)
KLEE: WARNING: killing 14393 states (over memory cap)
KLEE: WARNING: killing 13561 states (over memory cap)
KLEE: WARNING: killing 13430 states (over memory cap)
KLEE: WARNING: killing 13880 states (over memory cap)
KLEE: WARNING: killing 13749 states (over memory cap)
KLEE: WARNING: killing 13499 states (over memory cap)
KLEE: WARNING: killing 13836 states (over memory cap)
KLEE: WARNING: killing 13123 states (over memory cap)
KLEE: WARNING: killing 13456 states (over memory cap)
KLEE: WARNING: killing 13784 states (over memory cap)
KLEE: WARNING: killing 13774 states (over memory cap)
KLEE: WARNING: killing 14222 states (over memory cap)
KLEE: WARNING: killing 13866 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 14069 states (over memory cap)
KLEE: WARNING: killing 14173 states (over memory cap)
KLEE: WARNING: killing 13574 states (over memory cap)
KLEE: WARNING: killing 13786 states (over memory cap)
KLEE: WARNING: killing 13306 states (over memory cap)
KLEE: WARNING: killing 13752 states (over memory cap)
KLEE: WARNING: killing 14084 states (over memory cap)
KLEE: WARNING: killing 13958 states (over memory cap)
KLEE: WARNING: killing 14055 states (over memory cap)
KLEE: WARNING: killing 13801 states (over memory cap)
KLEE: WARNING: killing 13795 states (over memory cap)
KLEE: WARNING: killing 14238 states (over memory cap)
KLEE: WARNING: killing 13767 states (over memory cap)
KLEE: WARNING: killing 13299 states (over memory cap)
KLEE: WARNING: killing 13738 states (over memory cap)
KLEE: WARNING: killing 13498 states (over memory cap)
KLEE: WARNING: killing 13480 states (over memory cap)
KLEE: WARNING: killing 13576 states (over memory cap)
KLEE: WARNING: killing 13907 states (over memory cap)
KLEE: WARNING: killing 13665 states (over memory cap)
KLEE: WARNING: killing 13654 states (over memory cap)
KLEE: WARNING: killing 14200 states (over memory cap)
KLEE: WARNING: killing 14182 states (over memory cap)
KLEE: WARNING: killing 14062 states (over memory cap)
KLEE: WARNING: killing 13706 states (over memory cap)
KLEE: WARNING: killing 14025 states (over memory cap)
KLEE: WARNING: killing 13793 states (over memory cap)
KLEE: WARNING: killing 14224 states (over memory cap)
KLEE: WARNING: killing 13654 states (over memory cap)
KLEE: WARNING: killing 13522 states (over memory cap)
KLEE: WARNING: killing 13396 states (over memory cap)
KLEE: WARNING: killing 13718 states (over memory cap)
KLEE: WARNING: killing 14608 states (over memory cap)
KLEE: WARNING: killing 13805 states (over memory cap)
KLEE: WARNING: killing 13341 states (over memory cap)
KLEE: WARNING: killing 13101 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13525 states (over memory cap)
KLEE: WARNING: killing 13847 states (over memory cap)
KLEE: WARNING: killing 13611 states (over memory cap)
KLEE: WARNING: killing 13602 states (over memory cap)
KLEE: WARNING: killing 13918 states (over memory cap)
KLEE: WARNING: killing 13345 states (over memory cap)
KLEE: WARNING: killing 13440 states (over memory cap)
KLEE: WARNING: killing 13977 states (over memory cap)
KLEE: WARNING: killing 13423 states (over memory cap)
KLEE: WARNING: killing 13742 states (over memory cap)
KLEE: WARNING: killing 14493 states (over memory cap)
KLEE: WARNING: killing 13932 states (over memory cap)
KLEE: WARNING: killing 13584 states (over memory cap)
KLEE: WARNING: killing 13250 states (over memory cap)
KLEE: WARNING: killing 13668 states (over memory cap)
KLEE: WARNING: killing 13652 states (over memory cap)
KLEE: WARNING: killing 13864 states (over memory cap)
KLEE: WARNING: killing 14068 states (over memory cap)
KLEE: WARNING: killing 13511 states (over memory cap)
KLEE: WARNING: killing 13938 states (over memory cap)
KLEE: WARNING: killing 13481 states (over memory cap)
KLEE: WARNING: killing 13903 states (over memory cap)
KLEE: WARNING: killing 13239 states (over memory cap)
KLEE: WARNING: killing 13440 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13963 states (over memory cap)
KLEE: WARNING: killing 13406 states (over memory cap)
KLEE: WARNING: killing 13722 states (over memory cap)
KLEE: WARNING: killing 13920 states (over memory cap)
KLEE: WARNING: killing 13802 states (over memory cap)
KLEE: WARNING: killing 13241 states (over memory cap)
KLEE: WARNING: killing 13230 states (over memory cap)
KLEE: WARNING: killing 14197 states (over memory cap)
KLEE: WARNING: killing 14180 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 13942 states (over memory cap)
KLEE: WARNING: killing 13823 states (over memory cap)
KLEE: WARNING: killing 13805 states (over memory cap)
KLEE: WARNING: killing 14655 states (over memory cap)
KLEE: WARNING: killing 14105 states (over memory cap)
KLEE: WARNING: killing 13450 states (over memory cap)
KLEE: WARNING: killing 13651 states (over memory cap)
KLEE: WARNING: killing 13535 states (over memory cap)
KLEE: WARNING: killing 13739 states (over memory cap)
KLEE: WARNING: killing 13944 states (over memory cap)
KLEE: WARNING: killing 12962 states (over memory cap)
KLEE: WARNING: killing 13058 states (over memory cap)
KLEE: WARNING: killing 13686 states (over memory cap)
KLEE: WARNING: killing 13357 states (over memory cap)
KLEE: WARNING: killing 13554 states (over memory cap)
KLEE: WARNING: killing 13759 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13306 states (over memory cap)
KLEE: WARNING: killing 13192 states (over memory cap)
KLEE: WARNING: killing 13821 states (over memory cap)
KLEE: WARNING: killing 13806 states (over memory cap)
KLEE: WARNING: killing 13800 states (over memory cap)
KLEE: WARNING: killing 13889 states (over memory cap)
KLEE: WARNING: killing 13881 states (over memory cap)
KLEE: WARNING: killing 13761 states (over memory cap)
KLEE: WARNING: killing 13328 states (over memory cap)
KLEE: WARNING: killing 14053 states (over memory cap)
KLEE: WARNING: killing 13727 states (over memory cap)
KLEE: WARNING: killing 14134 states (over memory cap)
KLEE: WARNING: killing 13801 states (over memory cap)
KLEE: WARNING: killing 14101 states (over memory cap)
KLEE: WARNING: killing 13778 states (over memory cap)
KLEE: WARNING: killing 14080 states (over memory cap)
KLEE: WARNING: killing 14065 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 13833 states (over memory cap)
KLEE: WARNING: killing 13919 states (over memory cap)
KLEE: WARNING: killing 14332 states (over memory cap)
KLEE: WARNING: killing 13594 states (over memory cap)
KLEE: WARNING: killing 13150 states (over memory cap)
KLEE: WARNING: killing 13758 states (over memory cap)
KLEE: WARNING: killing 13236 states (over memory cap)
KLEE: WARNING: killing 13326 states (over memory cap)
KLEE: WARNING: killing 13217 states (over memory cap)
KLEE: WARNING: killing 13726 states (over memory cap)
KLEE: WARNING: killing 13194 states (over memory cap)
KLEE: WARNING: killing 13800 states (over memory cap)
KLEE: WARNING: killing 13694 states (over memory cap)
KLEE: WARNING: killing 13161 states (over memory cap)
KLEE: WARNING: killing 13051 states (over memory cap)
KLEE: WARNING: killing 14275 states (over memory cap)
KLEE: WARNING: killing 14063 states (over memory cap)
KLEE: WARNING: killing 13740 states (over memory cap)
KLEE: WARNING: killing 13622 states (over memory cap)
KLEE: WARNING: killing 14023 states (over memory cap)
KLEE: WARNING: killing 13918 states (over memory cap)
KLEE: WARNING: killing 14004 states (over memory cap)
KLEE: WARNING: killing 13379 states (over memory cap)
KLEE: WARNING: killing 13669 states (over memory cap)
KLEE: WARNING: killing 13554 states (over memory cap)
KLEE: WARNING: killing 13745 states (over memory cap)
KLEE: WARNING: killing 13734 states (over memory cap)
KLEE: WARNING: killing 14132 states (over memory cap)
KLEE: WARNING: killing 13711 states (over memory cap)
KLEE: WARNING: killing 14112 states (over memory cap)
KLEE: WARNING: killing 13999 states (over memory cap)
KLEE: WARNING: killing 13677 states (over memory cap)
KLEE: WARNING: killing 13154 states (over memory cap)
KLEE: WARNING: killing 14063 states (over memory cap)
KLEE: WARNING: killing 13637 states (over memory cap)
KLEE: WARNING: killing 13729 states (over memory cap)
KLEE: WARNING: killing 13813 states (over memory cap)
KLEE: WARNING: killing 13396 states (over memory cap)
KLEE: WARNING: killing 13789 states (over memory cap)
KLEE: WARNING: killing 13784 states (over memory cap)
KLEE: WARNING: killing 13363 states (over memory cap)
KLEE: WARNING: killing 13553 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13528 states (over memory cap)
KLEE: WARNING: killing 14027 states (over memory cap)
KLEE: WARNING: killing 13308 states (over memory cap)
KLEE: WARNING: killing 13901 states (over memory cap)
KLEE: WARNING: killing 13888 states (over memory cap)
KLEE: WARNING: killing 13882 states (over memory cap)
KLEE: WARNING: killing 14068 states (over memory cap)
KLEE: WARNING: killing 13157 states (over memory cap)
KLEE: WARNING: killing 13642 states (over memory cap)
KLEE: WARNING: killing 13336 states (over memory cap)
KLEE: WARNING: killing 13530 states (over memory cap)
KLEE: WARNING: killing 13306 states (over memory cap)
KLEE: WARNING: killing 14006 states (over memory cap)
KLEE: WARNING: killing 14096 states (over memory cap)
KLEE: WARNING: killing 13885 states (over memory cap)
KLEE: WARNING: killing 13667 states (over memory cap)
KLEE: WARNING: killing 13958 states (over memory cap)
KLEE: WARNING: killing 13938 states (over memory cap)
KLEE: WARNING: killing 13433 states (over memory cap)
KLEE: WARNING: killing 13420 states (over memory cap)
KLEE: WARNING: killing 13515 states (over memory cap)
KLEE: WARNING: killing 13802 states (over memory cap)
