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-cx88-cx8800_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.: 304 399 2500 16307
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.654173135757
Removed calls to 'cx88_set_tvaudio' (function is undefined)
Defining function printk as symbolic
Defining function video_devdata as symbolic
Defining function strlcpy as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'cx88_newstation' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'cx88_print_irqbits' (function is undefined)
Removed calls to 'cx88_sram_channel_dump' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'cx88_wakeup' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function cx88_core_irq as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function mod_timer as symbolic
Defining function cx88_sram_channel_setup as symbolic
Defining function cx88_set_scale as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Defining function v4l2_ctrl_find as symbolic
Defining function v4l2_ctrl_s_ctrl as symbolic
Removed calls to 'cx88_free_buffer' (function is undefined)
Defining function videobuf_to_dma as symbolic
Defining function videobuf_iolock as symbolic
Defining function cx88_risc_buffer as symbolic
Defining function v4l2_ctrl_poll as symbolic
Defining function video_ioctl2 as symbolic
Defining function videobuf_dqbuf as symbolic
Removed calls to 'cx88_get_stereo' (function is undefined)
Defining function videobuf_qbuf as symbolic
Defining function videobuf_querybuf as symbolic
Defining function sprintf as symbolic
Defining function videobuf_reqbufs as symbolic
Removed calls to 'v4l_bound_align_image' (function is undefined)
Defining function cx88_set_tvnorm as symbolic
Removed calls to 'cx88_set_stereo' (function is undefined)
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
Defining function videobuf_mmap_mapper as symbolic
Defining function videobuf_poll_stream as symbolic
Defining function videobuf_read_one as symbolic
Defining function videobuf_read_stream 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)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'cx88_core_put' (function is undefined)
Removed calls to 'cx88_ir_stop' (function is undefined)
Removed calls to 'cx88_shutdown' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'btcx_riscmem_free' (function is undefined)
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function pci_set_power_state as symbolic
Defining function cx88_reset as symbolic
Defining function cx88_ir_start as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Defining function del_timer as symbolic
Defining function kthread_stop as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'video_device_release' (function is undefined)
Defining function cx88_core_get as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function cx88_risc_stopper as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_add_handler as symbolic
Defining function v4l2_i2c_new_subdev_board as symbolic
Defining function v4l2_i2c_new_subdev as symbolic
Defining function __request_module as symbolic
Defining function i2c_new_device as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Defining function cx88_vdev_init as symbolic
Defining function cx88_audio_thread as symbolic
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function __video_register_device as symbolic
Defining function request_threaded_irq as symbolic
Defining function dma_supported as symbolic
Defining function pci_bus_read_config_byte as symbolic
Removed calls to 'v4l2_fh_init' (function is undefined)
Removed calls to 'videobuf_queue_sg_init' (function is undefined)
Removed calls to 'v4l2_fh_add' (function is undefined)
Removed calls to 'videobuf_queue_cancel' (function is undefined)
Removed calls to 'videobuf_stop' (function is undefined)
Removed calls to 'v4l2_fh_del' (function is undefined)
Removed calls to 'v4l2_fh_exit' (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 '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.578413009644
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 355 407 1354 9450
INFO: Starting verification
KLEE: WARNING ONCE: function "cx88_video_mux" has inline asm
KLEE: WARNING ONCE: function "cx8800_irq" has inline asm
KLEE: WARNING ONCE: function "cx8800_start_vbi_dma" has inline asm
KLEE: WARNING ONCE: function "start_video_dma" has inline asm
KLEE: WARNING ONCE: function "cx8800_s_aud_ctrl" has inline asm
KLEE: WARNING ONCE: function "cx8800_s_vid_ctrl" has inline asm
KLEE: WARNING ONCE: function "buffer_prepare" has inline asm
KLEE: WARNING ONCE: function "get_queue" has inline asm
KLEE: WARNING ONCE: function "vidioc_g_register" has inline asm
KLEE: WARNING ONCE: function "vidioc_g_tuner" has inline asm
KLEE: WARNING ONCE: function "vidioc_s_register" has inline asm
KLEE: WARNING ONCE: function "get_resource" has inline asm
KLEE: WARNING ONCE: function "res_free" has inline asm
KLEE: WARNING ONCE: function "video_read" has inline asm
KLEE: WARNING ONCE: function "cx8800_initdev" has inline asm
KLEE: WARNING ONCE: function "cx8800_suspend" has inline asm
KLEE: WARNING ONCE: function "cx8800_resume" has inline asm
KLEE: WARNING ONCE: function "cx8800_stop_vbi_dma" has inline asm
KLEE: WARNING ONCE: function "cx8800_vid_timeout" has inline asm
KLEE: WARNING ONCE: function "cx8800_vbi_timeout" has inline asm
KLEE: WARNING ONCE: function "video_open" has inline asm
KLEE: WARNING ONCE: function "ldv_v4l2_file_operations_io_instance_7" has inline asm
KLEE: WARNING ONCE: function "ldv_v4l2_file_operations_io_instance_8" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_8_33" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_8_48" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_7_33" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_7_48" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_d227fbbe-f517-4ed3-8b34-ac6451594806/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 21075 states (over memory cap)
KLEE: WARNING: killing 23603 states (over memory cap)
KLEE: WARNING: killing 24337 states (over memory cap)
KLEE: WARNING: killing 23685 states (over memory cap)
KLEE: WARNING: killing 23346 states (over memory cap)
KLEE: WARNING: killing 22848 states (over memory cap)
KLEE: WARNING: killing 22646 states (over memory cap)
KLEE: WARNING: killing 24065 states (over memory cap)
KLEE: WARNING: killing 23712 states (over memory cap)
KLEE: WARNING: killing 23921 states (over memory cap)
KLEE: WARNING: killing 24925 states (over memory cap)
KLEE: WARNING: killing 25791 states (over memory cap)
KLEE: WARNING: killing 24630 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 26260 states (over memory cap)
KLEE: WARNING: killing 13612 states (over memory cap)
KLEE: WARNING: killing 13721 states (over memory cap)
KLEE: WARNING: killing 13696 states (over memory cap)
KLEE: WARNING: killing 13412 states (over memory cap)
KLEE: WARNING: killing 13398 states (over memory cap)
KLEE: WARNING: killing 13511 states (over memory cap)
KLEE: WARNING: killing 13749 states (over memory cap)
KLEE: WARNING: killing 13468 states (over memory cap)
KLEE: WARNING: killing 13315 states (over memory cap)
KLEE: WARNING: killing 13428 states (over memory cap)
KLEE: WARNING: killing 13413 states (over memory cap)
KLEE: WARNING: killing 13792 states (over memory cap)
KLEE: WARNING: killing 13516 states (over memory cap)
KLEE: WARNING: killing 13768 states (over memory cap)
KLEE: WARNING: killing 13490 states (over memory cap)
KLEE: WARNING: killing 25174 states (over memory cap)
KLEE: WARNING: killing 13840 states (over memory cap)
KLEE: WARNING: killing 25210 states (over memory cap)
KLEE: WARNING: killing 13394 states (over memory cap)
KLEE: WARNING: killing 25260 states (over memory cap)
KLEE: WARNING: killing 12959 states (over memory cap)
KLEE: WARNING: killing 25554 states (over memory cap)
KLEE: WARNING: killing 13178 states (over memory cap)
KLEE: WARNING: killing 25088 states (over memory cap)
KLEE: WARNING: killing 13510 states (over memory cap)
KLEE: WARNING: killing 24738 states (over memory cap)
KLEE: WARNING: killing 13209 states (over memory cap)
KLEE: WARNING: killing 24264 states (over memory cap)
KLEE: WARNING: killing 13287 states (over memory cap)
KLEE: WARNING: killing 24063 states (over memory cap)
KLEE: WARNING: killing 13369 states (over memory cap)
KLEE: WARNING: killing 24232 states (over memory cap)
KLEE: WARNING: killing 13202 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 24644 states (over memory cap)
KLEE: WARNING: killing 13523 states (over memory cap)
KLEE: WARNING: killing 24434 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 12713 states (over memory cap)
KLEE: WARNING: killing 13448 states (over memory cap)
KLEE: WARNING: killing 13316 states (over memory cap)
KLEE: WARNING: killing 13171 states (over memory cap)
KLEE: WARNING: killing 12530 states (over memory cap)
KLEE: WARNING: killing 13138 states (over memory cap)
KLEE: WARNING: killing 12750 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 12476 states (over memory cap)
KLEE: WARNING: killing 12958 states (over memory cap)
KLEE: WARNING: killing 13070 states (over memory cap)
KLEE: WARNING: killing 12444 states (over memory cap)
KLEE: WARNING: killing 13046 states (over memory cap)
KLEE: WARNING: killing 24158 states (over memory cap)
KLEE: WARNING: killing 13750 states (over memory cap)
KLEE: WARNING: killing 12622 states (over memory cap)
KLEE: WARNING: killing 13349 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 12711 states (over memory cap)
KLEE: WARNING: killing 13074 states (over memory cap)
KLEE: WARNING: killing 12451 states (over memory cap)
KLEE: WARNING: killing 12676 states (over memory cap)
KLEE: WARNING: killing 12659 states (over memory cap)
KLEE: WARNING: killing 12277 states (over memory cap)
KLEE: WARNING: killing 12755 states (over memory cap)
KLEE: WARNING: killing 12746 states (over memory cap)
KLEE: WARNING: killing 13594 states (over memory cap)
KLEE: WARNING: killing 12724 states (over memory cap)
KLEE: WARNING: killing 12707 states (over memory cap)
KLEE: WARNING: killing 12208 states (over memory cap)
KLEE: WARNING: killing 13046 states (over memory cap)
KLEE: WARNING: killing 12547 states (over memory cap)
KLEE: WARNING: killing 13135 states (over memory cap)
KLEE: WARNING: killing 12397 states (over memory cap)
KLEE: WARNING: killing 13229 states (over memory cap)
KLEE: WARNING: killing 13100 states (over memory cap)
KLEE: WARNING: killing 12729 states (over memory cap)
KLEE: WARNING: killing 12952 states (over memory cap)
KLEE: WARNING: killing 12333 states (over memory cap)
KLEE: WARNING: killing 12563 states (over memory cap)
KLEE: WARNING: killing 12915 states (over memory cap)
KLEE: WARNING: killing 12783 states (over memory cap)
KLEE: WARNING: killing 12051 states (over memory cap)
KLEE: WARNING: killing 12996 states (over memory cap)
KLEE: WARNING: killing 12985 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 12113 states (over memory cap)
KLEE: WARNING: killing 12822 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 12797 states (over memory cap)
KLEE: WARNING: killing 12907 states (over memory cap)
KLEE: WARNING: killing 12066 states (over memory cap)
KLEE: WARNING: killing 12286 states (over memory cap)
KLEE: WARNING: killing 12877 states (over memory cap)
KLEE: WARNING: killing 12742 states (over memory cap)
KLEE: WARNING: killing 12497 states (over memory cap)
KLEE: WARNING: killing 13075 states (over memory cap)
KLEE: WARNING: killing 13183 states (over memory cap)
KLEE: WARNING: killing 12581 states (over memory cap)
KLEE: WARNING: killing 12806 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 12781 states (over memory cap)
KLEE: WARNING: killing 12173 states (over memory cap)
KLEE: WARNING: killing 12988 states (over memory cap)
KLEE: WARNING: killing 12626 states (over memory cap)
KLEE: WARNING: killing 12258 states (over memory cap)
KLEE: WARNING: killing 12711 states (over memory cap)
KLEE: WARNING: killing 12934 states (over memory cap)
KLEE: WARNING: killing 12571 states (over memory cap)
KLEE: WARNING: killing 13030 states (over memory cap)
KLEE: WARNING: killing 12670 states (over memory cap)
KLEE: WARNING: killing 13010 states (over memory cap)
KLEE: WARNING: killing 13115 states (over memory cap)
KLEE: WARNING: killing 12636 states (over memory cap)
KLEE: WARNING: killing 12978 states (over memory cap)
KLEE: WARNING: killing 12614 states (over memory cap)
KLEE: WARNING: killing 12835 states (over memory cap)
KLEE: WARNING: killing 12589 states (over memory cap)
KLEE: WARNING: killing 12459 states (over memory cap)
KLEE: WARNING: killing 12566 states (over memory cap)
KLEE: WARNING: killing 13020 states (over memory cap)
KLEE: WARNING: killing 13243 states (over memory cap)
KLEE: WARNING: killing 13351 states (over memory cap)
KLEE: WARNING: killing 12527 states (over memory cap)
KLEE: WARNING: killing 12748 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 13072 states (over memory cap)
KLEE: WARNING: killing 12712 states (over memory cap)
KLEE: WARNING: killing 11894 states (over memory cap)
KLEE: WARNING: killing 12570 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MJx53a/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-pci-cx88-cx8800_true-unreach-call.cil.c:9634: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13137 states (over memory cap)
KLEE: WARNING: killing 12780 states (over memory cap)
KLEE: WARNING: killing 12195 states (over memory cap)
KLEE: WARNING: killing 12756 states (over memory cap)
KLEE: WARNING: killing 12633 states (over memory cap)
KLEE: WARNING: killing 12390 states (over memory cap)
KLEE: WARNING: killing 13187 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12127 states (over memory cap)
KLEE: WARNING: killing 12116 states (over memory cap)
KLEE: WARNING: killing 12446 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MJx53a/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-pci-cx88-cx8800_true-unreach-call.cil.c:9719: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13011 states (over memory cap)
KLEE: WARNING: killing 12655 states (over memory cap)
KLEE: WARNING: killing 12759 states (over memory cap)
KLEE: WARNING: killing 12632 states (over memory cap)
KLEE: WARNING: killing 12624 states (over memory cap)
KLEE: WARNING: killing 12727 states (over memory cap)
KLEE: WARNING: killing 12943 states (over memory cap)
KLEE: WARNING: killing 12935 states (over memory cap)
KLEE: WARNING: killing 12928 states (over memory cap)
KLEE: WARNING: killing 12459 states (over memory cap)
KLEE: WARNING: killing 12560 states (over memory cap)
KLEE: WARNING: killing 12656 states (over memory cap)
KLEE: WARNING: killing 13099 states (over memory cap)
KLEE: WARNING: killing 12413 states (over memory cap)
KLEE: WARNING: killing 12971 states (over memory cap)
KLEE: WARNING: killing 13075 states (over memory cap)
KLEE: WARNING: killing 13403 states (over memory cap)
KLEE: WARNING: killing 12606 states (over memory cap)
KLEE: WARNING: killing 12818 states (over memory cap)
KLEE: WARNING: killing 12358 states (over memory cap)
KLEE: WARNING: killing 12569 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 12542 states (over memory cap)
KLEE: WARNING: killing 12983 states (over memory cap)
KLEE: WARNING: killing 12741 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 12279 states (over memory cap)
KLEE: WARNING: killing 12490 states (over memory cap)
