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-usb-dev__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 557 5368 33167
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.33186602592
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_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: 1.26710510254
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 855 536 2433 19749
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_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_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: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_1bf66a74-de92-4957-8f94-e369753d53c2/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 21334 states (over memory cap)
KLEE: WARNING: killing 13126 states (over memory cap)
KLEE: WARNING: killing 25210 states (over memory cap)
KLEE: WARNING: killing 13176 states (over memory cap)
KLEE: WARNING: killing 23710 states (over memory cap)
KLEE: WARNING: killing 12742 states (over memory cap)
KLEE: WARNING: killing 22986 states (over memory cap)
KLEE: WARNING: killing 23295 states (over memory cap)
KLEE: WARNING: killing 12656 states (over memory cap)
KLEE: WARNING: killing 24328 states (over memory cap)
KLEE: WARNING: killing 13476 states (over memory cap)
KLEE: WARNING: killing 13093 states (over memory cap)
KLEE: WARNING: killing 13319 states (over memory cap)
KLEE: WARNING: killing 13299 states (over memory cap)
KLEE: WARNING: killing 13398 states (over memory cap)
KLEE: WARNING: killing 13747 states (over memory cap)
KLEE: WARNING: killing 13602 states (over memory cap)
KLEE: WARNING: killing 14687 states (over memory cap)
KLEE: WARNING: killing 14052 states (over memory cap)
KLEE: WARNING: killing 14155 states (over memory cap)
KLEE: WARNING: killing 14741 states (over memory cap)
KLEE: WARNING: killing 14479 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: WARNING: killing 15032 states (over memory cap)
KLEE: WARNING: killing 14649 states (over memory cap)
KLEE: WARNING: killing 14866 states (over memory cap)
KLEE: WARNING: killing 15210 states (over memory cap)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 14907 states (over memory cap)
KLEE: WARNING: killing 14773 states (over memory cap)
KLEE: WARNING: killing 14880 states (over memory cap)
KLEE: WARNING: killing 14745 states (over memory cap)
KLEE: WARNING: killing 15208 states (over memory cap)
KLEE: WARNING: killing 14710 states (over memory cap)
KLEE: WARNING: killing 14095 states (over memory cap)
KLEE: WARNING: killing 13472 states (over memory cap)
KLEE: WARNING: killing 13687 states (over memory cap)
KLEE: WARNING: killing 14149 states (over memory cap)
KLEE: WARNING: killing 14133 states (over memory cap)
KLEE: WARNING: killing 13755 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 13376 states (over memory cap)
KLEE: WARNING: killing 13235 states (over memory cap)
KLEE: WARNING: killing 13808 states (over memory cap)
KLEE: WARNING: killing 13677 states (over memory cap)
KLEE: WARNING: killing 13539 states (over memory cap)
KLEE: WARNING: killing 13056 states (over memory cap)
KLEE: WARNING: killing 13862 states (over memory cap)
KLEE: WARNING: killing 13620 states (over memory cap)
KLEE: WARNING: killing 13485 states (over memory cap)
KLEE: WARNING: killing 13469 states (over memory cap)
KLEE: WARNING: killing 14044 states (over memory cap)
KLEE: WARNING: killing 13323 states (over memory cap)
KLEE: WARNING: killing 13771 states (over memory cap)
KLEE: WARNING: killing 13288 states (over memory cap)
KLEE: WARNING: killing 13625 states (over memory cap)
KLEE: WARNING: killing 13379 states (over memory cap)
KLEE: WARNING: killing 13708 states (over memory cap)
KLEE: WARNING: killing 13930 states (over memory cap)
KLEE: WARNING: killing 14145 states (over memory cap)
KLEE: WARNING: killing 13549 states (over memory cap)
KLEE: WARNING: killing 13651 states (over memory cap)
KLEE: WARNING: killing 13753 states (over memory cap)
KLEE: WARNING: killing 13852 states (over memory cap)
KLEE: WARNING: killing 14067 states (over memory cap)
KLEE: WARNING: killing 13824 states (over memory cap)
KLEE: WARNING: killing 14045 states (over memory cap)
KLEE: WARNING: killing 13341 states (over memory cap)
KLEE: WARNING: killing 14012 states (over memory cap)
KLEE: WARNING: killing 14340 states (over memory cap)
KLEE: WARNING: killing 13747 states (over memory cap)
KLEE: WARNING: killing 13730 states (over memory cap)
KLEE: WARNING: killing 14180 states (over memory cap)
KLEE: WARNING: killing 13591 states (over memory cap)
KLEE: WARNING: killing 13569 states (over memory cap)
KLEE: WARNING: killing 13554 states (over memory cap)
KLEE: WARNING: killing 13202 states (over memory cap)
KLEE: WARNING: killing 13870 states (over memory cap)
KLEE: WARNING: killing 14200 states (over memory cap)
KLEE: WARNING: killing 14072 states (over memory cap)
KLEE: WARNING: killing 14285 states (over memory cap)
KLEE: WARNING: killing 13359 states (over memory cap)
KLEE: WARNING: killing 13341 states (over memory cap)
KLEE: WARNING: killing 13667 states (over memory cap)
KLEE: WARNING: killing 13759 states (over memory cap)
KLEE: WARNING: killing 13741 states (over memory cap)
KLEE: WARNING: killing 13842 states (over memory cap)
KLEE: WARNING: killing 12931 states (over memory cap)
KLEE: WARNING: killing 13471 states (over memory cap)
KLEE: WARNING: killing 13911 states (over memory cap)
KLEE: WARNING: killing 14354 states (over memory cap)
KLEE: WARNING: killing 14346 states (over memory cap)
KLEE: WARNING: killing 13772 states (over memory cap)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 13632 states (over memory cap)
KLEE: WARNING: killing 13608 states (over memory cap)
KLEE: WARNING: killing 14386 states (over memory cap)
KLEE: WARNING: killing 13594 states (over memory cap)
KLEE: WARNING: killing 13690 states (over memory cap)
KLEE: WARNING: killing 13894 states (over memory cap)
KLEE: WARNING: killing 13767 states (over memory cap)
KLEE: WARNING: killing 13642 states (over memory cap)
KLEE: WARNING: killing 13632 states (over memory cap)
KLEE: WARNING: killing 13504 states (over memory cap)
KLEE: WARNING: killing 13379 states (over memory cap)
KLEE: WARNING: killing 13591 states (over memory cap)
KLEE: WARNING: killing 13246 states (over memory cap)
KLEE: WARNING: killing 13562 states (over memory cap)
KLEE: WARNING: killing 13439 states (over memory cap)
KLEE: WARNING: killing 13870 states (over memory cap)
KLEE: WARNING: killing 13198 states (over memory cap)
KLEE: WARNING: killing 13618 states (over memory cap)
KLEE: WARNING: killing 13936 states (over memory cap)
KLEE: WARNING: killing 13488 states (over memory cap)
KLEE: WARNING: killing 14583 states (over memory cap)
KLEE: WARNING: killing 13684 states (over memory cap)
KLEE: WARNING: killing 14000 states (over memory cap)
KLEE: WARNING: killing 13981 states (over memory cap)
KLEE: WARNING: killing 13751 states (over memory cap)
KLEE: WARNING: killing 13731 states (over memory cap)
KLEE: WARNING: killing 13506 states (over memory cap)
KLEE: WARNING: killing 13387 states (over memory cap)
KLEE: WARNING: killing 14250 states (over memory cap)
KLEE: WARNING: killing 14128 states (over memory cap)
KLEE: WARNING: killing 14001 states (over memory cap)
KLEE: WARNING: killing 13226 states (over memory cap)
KLEE: WARNING: killing 13430 states (over memory cap)
KLEE: WARNING: killing 13529 states (over memory cap)
KLEE: WARNING: killing 14059 states (over memory cap)
KLEE: WARNING: killing 14158 states (over memory cap)
KLEE: WARNING: killing 13923 states (over memory cap)
KLEE: WARNING: killing 13474 states (over memory cap)
KLEE: WARNING: killing 13682 states (over memory cap)
KLEE: WARNING: killing 14320 states (over memory cap)
KLEE: WARNING: killing 12896 states (over memory cap)
KLEE: WARNING: killing 13418 states (over memory cap)
KLEE: WARNING: killing 13302 states (over memory cap)
KLEE: WARNING: killing 13607 states (over memory cap)
KLEE: WARNING: killing 13924 states (over memory cap)
KLEE: WARNING: killing 13698 states (over memory cap)
KLEE: WARNING: killing 13687 states (over memory cap)
KLEE: WARNING: killing 13245 states (over memory cap)
KLEE: WARNING: killing 13552 states (over memory cap)
KLEE: WARNING: killing 13862 states (over memory cap)
KLEE: WARNING: killing 14176 states (over memory cap)
KLEE: WARNING: killing 13741 states (over memory cap)
KLEE: WARNING: killing 13400 states (over memory cap)
KLEE: WARNING: killing 13391 states (over memory cap)
KLEE: WARNING: killing 14123 states (over memory cap)
KLEE: WARNING: killing 13791 states (over memory cap)
KLEE: WARNING: killing 13678 states (over memory cap)
KLEE: WARNING: killing 13657 states (over memory cap)
KLEE: WARNING: killing 13971 states (over memory cap)
KLEE: WARNING: killing 14061 states (over memory cap)
KLEE: WARNING: killing 13844 states (over memory cap)
KLEE: WARNING: killing 13507 states (over memory cap)
KLEE: WARNING: killing 13693 states (over memory cap)
KLEE: WARNING: killing 13155 states (over memory cap)
KLEE: WARNING: killing 13774 states (over memory cap)
KLEE: WARNING: killing 13137 states (over memory cap)
KLEE: WARNING: killing 13653 states (over memory cap)
KLEE: WARNING: killing 13317 states (over memory cap)
KLEE: WARNING: killing 13731 states (over memory cap)
KLEE: WARNING: killing 14354 states (over memory cap)
KLEE: WARNING: killing 14026 states (over memory cap)
KLEE: WARNING: killing 14021 states (over memory cap)
KLEE: WARNING: killing 14422 states (over memory cap)
KLEE: WARNING: killing 14417 states (over memory cap)
KLEE: WARNING: killing 13878 states (over memory cap)
KLEE: WARNING: killing 13968 states (over memory cap)
KLEE: WARNING: killing 13639 states (over memory cap)
KLEE: WARNING: killing 13722 states (over memory cap)
KLEE: WARNING: killing 13190 states (over memory cap)
KLEE: WARNING: killing 13798 states (over memory cap)
KLEE: WARNING: killing 13264 states (over memory cap)
KLEE: WARNING: killing 13778 states (over memory cap)
KLEE: WARNING: killing 13657 states (over memory cap)
KLEE: WARNING: killing 13962 states (over memory cap)
KLEE: WARNING: killing 13646 states (over memory cap)
KLEE: WARNING: killing 13319 states (over memory cap)
KLEE: WARNING: killing 14245 states (over memory cap)
KLEE: WARNING: killing 13828 states (over memory cap)
KLEE: WARNING: killing 12771 states (over memory cap)
KLEE: WARNING: killing 13069 states (over memory cap)
KLEE: WARNING: killing 13475 states (over memory cap)
KLEE: WARNING: killing 13774 states (over memory cap)
KLEE: WARNING: killing 13350 states (over memory cap)
KLEE: WARNING: killing 13538 states (over memory cap)
KLEE: WARNING: killing 13424 states (over memory cap)
KLEE: WARNING: killing 14142 states (over memory cap)
KLEE: WARNING: killing 13921 states (over memory cap)
KLEE: WARNING: killing 13705 states (over memory cap)
KLEE: WARNING: killing 13179 states (over memory cap)
KLEE: WARNING: killing 13469 states (over memory cap)
KLEE: WARNING: killing 13769 states (over memory cap)
KLEE: WARNING: killing 12932 states (over memory cap)
KLEE: WARNING: killing 13431 states (over memory cap)
KLEE: WARNING: killing 13727 states (over memory cap)
KLEE: WARNING: killing 13724 states (over memory cap)
KLEE: WARNING: killing 14025 states (over memory cap)
KLEE: WARNING: killing 13599 states (over memory cap)
KLEE: WARNING: killing 13989 states (over memory cap)
KLEE: WARNING: killing 13979 states (over memory cap)
KLEE: WARNING: killing 13869 states (over memory cap)
KLEE: WARNING: killing 13649 states (over memory cap)
KLEE: WARNING: killing 14147 states (over memory cap)
KLEE: WARNING: killing 13525 states (over memory cap)
KLEE: WARNING: killing 13814 states (over memory cap)
KLEE: WARNING: killing 13392 states (over memory cap)
KLEE: WARNING: killing 13487 states (over memory cap)
KLEE: WARNING: killing 13782 states (over memory cap)
KLEE: WARNING: killing 14375 states (over memory cap)
KLEE: WARNING: killing 14367 states (over memory cap)
KLEE: WARNING: killing 13648 states (over memory cap)
KLEE: WARNING: killing 14240 states (over memory cap)
KLEE: WARNING: killing 13826 states (over memory cap)
KLEE: WARNING: killing 14113 states (over memory cap)
KLEE: WARNING: killing 13401 states (over memory cap)
KLEE: WARNING: killing 13486 states (over memory cap)
KLEE: WARNING: killing 13375 states (over memory cap)
KLEE: WARNING: killing 13662 states (over memory cap)
KLEE: WARNING: killing 13544 states (over memory cap)
KLEE: WARNING: killing 13735 states (over memory cap)
KLEE: WARNING: killing 13930 states (over memory cap)
KLEE: WARNING: killing 13309 states (over memory cap)
KLEE: WARNING: killing 13601 states (over memory cap)
KLEE: WARNING: killing 13185 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
