bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--pci--ivtv--ivtv.ko-entry_point_true-unreach-call.cil.out.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.: 798 547 7119 50821
Removed infinite loop in dma_sync_single_for_device___0
Removed infinite loop in dma_map_sg_attrs
Removed infinite loop in sg_page
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in sg_assign_page
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in dma_sync_single_for_cpu___0
Removed infinite loop in dma_unmap_sg_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_sync_single_for_device
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 2.11311388016
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_arg' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function schedule_timeout as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function schedule_timeout_interruptible as symbolic
Removed calls to 'put_page' (function is undefined)
Defining function get_user_pages_unlocked as symbolic
Removed calls to 'debug_dma_map_sg' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Defining function sg_next as symbolic
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'cx2341x_handler_set_50hz' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function cx2341x_handler_setup as symbolic
Defining function autoremove_wake_function as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'cx2341x_handler_set_busy' (function is undefined)
Defining function v4l2_ctrl_g_ctrl as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function default_wake_function as symbolic
Defining function del_timer as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_kthread_worker' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'v4l2_ctrl_cluster' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Removed calls to 'flush_kthread_worker' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'v4l2_event_queue' (function is undefined)
Defining function kthread_stop as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function flush_work as symbolic
Defining function __request_module as symbolic
Defining function v4l2_device_set_name as symbolic
Defining function v4l2_device_register as symbolic
Defining function cx2341x_handler_init as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'v4l2_subdev_init' (function is undefined)
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_new_std_menu as symbolic
Removed calls to 'add_timer' (function is undefined)
Defining function queue_work_on as symbolic
Defining function __video_register_device as symbolic
Defining function snprintf as symbolic
Defining function request_threaded_irq as symbolic
Defining function queue_kthread_work as symbolic
Defining function __memmove as symbolic
Defining function strstr as symbolic
Defining function strlcpy as symbolic
Defining function i2c_new_probed_device as symbolic
Defining function v4l2_i2c_new_subdev as symbolic
Defining function v4l2_i2c_new_subdev_board as symbolic
Defining function i2c_master_send as symbolic
Defining function i2c_master_recv as symbolic
Removed calls to 'tveeprom_hauppauge_analog' (function is undefined)
Defining function tveeprom_read as symbolic
Defining function sprintf as symbolic
Defining function i2c_add_adapter as symbolic
Defining function i2c_bit_add_bus as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Defining function v4l2_device_register_subdev as symbolic
Defining function pci_enable_device as symbolic
Defining function __request_region as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function dma_set_mask as symbolic
Defining function kthread_worker_fn as symbolic
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function sched_setscheduler as symbolic
Removed calls to 'v4l2_ctrl_handler_log_status' (function is undefined)
Defining function v4l2_subdev_queryctrl as symbolic
Defining function v4l2_subdev_g_ctrl as symbolic
Defining function v4l2_subdev_s_ctrl as symbolic
Defining function v4l2_subdev_g_ext_ctrls as symbolic
Defining function v4l2_subdev_s_ext_ctrls as symbolic
Defining function v4l2_subdev_try_ext_ctrls as symbolic
Defining function v4l2_subdev_querymenu as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function __v4l2_ctrl_s_ctrl as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function get_user_pages as symbolic
Defining function v4l2_event_subscribe as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function video_ioctl2 as symbolic
Removed calls to 'v4l2_fh_init' (function is undefined)
Removed calls to 'v4l2_fh_add' (function is undefined)
Removed calls to 'v4l2_fh_del' (function is undefined)
Removed calls to 'v4l2_fh_exit' (function is undefined)
Defining function v4l2_fh_is_singular as symbolic
Defining function video_devdata as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function v4l2_event_pending as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_shutdown_15 as symbolic
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  memchr
  memcmp
  strlen
  __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: 4.83473300934
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 970 462 4163 33159
INFO: Starting verification
KLEE: WARNING ONCE: function "ivtv_api_call" has inline asm
KLEE: WARNING ONCE: function "write_mailbox" has inline asm
KLEE: WARNING ONCE: function "try_mailbox" has inline asm
KLEE: WARNING ONCE: function "clear_all_mailboxes" has inline asm
KLEE: WARNING ONCE: function "ivtv_msleep_timeout" has inline asm
KLEE: WARNING ONCE: function "ivtv_g_pts_frame" has inline asm
KLEE: WARNING ONCE: function "ivtv_set_irq_mask" has inline asm
KLEE: WARNING ONCE: function "ivtv_clear_irq_mask" has inline asm
KLEE: WARNING ONCE: function "ivtv_reset_ir_gpio" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_setup" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_fill_sg_list" has inline asm
KLEE: WARNING ONCE: function "pci_map_sg" has inline asm
KLEE: WARNING ONCE: function "pci_dma_sync_single_for_cpu___0" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_prepare" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_start" has inline asm
KLEE: WARNING ONCE: function "ivtv_init_on_first_open" has inline asm
KLEE: WARNING ONCE: function "ivtv_firmware_init" has inline asm
KLEE: WARNING ONCE: function "ivtv_init_mpeg_decoder" has inline asm
KLEE: WARNING ONCE: function "ivtv_s_std_dec" has inline asm
KLEE: WARNING ONCE: function "load_fw_direct" has inline asm
KLEE: WARNING ONCE: function "ivtv_halt_firmware" has inline asm
KLEE: WARNING ONCE: function "ivtv_search_mailbox" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_filter_check" has inline asm
KLEE: WARNING ONCE: function "ivtv_firmware_check" has inline asm
KLEE: WARNING ONCE: function "ivtv_claim_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_release_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_start_v4l2_encode_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_passthrough_mode" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop_v4l2_encode_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_probe" has inline asm
KLEE: WARNING ONCE: function "ivtv_remove" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop_v4l2_decode_stream" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "ivtv_irq_work_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_unfinished_dma" has inline asm
KLEE: WARNING ONCE: function "ivtv_gpio_init" has inline asm
KLEE: WARNING ONCE: function "init_ivtv_i2c" has inline asm
KLEE: WARNING ONCE: function "ivtv_reset_tuner_gpio" has inline asm
KLEE: WARNING ONCE: function "ivtv_irq_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_streams_setup" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_dec_start_xfer" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_enc_start_xfer" has inline asm
KLEE: WARNING ONCE: function "dma_post" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_dec_start" has inline asm
KLEE: WARNING ONCE: function "stream_enc_dma_append" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_stream_dec_prepare" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_enc_start" has inline asm
KLEE: WARNING ONCE: function "pci_dma_sync_single_for_device" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_next_free" has inline asm
KLEE: WARNING ONCE: function "ivtv_process_vbi_data" has inline asm
KLEE: WARNING ONCE: function "ivtv_write_vbi_line" has inline asm
KLEE: WARNING ONCE: function "pci_dma_sync_single_for_cpu" has inline asm
KLEE: WARNING ONCE: function "ivtv_vbi_work_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_work_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_filter" has inline asm
KLEE: WARNING ONCE: function "subdev_log_status" has inline asm
KLEE: WARNING ONCE: function "subdev_s_radio" has inline asm
KLEE: WARNING ONCE: function "subdev_g_tuner" has inline asm
KLEE: WARNING ONCE: function "subdev_s_tuner" has inline asm
KLEE: WARNING ONCE: function "subdev_s_clock_freq" has inline asm
KLEE: WARNING ONCE: function "subdev_s_audio_routing" has inline asm
KLEE: WARNING ONCE: function "subdev_s_video_routing" has inline asm
KLEE: WARNING ONCE: function "subdev_s_ctrl" has inline asm
KLEE: WARNING ONCE: function "ivtv_xfer" has inline asm
KLEE: WARNING ONCE: function "ivtv_sendbyte" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop" has inline asm
KLEE: WARNING ONCE: function "ivtv_start" has inline asm
KLEE: WARNING ONCE: function "ivtv_setsda_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_setscl_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_getsda_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_getscl_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_g_fbuf" has inline asm
KLEE: WARNING ONCE: function "ivtv_encoder_cmd" has inline asm
KLEE: WARNING ONCE: function "ivtv_log_status" has inline asm
KLEE: WARNING ONCE: function "ivtv_default" has inline asm
KLEE: WARNING ONCE: function "ivtv_video_command" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_udma_frame" has inline asm
KLEE: WARNING ONCE: function "ivtv_start_v4l2_decode_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_set_speed" has inline asm
KLEE: WARNING ONCE: function "ivtv_itvc" has inline asm
KLEE: WARNING ONCE: function "ivtv_start_capture" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop_capture" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_read" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_write" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_open" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_close" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_close" has inline asm
KLEE: WARNING ONCE: function "ivtv_waitq" has inline asm
KLEE: WARNING ONCE: function "ivtv_write_vbi_from_user" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_dec_poll" has inline asm
KLEE: WARNING ONCE: function "ivtv_api_get_data" has inline asm
KLEE: WARNING ONCE: function "ivtv_disable_cc" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_12" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_8" has inline asm
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-Vwbkqx/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "ivtv_api_call" has inline asm
KLEE: WARNING ONCE: function "write_mailbox" has inline asm
KLEE: WARNING ONCE: function "try_mailbox" has inline asm
KLEE: WARNING ONCE: function "clear_all_mailboxes" has inline asm
KLEE: WARNING ONCE: function "ivtv_msleep_timeout" has inline asm
KLEE: WARNING ONCE: function "ivtv_g_pts_frame" has inline asm
KLEE: WARNING ONCE: function "ivtv_set_irq_mask" has inline asm
KLEE: WARNING ONCE: function "ivtv_clear_irq_mask" has inline asm
KLEE: WARNING ONCE: function "ivtv_reset_ir_gpio" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_setup" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_fill_sg_list" has inline asm
KLEE: WARNING ONCE: function "pci_map_sg" has inline asm
KLEE: WARNING ONCE: function "pci_dma_sync_single_for_cpu___0" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_prepare" has inline asm
KLEE: WARNING ONCE: function "ivtv_udma_start" has inline asm
KLEE: WARNING ONCE: function "ivtv_init_on_first_open" has inline asm
KLEE: WARNING ONCE: function "ivtv_firmware_init" has inline asm
KLEE: WARNING ONCE: function "ivtv_init_mpeg_decoder" has inline asm
KLEE: WARNING ONCE: function "ivtv_s_std_dec" has inline asm
KLEE: WARNING ONCE: function "load_fw_direct" has inline asm
KLEE: WARNING ONCE: function "ivtv_halt_firmware" has inline asm
KLEE: WARNING ONCE: function "ivtv_search_mailbox" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_filter_check" has inline asm
KLEE: WARNING ONCE: function "ivtv_firmware_check" has inline asm
KLEE: WARNING ONCE: function "ivtv_claim_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_release_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_start_v4l2_encode_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_passthrough_mode" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop_v4l2_encode_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_probe" has inline asm
KLEE: WARNING ONCE: function "ivtv_remove" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop_v4l2_decode_stream" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "ivtv_irq_work_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_unfinished_dma" has inline asm
KLEE: WARNING ONCE: function "ivtv_gpio_init" has inline asm
KLEE: WARNING ONCE: function "init_ivtv_i2c" has inline asm
KLEE: WARNING ONCE: function "ivtv_reset_tuner_gpio" has inline asm
KLEE: WARNING ONCE: function "ivtv_irq_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_streams_setup" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_dec_start_xfer" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_enc_start_xfer" has inline asm
KLEE: WARNING ONCE: function "dma_post" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_dec_start" has inline asm
KLEE: WARNING ONCE: function "stream_enc_dma_append" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_stream_dec_prepare" has inline asm
KLEE: WARNING ONCE: function "ivtv_dma_enc_start" has inline asm
KLEE: WARNING ONCE: function "pci_dma_sync_single_for_device" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_next_free" has inline asm
KLEE: WARNING ONCE: function "ivtv_process_vbi_data" has inline asm
KLEE: WARNING ONCE: function "ivtv_write_vbi_line" has inline asm
KLEE: WARNING ONCE: function "pci_dma_sync_single_for_cpu" has inline asm
KLEE: WARNING ONCE: function "ivtv_vbi_work_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_work_handler" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_filter" has inline asm
KLEE: WARNING ONCE: function "subdev_log_status" has inline asm
KLEE: WARNING ONCE: function "subdev_s_radio" has inline asm
KLEE: WARNING ONCE: function "subdev_g_tuner" has inline asm
KLEE: WARNING ONCE: function "subdev_s_tuner" has inline asm
KLEE: WARNING ONCE: function "subdev_s_clock_freq" has inline asm
KLEE: WARNING ONCE: function "subdev_s_audio_routing" has inline asm
KLEE: WARNING ONCE: function "subdev_s_video_routing" has inline asm
KLEE: WARNING ONCE: function "subdev_s_ctrl" has inline asm
KLEE: WARNING ONCE: function "ivtv_xfer" has inline asm
KLEE: WARNING ONCE: function "ivtv_sendbyte" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop" has inline asm
KLEE: WARNING ONCE: function "ivtv_start" has inline asm
KLEE: WARNING ONCE: function "ivtv_setsda_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_setscl_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_getsda_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_getscl_old" has inline asm
KLEE: WARNING ONCE: function "ivtv_g_fbuf" has inline asm
KLEE: WARNING ONCE: function "ivtv_encoder_cmd" has inline asm
KLEE: WARNING ONCE: function "ivtv_log_status" has inline asm
KLEE: WARNING ONCE: function "ivtv_default" has inline asm
KLEE: WARNING ONCE: function "ivtv_video_command" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_udma_frame" has inline asm
KLEE: WARNING ONCE: function "ivtv_start_v4l2_decode_stream" has inline asm
KLEE: WARNING ONCE: function "ivtv_set_speed" has inline asm
KLEE: WARNING ONCE: function "ivtv_itvc" has inline asm
KLEE: WARNING ONCE: function "ivtv_start_capture" has inline asm
KLEE: WARNING ONCE: function "ivtv_stop_capture" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_read" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_write" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_open" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_close" has inline asm
KLEE: WARNING ONCE: function "ivtv_yuv_close" has inline asm
KLEE: WARNING ONCE: function "ivtv_waitq" has inline asm
KLEE: WARNING ONCE: function "ivtv_write_vbi_from_user" has inline asm
KLEE: WARNING ONCE: function "ivtv_v4l2_dec_poll" has inline asm
KLEE: WARNING ONCE: function "ivtv_api_get_data" has inline asm
KLEE: WARNING ONCE: function "ivtv_disable_cc" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_12" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_8" has inline asm
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 7.59291696548
