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-spinlock__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.: 786 620 5534 33922
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.09423208237
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 '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function atomic_dec_and_mutex_lock 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: 1.04421305656
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 860 586 2599 20447
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_862821b3-fff2-46a5-975b-7030aff330b9/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 17442 states (over memory cap)
KLEE: WARNING: killing 14467 states (over memory cap)
KLEE: WARNING: killing 13416 states (over memory cap)
KLEE: WARNING: killing 12749 states (over memory cap)
KLEE: WARNING: killing 12713 states (over memory cap)
KLEE: WARNING: killing 24255 states (over memory cap)
KLEE: WARNING: killing 13143 states (over memory cap)
KLEE: WARNING: killing 24145 states (over memory cap)
KLEE: WARNING: killing 12598 states (over memory cap)
KLEE: WARNING: killing 24330 states (over memory cap)
KLEE: WARNING: killing 12803 states (over memory cap)
KLEE: WARNING: killing 12788 states (over memory cap)
KLEE: WARNING: killing 12521 states (over memory cap)
KLEE: WARNING: killing 12633 states (over memory cap)
KLEE: WARNING: killing 12993 states (over memory cap)
KLEE: WARNING: killing 12474 states (over memory cap)
KLEE: WARNING: killing 12700 states (over memory cap)
KLEE: WARNING: killing 13052 states (over memory cap)
KLEE: WARNING: killing 13652 states (over memory cap)
KLEE: WARNING: killing 14253 states (over memory cap)
KLEE: WARNING: killing 13618 states (over memory cap)
KLEE: WARNING: killing 13966 states (over memory cap)
KLEE: WARNING: killing 14558 states (over memory cap)
KLEE: WARNING: killing 14409 states (over memory cap)
KLEE: WARNING: killing 14142 states (over memory cap)
KLEE: WARNING: killing 14975 states (over memory cap)
KLEE: WARNING: killing 14459 states (over memory cap)
KLEE: WARNING: killing 14682 states (over memory cap)
KLEE: WARNING: killing 14419 states (over memory cap)
KLEE: WARNING: killing 14881 states (over memory cap)
KLEE: WARNING: killing 14131 states (over memory cap)
KLEE: WARNING: killing 14591 states (over memory cap)
KLEE: WARNING: killing 14939 states (over memory cap)
KLEE: WARNING: killing 14443 states (over memory cap)
KLEE: WARNING: killing 14062 states (over memory cap)
KLEE: WARNING: killing 14163 states (over memory cap)
KLEE: WARNING: killing 14626 states (over memory cap)
KLEE: WARNING: killing 14367 states (over memory cap)
KLEE: WARNING: killing 13864 states (over memory cap)
KLEE: WARNING: killing 14084 states (over memory cap)
KLEE: WARNING: killing 13945 states (over memory cap)
KLEE: WARNING: killing 13569 states (over memory cap)
KLEE: WARNING: killing 14152 states (over memory cap)
KLEE: WARNING: killing 13300 states (over memory cap)
KLEE: WARNING: killing 14002 states (over memory cap)
KLEE: WARNING: killing 13987 states (over memory cap)
KLEE: WARNING: killing 13373 states (over memory cap)
KLEE: WARNING: killing 13114 states (over memory cap)
KLEE: WARNING: killing 13697 states (over memory cap)
KLEE: WARNING: killing 13673 states (over memory cap)
KLEE: WARNING: killing 13663 states (over memory cap)
KLEE: WARNING: killing 13534 states (over memory cap)
KLEE: WARNING: killing 13876 states (over memory cap)
KLEE: WARNING: killing 13864 states (over memory cap)
KLEE: WARNING: killing 13969 states (over memory cap)
KLEE: WARNING: killing 13830 states (over memory cap)
KLEE: WARNING: killing 13700 states (over memory cap)
KLEE: WARNING: killing 13802 states (over memory cap)
KLEE: WARNING: killing 13779 states (over memory cap)
KLEE: WARNING: killing 13648 states (over memory cap)
KLEE: WARNING: killing 13512 states (over memory cap)
KLEE: WARNING: killing 13381 states (over memory cap)
KLEE: WARNING: killing 13597 states (over memory cap)
KLEE: WARNING: killing 13818 states (over memory cap)
KLEE: WARNING: killing 13796 states (over memory cap)
KLEE: WARNING: killing 13666 states (over memory cap)
KLEE: WARNING: killing 14005 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13971 states (over memory cap)
KLEE: WARNING: killing 13252 states (over memory cap)
KLEE: WARNING: killing 13942 states (over memory cap)
KLEE: WARNING: killing 13808 states (over memory cap)
KLEE: WARNING: killing 14031 states (over memory cap)
KLEE: WARNING: killing 13783 states (over memory cap)
KLEE: WARNING: killing 13647 states (over memory cap)
KLEE: WARNING: killing 13402 states (over memory cap)
KLEE: WARNING: killing 13730 states (over memory cap)
KLEE: WARNING: killing 13951 states (over memory cap)
KLEE: WARNING: killing 13246 states (over memory cap)
KLEE: WARNING: killing 13809 states (over memory cap)
KLEE: WARNING: killing 13791 states (over memory cap)
KLEE: WARNING: killing 13543 states (over memory cap)
KLEE: WARNING: killing 13643 states (over memory cap)
KLEE: WARNING: killing 13751 states (over memory cap)
KLEE: WARNING: killing 13863 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 13488 states (over memory cap)
KLEE: WARNING: killing 13927 states (over memory cap)
KLEE: WARNING: killing 13682 states (over memory cap)
KLEE: WARNING: killing 13895 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13411 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 14069 states (over memory cap)
KLEE: WARNING: killing 13938 states (over memory cap)
KLEE: WARNING: killing 13695 states (over memory cap)
KLEE: WARNING: killing 13563 states (over memory cap)
KLEE: WARNING: killing 13996 states (over memory cap)
KLEE: WARNING: killing 13534 states (over memory cap)
KLEE: WARNING: killing 13854 states (over memory cap)
KLEE: WARNING: killing 13728 states (over memory cap)
KLEE: WARNING: killing 13377 states (over memory cap)
KLEE: WARNING: killing 13367 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
KLEE: WARNING: killing 13904 states (over memory cap)
KLEE: WARNING: killing 14458 states (over memory cap)
KLEE: WARNING: killing 13770 states (over memory cap)
KLEE: WARNING: killing 13982 states (over memory cap)
KLEE: WARNING: killing 13294 states (over memory cap)
KLEE: WARNING: killing 13280 states (over memory cap)
KLEE: WARNING: killing 13933 states (over memory cap)
KLEE: WARNING: killing 14031 states (over memory cap)
KLEE: WARNING: killing 14130 states (over memory cap)
KLEE: WARNING: killing 13227 states (over memory cap)
KLEE: WARNING: killing 13769 states (over memory cap)
KLEE: WARNING: killing 13863 states (over memory cap)
KLEE: WARNING: killing 13298 states (over memory cap)
KLEE: WARNING: killing 13847 states (over memory cap)
KLEE: WARNING: killing 13830 states (over memory cap)
KLEE: WARNING: killing 13597 states (over memory cap)
KLEE: WARNING: killing 13250 states (over memory cap)
KLEE: WARNING: killing 13904 states (over memory cap)
KLEE: WARNING: killing 13777 states (over memory cap)
KLEE: WARNING: killing 14212 states (over memory cap)
KLEE: WARNING: killing 13642 states (over memory cap)
KLEE: WARNING: killing 13623 states (over memory cap)
KLEE: WARNING: killing 14163 states (over memory cap)
KLEE: WARNING: killing 13706 states (over memory cap)
KLEE: WARNING: killing 13584 states (over memory cap)
KLEE: WARNING: killing 13464 states (over memory cap)
KLEE: WARNING: killing 14102 states (over memory cap)
KLEE: WARNING: killing 13765 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13958 states (over memory cap)
KLEE: WARNING: killing 13616 states (over memory cap)
KLEE: WARNING: killing 14158 states (over memory cap)
KLEE: WARNING: killing 13600 states (over memory cap)
KLEE: WARNING: killing 13800 states (over memory cap)
KLEE: WARNING: killing 13681 states (over memory cap)
KLEE: WARNING: killing 13669 states (over memory cap)
KLEE: WARNING: killing 13759 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 13521 states (over memory cap)
KLEE: WARNING: killing 13391 states (over memory cap)
KLEE: WARNING: killing 13171 states (over memory cap)
KLEE: WARNING: killing 14026 states (over memory cap)
KLEE: WARNING: killing 13801 states (over memory cap)
KLEE: WARNING: killing 13897 states (over memory cap)
KLEE: WARNING: killing 13660 states (over memory cap)
KLEE: WARNING: killing 13647 states (over memory cap)
KLEE: WARNING: killing 13640 states (over memory cap)
KLEE: WARNING: killing 13733 states (over memory cap)
KLEE: WARNING: killing 13401 states (over memory cap)
KLEE: WARNING: killing 13707 states (over memory cap)
KLEE: WARNING: killing 13917 states (over memory cap)
KLEE: WARNING: killing 13898 states (over memory cap)
KLEE: WARNING: killing 13250 states (over memory cap)
KLEE: WARNING: killing 13666 states (over memory cap)
KLEE: WARNING: killing 13339 states (over memory cap)
KLEE: WARNING: killing 13637 states (over memory cap)
KLEE: WARNING: killing 13734 states (over memory cap)
KLEE: WARNING: killing 13505 states (over memory cap)
KLEE: WARNING: killing 13281 states (over memory cap)
KLEE: WARNING: killing 13270 states (over memory cap)
KLEE: WARNING: killing 13790 states (over memory cap)
KLEE: WARNING: killing 13463 states (over memory cap)
KLEE: WARNING: killing 14195 states (over memory cap)
KLEE: WARNING: killing 14188 states (over memory cap)
KLEE: WARNING: killing 13644 states (over memory cap)
KLEE: WARNING: killing 13629 states (over memory cap)
KLEE: WARNING: killing 13191 states (over memory cap)
KLEE: WARNING: killing 13812 states (over memory cap)
KLEE: WARNING: killing 13802 states (over memory cap)
KLEE: WARNING: killing 13472 states (over memory cap)
KLEE: WARNING: killing 13032 states (over memory cap)
KLEE: WARNING: killing 13974 states (over memory cap)
KLEE: WARNING: killing 13857 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 13407 states (over memory cap)
KLEE: WARNING: killing 13822 states (over memory cap)
KLEE: WARNING: killing 13818 states (over memory cap)
KLEE: WARNING: killing 13697 states (over memory cap)
KLEE: WARNING: killing 13682 states (over memory cap)
KLEE: WARNING: killing 13362 states (over memory cap)
KLEE: WARNING: killing 14088 states (over memory cap)
KLEE: WARNING: killing 14184 states (over memory cap)
KLEE: WARNING: killing 13956 states (over memory cap)
KLEE: WARNING: killing 14475 states (over memory cap)
KLEE: WARNING: killing 14140 states (over memory cap)
KLEE: WARNING: killing 13717 states (over memory cap)
KLEE: WARNING: killing 13595 states (over memory cap)
KLEE: WARNING: killing 14110 states (over memory cap)
KLEE: WARNING: killing 13577 states (over memory cap)
KLEE: WARNING: killing 13251 states (over memory cap)
KLEE: WARNING: killing 13231 states (over memory cap)
KLEE: WARNING: killing 14148 states (over memory cap)
KLEE: WARNING: killing 13938 states (over memory cap)
KLEE: WARNING: killing 13714 states (over memory cap)
KLEE: WARNING: killing 13182 states (over memory cap)
KLEE: WARNING: killing 13790 states (over memory cap)
KLEE: WARNING: killing 13472 states (over memory cap)
KLEE: WARNING: killing 13353 states (over memory cap)
KLEE: WARNING: killing 13962 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13629 states (over memory cap)
KLEE: WARNING: killing 13929 states (over memory cap)
KLEE: WARNING: killing 13921 states (over memory cap)
KLEE: WARNING: killing 13293 states (over memory cap)
KLEE: WARNING: killing 13179 states (over memory cap)
KLEE: WARNING: killing 14096 states (over memory cap)
KLEE: WARNING: killing 13883 states (over memory cap)
KLEE: WARNING: killing 13981 states (over memory cap)
KLEE: WARNING: killing 13657 states (over memory cap)
