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-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.: 783 648 5502 33977
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.35686302185
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 '_raw_spin_unlock_irqrestore' (function is undefined)
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)
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.20714688301
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 859 552 2656 20427
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_7d250f76-564b-4c22-b902-8e3ca11c4b32/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 23265 states (over memory cap)
KLEE: WARNING: killing 12947 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 24172 states (over memory cap)
KLEE: WARNING: killing 12720 states (over memory cap)
KLEE: WARNING: killing 23698 states (over memory cap)
KLEE: WARNING: killing 24151 states (over memory cap)
KLEE: WARNING: killing 13014 states (over memory cap)
KLEE: WARNING: killing 24314 states (over memory cap)
KLEE: WARNING: killing 12968 states (over memory cap)
KLEE: WARNING: killing 24199 states (over memory cap)
KLEE: WARNING: killing 13270 states (over memory cap)
KLEE: WARNING: killing 13005 states (over memory cap)
KLEE: WARNING: killing 13476 states (over memory cap)
KLEE: WARNING: killing 12969 states (over memory cap)
KLEE: WARNING: killing 13921 states (over memory cap)
KLEE: WARNING: killing 13779 states (over memory cap)
KLEE: WARNING: killing 13881 states (over memory cap)
KLEE: WARNING: killing 14220 states (over memory cap)
KLEE: WARNING: killing 14688 states (over memory cap)
KLEE: WARNING: killing 14546 states (over memory cap)
KLEE: WARNING: killing 14528 states (over memory cap)
KLEE: WARNING: killing 14509 states (over memory cap)
KLEE: WARNING: killing 14122 states (over memory cap)
KLEE: WARNING: killing 14217 states (over memory cap)
KLEE: WARNING: killing 14317 states (over memory cap)
KLEE: WARNING: killing 15023 states (over memory cap)
KLEE: WARNING: killing 14286 states (over memory cap)
KLEE: WARNING: killing 14858 states (over memory cap)
KLEE: WARNING: killing 14715 states (over memory cap)
KLEE: WARNING: killing 14573 states (over memory cap)
KLEE: WARNING: killing 14077 states (over memory cap)
KLEE: WARNING: killing 14410 states (over memory cap)
KLEE: WARNING: killing 14158 states (over memory cap)
KLEE: WARNING: killing 14256 states (over memory cap)
KLEE: WARNING: killing 14123 states (over memory cap)
KLEE: WARNING: killing 14112 states (over memory cap)
KLEE: WARNING: killing 14094 states (over memory cap)
KLEE: WARNING: killing 13363 states (over memory cap)
KLEE: WARNING: killing 13700 states (over memory cap)
KLEE: WARNING: killing 13213 states (over memory cap)
KLEE: WARNING: killing 14028 states (over memory cap)
KLEE: WARNING: killing 13074 states (over memory cap)
KLEE: WARNING: killing 13519 states (over memory cap)
KLEE: WARNING: killing 13743 states (over memory cap)
KLEE: WARNING: killing 13609 states (over memory cap)
KLEE: WARNING: killing 13598 states (over memory cap)
KLEE: WARNING: killing 13811 states (over memory cap)
KLEE: WARNING: killing 13088 states (over memory cap)
KLEE: WARNING: killing 13543 states (over memory cap)
KLEE: WARNING: killing 13527 states (over memory cap)
KLEE: WARNING: killing 13979 states (over memory cap)
KLEE: WARNING: killing 13844 states (over memory cap)
KLEE: WARNING: killing 13829 states (over memory cap)
KLEE: WARNING: killing 14048 states (over memory cap)
KLEE: WARNING: killing 14152 states (over memory cap)
KLEE: WARNING: killing 14015 states (over memory cap)
KLEE: WARNING: killing 13541 states (over memory cap)
KLEE: WARNING: killing 13980 states (over memory cap)
KLEE: WARNING: killing 13390 states (over memory cap)
KLEE: WARNING: killing 14410 states (over memory cap)
KLEE: WARNING: killing 14165 states (over memory cap)
KLEE: WARNING: killing 14151 states (over memory cap)
KLEE: WARNING: killing 13564 states (over memory cap)
KLEE: WARNING: killing 13429 states (over memory cap)
KLEE: WARNING: killing 13535 states (over memory cap)
KLEE: WARNING: killing 13632 states (over memory cap)
KLEE: WARNING: killing 13618 states (over memory cap)
KLEE: WARNING: killing 14401 states (over memory cap)
KLEE: WARNING: killing 13358 states (over memory cap)
KLEE: WARNING: killing 13007 states (over memory cap)
KLEE: WARNING: killing 13441 states (over memory cap)
KLEE: WARNING: killing 14116 states (over memory cap)
KLEE: WARNING: killing 13873 states (over memory cap)
KLEE: WARNING: killing 13516 states (over memory cap)
KLEE: WARNING: killing 13387 states (over memory cap)
KLEE: WARNING: killing 14286 states (over memory cap)
KLEE: WARNING: killing 13819 states (over memory cap)
KLEE: WARNING: killing 14033 states (over memory cap)
KLEE: WARNING: killing 13789 states (over memory cap)
KLEE: WARNING: killing 13314 states (over memory cap)
KLEE: WARNING: killing 13864 states (over memory cap)
KLEE: WARNING: killing 13400 states (over memory cap)
KLEE: WARNING: killing 14293 states (over memory cap)
KLEE: WARNING: killing 14391 states (over memory cap)
KLEE: WARNING: killing 13475 states (over memory cap)
KLEE: WARNING: killing 14023 states (over memory cap)
KLEE: WARNING: killing 13564 states (over memory cap)
KLEE: WARNING: killing 13440 states (over memory cap)
KLEE: WARNING: killing 13085 states (over memory cap)
KLEE: WARNING: killing 13739 states (over memory cap)
KLEE: WARNING: killing 13839 states (over memory cap)
KLEE: WARNING: killing 13048 states (over memory cap)
KLEE: WARNING: killing 14484 states (over memory cap)
KLEE: WARNING: killing 13578 states (over memory cap)
KLEE: WARNING: killing 13345 states (over memory cap)
KLEE: WARNING: killing 13443 states (over memory cap)
KLEE: WARNING: killing 13651 states (over memory cap)
KLEE: WARNING: killing 13642 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: WARNING: killing 14171 states (over memory cap)
KLEE: WARNING: killing 13270 states (over memory cap)
KLEE: WARNING: killing 13697 states (over memory cap)
KLEE: WARNING: killing 13683 states (over memory cap)
KLEE: WARNING: killing 13329 states (over memory cap)
KLEE: WARNING: killing 13644 states (over memory cap)
KLEE: WARNING: killing 13849 states (over memory cap)
KLEE: WARNING: killing 13848 states (over memory cap)
KLEE: WARNING: killing 14381 states (over memory cap)
KLEE: WARNING: killing 14038 states (over memory cap)
KLEE: WARNING: killing 14018 states (over memory cap)
KLEE: WARNING: killing 13774 states (over memory cap)
KLEE: WARNING: killing 13648 states (over memory cap)
KLEE: WARNING: killing 13417 states (over memory cap)
KLEE: WARNING: killing 13732 states (over memory cap)
KLEE: WARNING: killing 13616 states (over memory cap)
KLEE: WARNING: killing 13717 states (over memory cap)
KLEE: WARNING: killing 13807 states (over memory cap)
KLEE: WARNING: killing 13585 states (over memory cap)
KLEE: WARNING: killing 14112 states (over memory cap)
KLEE: WARNING: killing 14212 states (over memory cap)
KLEE: WARNING: killing 13221 states (over memory cap)
KLEE: WARNING: killing 14296 states (over memory cap)
KLEE: WARNING: killing 13420 states (over memory cap)
KLEE: WARNING: killing 13835 states (over memory cap)
KLEE: WARNING: killing 13715 states (over memory cap)
KLEE: WARNING: killing 13914 states (over memory cap)
KLEE: WARNING: killing 12819 states (over memory cap)
KLEE: WARNING: killing 13672 states (over memory cap)
KLEE: WARNING: killing 13227 states (over memory cap)
KLEE: WARNING: killing 14296 states (over memory cap)
KLEE: WARNING: killing 13748 states (over memory cap)
KLEE: WARNING: killing 13518 states (over memory cap)
KLEE: WARNING: killing 14042 states (over memory cap)
KLEE: WARNING: killing 13381 states (over memory cap)
KLEE: WARNING: killing 13478 states (over memory cap)
KLEE: WARNING: killing 13572 states (over memory cap)
KLEE: WARNING: killing 13333 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13528 states (over memory cap)
KLEE: WARNING: killing 13734 states (over memory cap)
KLEE: WARNING: killing 13829 states (over memory cap)
KLEE: WARNING: killing 13604 states (over memory cap)
KLEE: WARNING: killing 13485 states (over memory cap)
KLEE: WARNING: killing 13576 states (over memory cap)
KLEE: WARNING: killing 13996 states (over memory cap)
KLEE: WARNING: killing 13668 states (over memory cap)
KLEE: WARNING: killing 13114 states (over memory cap)
KLEE: WARNING: killing 13851 states (over memory cap)
KLEE: WARNING: killing 14681 states (over memory cap)
KLEE: WARNING: killing 13510 states (over memory cap)
KLEE: WARNING: killing 13595 states (over memory cap)
KLEE: WARNING: killing 14003 states (over memory cap)
KLEE: WARNING: killing 14106 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13548 states (over memory cap)
KLEE: WARNING: killing 13324 states (over memory cap)
KLEE: WARNING: killing 13948 states (over memory cap)
KLEE: WARNING: killing 14042 states (over memory cap)
KLEE: WARNING: killing 13188 states (over memory cap)
KLEE: WARNING: killing 13486 states (over memory cap)
KLEE: WARNING: killing 13577 states (over memory cap)
KLEE: WARNING: killing 14414 states (over memory cap)
KLEE: WARNING: killing 13664 states (over memory cap)
KLEE: WARNING: killing 13545 states (over memory cap)
KLEE: WARNING: killing 13853 states (over memory cap)
KLEE: WARNING: killing 13422 states (over memory cap)
KLEE: WARNING: killing 13821 states (over memory cap)
KLEE: WARNING: killing 12975 states (over memory cap)
KLEE: WARNING: killing 14113 states (over memory cap)
KLEE: WARNING: killing 13065 states (over memory cap)
KLEE: WARNING: killing 13678 states (over memory cap)
KLEE: WARNING: killing 13252 states (over memory cap)
KLEE: WARNING: killing 13968 states (over memory cap)
KLEE: WARNING: killing 13746 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 13624 states (over memory cap)
KLEE: WARNING: killing 13913 states (over memory cap)
KLEE: WARNING: killing 13798 states (over memory cap)
KLEE: WARNING: killing 12754 states (over memory cap)
KLEE: WARNING: killing 13774 states (over memory cap)
KLEE: WARNING: killing 13873 states (over memory cap)
KLEE: WARNING: killing 14068 states (over memory cap)
KLEE: WARNING: killing 13838 states (over memory cap)
KLEE: WARNING: killing 13730 states (over memory cap)
KLEE: WARNING: killing 13307 states (over memory cap)
KLEE: WARNING: killing 13915 states (over memory cap)
KLEE: WARNING: killing 13803 states (over memory cap)
KLEE: WARNING: killing 13890 states (over memory cap)
KLEE: WARNING: killing 13468 states (over memory cap)
KLEE: WARNING: killing 13247 states (over memory cap)
KLEE: WARNING: killing 13332 states (over memory cap)
KLEE: WARNING: killing 13940 states (over memory cap)
KLEE: WARNING: killing 13421 states (over memory cap)
KLEE: WARNING: killing 13817 states (over memory cap)
KLEE: WARNING: killing 13809 states (over memory cap)
KLEE: WARNING: killing 13694 states (over memory cap)
KLEE: WARNING: killing 13373 states (over memory cap)
KLEE: WARNING: killing 14274 states (over memory cap)
KLEE: WARNING: killing 13657 states (over memory cap)
KLEE: WARNING: killing 14257 states (over memory cap)
KLEE: WARNING: killing 13739 states (over memory cap)
KLEE: WARNING: killing 13418 states (over memory cap)
KLEE: WARNING: killing 13813 states (over memory cap)
KLEE: WARNING: killing 13598 states (over memory cap)
KLEE: WARNING: killing 13383 states (over memory cap)
KLEE: WARNING: killing 13271 states (over memory cap)
KLEE: WARNING: killing 13255 states (over memory cap)
KLEE: WARNING: killing 13857 states (over memory cap)
