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-cx25821-cx25821_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.: 398 424 2961 22427
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.735001802444
Defining function printk as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'btcx_riscmem_free' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function btcx_riscmem_alloc as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'v4l2_get_timestamp' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function mod_timer as symbolic
Defining function del_timer as symbolic
Defining function videobuf_to_dma as symbolic
Defining function videobuf_iolock as symbolic
Defining function videobuf_waiton as symbolic
Defining function videobuf_dma_unmap as symbolic
Defining function videobuf_dma_free as symbolic
Defining function videobuf_mmap_mapper as symbolic
Defining function video_devdata as symbolic
Defining function v4l2_ctrl_poll as symbolic
Defining function videobuf_poll_stream as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Defining function videobuf_read_one as symbolic
Defining function video_ioctl2 as symbolic
Defining function videobuf_dqbuf as symbolic
Defining function strlcpy as symbolic
Defining function videobuf_qbuf as symbolic
Defining function videobuf_querybuf as symbolic
Defining function sprintf as symbolic
Defining function videobuf_reqbufs as symbolic
Defining function videobuf_streamoff as symbolic
Defining function videobuf_streamon as symbolic
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function pci_enable_device as symbolic
Defining function dma_supported as symbolic
Defining function pci_bus_read_config_byte as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'videobuf_queue_sg_init' (function is undefined)
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function snprintf as symbolic
Defining function __video_register_device as symbolic
Defining function i2c_add_adapter as symbolic
Defining function ioremap_nocache as symbolic
Defining function __request_region as symbolic
Defining function v4l2_fh_open as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function v4l2_fh_release as symbolic
Removed calls to 'videobuf_queue_cancel' (function is undefined)
Defining function videobuf_mmap_free 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 'video_device_release_empty' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcpy
  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.72290802002
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 456 397 1512 12707
INFO: Starting verification
KLEE: WARNING ONCE: function "cx25821_sram_channel_setup_audio" has inline asm
KLEE: WARNING ONCE: function "cx25821_sram_channel_dump_audio" has inline asm
KLEE: WARNING ONCE: function "i2c_readbytes" has inline asm
KLEE: WARNING ONCE: function "i2c_sendbytes" has inline asm
KLEE: WARNING ONCE: function "i2c_wait_done" has inline asm
KLEE: WARNING ONCE: function "cx25821_video_unregister" has inline asm
KLEE: WARNING ONCE: function "cx25821_stop_upstream_video" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "cx25821_risc_databuffer_audio" has inline asm
KLEE: WARNING ONCE: function "cx25821_irq" has inline asm
KLEE: WARNING ONCE: function "cx25821_video_irq" has inline asm
KLEE: WARNING ONCE: function "cx25821_sram_channel_dump" has inline asm
KLEE: WARNING ONCE: function "cx25821_start_video_dma" has inline asm
KLEE: WARNING ONCE: function "cx25821_sram_channel_setup" has inline asm
KLEE: WARNING ONCE: function "cx25821_set_gpiopin_direction" has inline asm
KLEE: WARNING ONCE: function "cx25821_buffer_prepare" has inline asm
KLEE: WARNING ONCE: function "cx25821_free_buffer" has inline asm
KLEE: WARNING ONCE: function "cx25821_risc_buffer" has inline asm
KLEE: WARNING ONCE: function "vidioc_log_status" has inline asm
KLEE: WARNING ONCE: function "vidioc_s_fmt_vid_cap" has inline asm
KLEE: WARNING ONCE: function "cx25821_vidupstream_init" has inline asm
KLEE: WARNING ONCE: function "cx25821_sram_channel_setup_upstream" has inline asm
KLEE: WARNING ONCE: function "cx25821_upstream_irq" has inline asm
KLEE: WARNING ONCE: function "cx25821_initdev" has inline asm
KLEE: WARNING ONCE: function "cx25821_shutdown" has inline asm
KLEE: WARNING ONCE: function "cx25821_gpio_init" has inline asm
KLEE: WARNING ONCE: function "cx25821_video_register" has inline asm
KLEE: WARNING ONCE: function "cx25821_vid_timeout" has inline asm
KLEE: WARNING ONCE: function "video_release" has inline asm
KLEE: WARNING ONCE: function "cx25821_set_pixel_format" has inline asm
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_ad2ebc5c-dd44-4556-93a2-88298af913c1/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 15177 states (over memory cap)
KLEE: WARNING: killing 23344 states (over memory cap)
KLEE: WARNING: killing 23477 states (over memory cap)
KLEE: WARNING: killing 23383 states (over memory cap)
KLEE: WARNING: killing 22700 states (over memory cap)
KLEE: WARNING: killing 12500 states (over memory cap)
KLEE: WARNING: killing 22363 states (over memory cap)
KLEE: WARNING: killing 11968 states (over memory cap)
KLEE: WARNING: killing 21902 states (over memory cap)
KLEE: WARNING: killing 12268 states (over memory cap)
KLEE: WARNING: killing 23820 states (over memory cap)
KLEE: WARNING: killing 13390 states (over memory cap)
KLEE: WARNING: killing 12428 states (over memory cap)
KLEE: WARNING: killing 12524 states (over memory cap)
KLEE: WARNING: killing 13089 states (over memory cap)
KLEE: WARNING: killing 13424 states (over memory cap)
KLEE: WARNING: killing 13281 states (over memory cap)
KLEE: WARNING: killing 13143 states (over memory cap)
KLEE: WARNING: killing 12658 states (over memory cap)
KLEE: WARNING: killing 12987 states (over memory cap)
KLEE: WARNING: killing 13896 states (over memory cap)
KLEE: WARNING: killing 13648 states (over memory cap)
KLEE: WARNING: killing 13046 states (over memory cap)
KLEE: WARNING: killing 12915 states (over memory cap)
KLEE: WARNING: killing 13593 states (over memory cap)
KLEE: WARNING: killing 13459 states (over memory cap)
KLEE: WARNING: killing 13212 states (over memory cap)
KLEE: WARNING: killing 13422 states (over memory cap)
KLEE: WARNING: killing 13409 states (over memory cap)
KLEE: WARNING: killing 13274 states (over memory cap)
KLEE: WARNING: killing 13259 states (over memory cap)
KLEE: WARNING: killing 13134 states (over memory cap)
KLEE: WARNING: killing 13111 states (over memory cap)
KLEE: WARNING: killing 13555 states (over memory cap)
KLEE: WARNING: killing 12963 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12477 states (over memory cap)
KLEE: WARNING: killing 12692 states (over memory cap)
KLEE: WARNING: killing 13475 states (over memory cap)
KLEE: WARNING: killing 12212 states (over memory cap)
KLEE: WARNING: killing 12192 states (over memory cap)
KLEE: WARNING: killing 12743 states (over memory cap)
KLEE: WARNING: killing 12840 states (over memory cap)
KLEE: WARNING: killing 12258 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 12907 states (over memory cap)
KLEE: WARNING: killing 12217 states (over memory cap)
KLEE: WARNING: killing 12535 states (over memory cap)
KLEE: WARNING: killing 12291 states (over memory cap)
KLEE: WARNING: killing 13067 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12705 states (over memory cap)
KLEE: WARNING: killing 12358 states (over memory cap)
KLEE: WARNING: killing 12787 states (over memory cap)
KLEE: WARNING: killing 12553 states (over memory cap)
KLEE: WARNING: killing 12866 states (over memory cap)
KLEE: WARNING: killing 13407 states (over memory cap)
KLEE: WARNING: killing 12614 states (over memory cap)
KLEE: WARNING: killing 13157 states (over memory cap)
KLEE: WARNING: killing 12698 states (over memory cap)
KLEE: WARNING: killing 12460 states (over memory cap)
KLEE: WARNING: killing 12112 states (over memory cap)
KLEE: WARNING: killing 12762 states (over memory cap)
KLEE: WARNING: killing 12751 states (over memory cap)
KLEE: WARNING: killing 13182 states (over memory cap)
KLEE: WARNING: killing 12834 states (over memory cap)
KLEE: WARNING: killing 12715 states (over memory cap)
KLEE: WARNING: killing 12921 states (over memory cap)
KLEE: WARNING: killing 12574 states (over memory cap)
KLEE: WARNING: killing 12668 states (over memory cap)
KLEE: WARNING: killing 13313 states (over memory cap)
KLEE: WARNING: killing 12199 states (over memory cap)
KLEE: WARNING: killing 12296 states (over memory cap)
KLEE: WARNING: killing 12720 states (over memory cap)
KLEE: WARNING: killing 13145 states (over memory cap)
KLEE: WARNING: killing 12366 states (over memory cap)
KLEE: WARNING: killing 12899 states (over memory cap)
KLEE: WARNING: killing 12342 states (over memory cap)
KLEE: WARNING: killing 12214 states (over memory cap)
KLEE: WARNING: killing 12857 states (over memory cap)
KLEE: WARNING: killing 12733 states (over memory cap)
KLEE: WARNING: killing 12612 states (over memory cap)
KLEE: WARNING: killing 13248 states (over memory cap)
KLEE: WARNING: killing 12589 states (over memory cap)
KLEE: WARNING: killing 12791 states (over memory cap)
KLEE: WARNING: killing 13210 states (over memory cap)
KLEE: WARNING: killing 12872 states (over memory cap)
KLEE: WARNING: killing 12427 states (over memory cap)
KLEE: WARNING: killing 12738 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 13235 states (over memory cap)
KLEE: WARNING: killing 12257 states (over memory cap)
KLEE: WARNING: killing 13106 states (over memory cap)
KLEE: WARNING: killing 12343 states (over memory cap)
KLEE: WARNING: killing 12862 states (over memory cap)
KLEE: WARNING: killing 12637 states (over memory cap)
KLEE: WARNING: killing 12514 states (over memory cap)
KLEE: WARNING: killing 12394 states (over memory cap)
KLEE: WARNING: killing 12910 states (over memory cap)
KLEE: WARNING: killing 12474 states (over memory cap)
KLEE: WARNING: killing 12460 states (over memory cap)
KLEE: WARNING: killing 12765 states (over memory cap)
KLEE: WARNING: killing 12753 states (over memory cap)
KLEE: WARNING: killing 12952 states (over memory cap)
KLEE: WARNING: killing 12622 states (over memory cap)
KLEE: WARNING: killing 12397 states (over memory cap)
KLEE: WARNING: killing 12275 states (over memory cap)
KLEE: WARNING: killing 12480 states (over memory cap)
KLEE: WARNING: killing 12789 states (over memory cap)
KLEE: WARNING: killing 12461 states (over memory cap)
KLEE: WARNING: killing 12026 states (over memory cap)
KLEE: WARNING: killing 12011 states (over memory cap)
KLEE: WARNING: killing 12315 states (over memory cap)
KLEE: WARNING: killing 12088 states (over memory cap)
KLEE: WARNING: killing 12712 states (over memory cap)
KLEE: WARNING: killing 12705 states (over memory cap)
KLEE: WARNING: killing 12692 states (over memory cap)
KLEE: WARNING: killing 13103 states (over memory cap)
KLEE: WARNING: killing 12778 states (over memory cap)
KLEE: WARNING: killing 13075 states (over memory cap)
KLEE: WARNING: killing 12745 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 12827 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 13220 states (over memory cap)
KLEE: WARNING: killing 12896 states (over memory cap)
KLEE: WARNING: killing 12672 states (over memory cap)
KLEE: WARNING: killing 12976 states (over memory cap)
KLEE: WARNING: killing 13067 states (over memory cap)
KLEE: WARNING: killing 12634 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 12302 states (over memory cap)
KLEE: WARNING: killing 12495 states (over memory cap)
KLEE: WARNING: killing 11871 states (over memory cap)
KLEE: WARNING: killing 13097 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 12562 states (over memory cap)
KLEE: WARNING: killing 12551 states (over memory cap)
KLEE: WARNING: killing 12644 states (over memory cap)
KLEE: WARNING: killing 13044 states (over memory cap)
KLEE: WARNING: killing 12929 states (over memory cap)
KLEE: WARNING: killing 12815 states (over memory cap)
KLEE: WARNING: killing 12913 states (over memory cap)
KLEE: WARNING: killing 12486 states (over memory cap)
KLEE: WARNING: killing 12480 states (over memory cap)
KLEE: WARNING: killing 12259 states (over memory cap)
KLEE: WARNING: killing 12757 states (over memory cap)
KLEE: WARNING: killing 12640 states (over memory cap)
KLEE: WARNING: killing 12832 states (over memory cap)
KLEE: WARNING: killing 12418 states (over memory cap)
KLEE: WARNING: killing 13123 states (over memory cap)
KLEE: WARNING: killing 12802 states (over memory cap)
KLEE: WARNING: killing 12586 states (over memory cap)
KLEE: WARNING: killing 12677 states (over memory cap)
KLEE: WARNING: killing 12671 states (over memory cap)
KLEE: WARNING: killing 12253 states (over memory cap)
KLEE: WARNING: killing 12039 states (over memory cap)
KLEE: WARNING: killing 12532 states (over memory cap)
KLEE: WARNING: killing 12521 states (over memory cap)
KLEE: WARNING: killing 12613 states (over memory cap)
KLEE: WARNING: killing 12701 states (over memory cap)
KLEE: WARNING: killing 12286 states (over memory cap)
KLEE: WARNING: killing 12070 states (over memory cap)
KLEE: WARNING: killing 12768 states (over memory cap)
KLEE: WARNING: killing 12764 states (over memory cap)
KLEE: WARNING: killing 12957 states (over memory cap)
KLEE: WARNING: killing 12547 states (over memory cap)
KLEE: WARNING: killing 12535 states (over memory cap)
KLEE: WARNING: killing 12421 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 12194 states (over memory cap)
KLEE: WARNING: killing 12682 states (over memory cap)
KLEE: WARNING: killing 12276 states (over memory cap)
KLEE: WARNING: killing 12860 states (over memory cap)
KLEE: WARNING: killing 13350 states (over memory cap)
KLEE: WARNING: killing 13047 states (over memory cap)
KLEE: WARNING: killing 12428 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 13491 states (over memory cap)
KLEE: WARNING: killing 12683 states (over memory cap)
KLEE: WARNING: killing 12470 states (over memory cap)
KLEE: WARNING: killing 12657 states (over memory cap)
KLEE: WARNING: killing 12748 states (over memory cap)
KLEE: WARNING: killing 12737 states (over memory cap)
KLEE: WARNING: killing 13418 states (over memory cap)
KLEE: WARNING: killing 12714 states (over memory cap)
KLEE: WARNING: killing 12900 states (over memory cap)
KLEE: WARNING: killing 12496 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 12775 states (over memory cap)
KLEE: WARNING: killing 12767 states (over memory cap)
KLEE: WARNING: killing 12659 states (over memory cap)
KLEE: WARNING: killing 12547 states (over memory cap)
KLEE: WARNING: killing 12727 states (over memory cap)
KLEE: WARNING: killing 12227 states (over memory cap)
KLEE: WARNING: killing 11722 states (over memory cap)
KLEE: WARNING: killing 11808 states (over memory cap)
KLEE: WARNING: killing 12876 states (over memory cap)
KLEE: WARNING: killing 13059 states (over memory cap)
KLEE: WARNING: killing 12660 states (over memory cap)
KLEE: WARNING: killing 12553 states (over memory cap)
KLEE: WARNING: killing 12444 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-fFIVzS/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-pci-cx25821-cx25821_true-unreach-call.cil.c:8303: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13022 states (over memory cap)
KLEE: WARNING: killing 12519 states (over memory cap)
KLEE: WARNING: killing 13189 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 12780 states (over memory cap)
KLEE: WARNING: killing 12873 states (over memory cap)
KLEE: WARNING: killing 12958 states (over memory cap)
KLEE: WARNING: killing 12748 states (over memory cap)
KLEE: WARNING: killing 12541 states (over memory cap)
KLEE: WARNING: killing 12534 states (over memory cap)
