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-43_2a-drivers--media--pci--bt8xx--bttv.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.: 915 529 5073 37684
Removed infinite loop in bttv_dma_free
Removed infinite loop in bttv_risc_packed
Removed infinite loop in bttv_read
Removed infinite loop in set_tvnorm
Removed infinite loop in bttv_vbi_fmt_reset
Removed infinite loop in bttv_queue
Removed infinite loop in bttv_resource
Removed infinite loop in limit_scaled_size_lock
Removed infinite loop in bttv_overlay_risc
Removed infinite loop in bttv_risc_overlay
Removed infinite loop in try_fmt
Removed infinite loop in verify_window_lock
Removed infinite loop in setup_window_lock
Removed infinite loop in bttv_buffer_risc
Removed infinite loop in bttv_risc_planar
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.26008701324
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function videobuf_to_dma as symbolic
Defining function videobuf_waiton as symbolic
Defining function videobuf_dma_unmap as symbolic
Defining function videobuf_dma_free as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function printk as symbolic
Defining function del_timer as symbolic
Defining function mod_timer as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function videobuf_iolock as symbolic
Defining function sg_next as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function snprintf as symbolic
Defining function driver_register as symbolic
Removed calls to 'driver_unregister' (function is undefined)
Defining function v4l2_ctrl_find as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function __v4l2_ctrl_s_ctrl as symbolic
Defining function video_ioctl2 as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
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_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_streamoff as symbolic
Defining function videobuf_mmap_free as symbolic
Defining function video_devdata as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function videobuf_mmap_mapper as symbolic
Defining function v4l2_event_pending as symbolic
Defining function videobuf_poll_stream as symbolic
Defining function videobuf_sg_alloc as symbolic
Defining function videobuf_next_field as symbolic
Defining function videobuf_read_one as symbolic
Defining function videobuf_read_stream as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to 'v4l2_video_std_frame_period' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_log_status' (function is undefined)
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Removed calls to 'snd_tea575x_set_freq' (function is undefined)
Defining function sprintf as symbolic
Defining function videobuf_streamon as symbolic
Defining function capable as symbolic
Defining function videobuf_dqbuf as symbolic
Defining function videobuf_qbuf as symbolic
Defining function videobuf_querybuf as symbolic
Defining function videobuf_reqbufs as symbolic
Defining function _copy_from_user as symbolic
Defining function videobuf_queue_is_busy as symbolic
Defining function strlcpy as symbolic
Defining function snd_tea575x_s_hw_freq_seek as symbolic
Defining function snd_tea575x_enum_freq_bands as symbolic
Defining function snd_tea575x_g_tuner as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'video_unregister_device' (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 'iounmap' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'i2c_del_adapter' (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
Removed calls to 'list_del' (function is undefined)
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'rc_unregister_device' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function flush_work as symbolic
Defining function __request_module as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function __request_region as symbolic
Defining function v4l2_device_register as symbolic
Defining function v4l2_ctrl_handler_init_class 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)
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_new_custom as symbolic
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'tveeprom_hauppauge_analog' (function is undefined)
Defining function v4l2_ctrl_radio_filter as symbolic
Defining function v4l2_ctrl_add_handler as symbolic
Removed calls to 'put_device' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'rc_free_device' (function is undefined)
Defining function rc_allocate_device as symbolic
Defining function rc_register_device as symbolic
Removed calls to 'rc_keydown_notimeout' (function is undefined)
Removed calls to 'rc_keyup' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to 'rc_keydown' (function is undefined)
Defining function i2c_new_device as symbolic
Defining function i2c_new_probed_device as symbolic
Defining function i2c_master_recv as symbolic
Defining function queue_work_on as symbolic
Defining function dev_set_name as symbolic
Defining function device_register as symbolic
Defining function device_create_file as symbolic
Defining function __video_register_device as symbolic
Defining function v4l2_i2c_tuner_addrs as symbolic
Defining function v4l2_i2c_new_subdev as symbolic
Defining function i2c_master_send as symbolic
Defining function ip_compute_csum as symbolic
Defining function snd_tea575x_hw_init as symbolic
Defining function tveeprom_read as symbolic
Defining function i2c_add_adapter as symbolic
Defining function i2c_bit_add_bus as symbolic
Defining function request_firmware as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function request_threaded_irq as symbolic
Defining function ioremap_nocache as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dma_set_mask as symbolic
Removed calls to '__might_sleep' (function is undefined)
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 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'bus_unregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_suspend_late_11 as symbolic
Defining function ldv_resume_early_11 as symbolic
Defining function ldv_shutdown_11 as symbolic
Defining function bus_register as symbolic
Defining function __pci_register_driver as symbolic
Defining function pci_get_device as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  strlen
  strncmp
  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.25468301773
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 897 511 2898 24334
INFO: Starting verification
KLEE: WARNING ONCE: function "avermedia_tvphone_audio" has inline asm
KLEE: WARNING ONCE: function "avermedia_tv_stereo_audio" has inline asm
KLEE: WARNING ONCE: function "winview_volume" has inline asm
KLEE: WARNING ONCE: function "terratv_audio" has inline asm
KLEE: WARNING ONCE: function "PXC200_muxsel" has inline asm
KLEE: WARNING ONCE: function "winfast2000_audio" has inline asm
KLEE: WARNING ONCE: function "gvbctv3pci_audio" has inline asm
KLEE: WARNING ONCE: function "fv2000s_audio" has inline asm
KLEE: WARNING ONCE: function "pvbt878p9b_audio" has inline asm
KLEE: WARNING ONCE: function "rv605_muxsel" has inline asm
KLEE: WARNING ONCE: function "windvr_audio" has inline asm
KLEE: WARNING ONCE: function "gvbctv5pci_audio" has inline asm
KLEE: WARNING ONCE: function "eagle_muxsel" has inline asm
KLEE: WARNING ONCE: function "adtvk503_audio" has inline asm
KLEE: WARNING ONCE: function "xguard_muxsel" has inline asm
KLEE: WARNING ONCE: function "phytec_muxsel" has inline asm
KLEE: WARNING ONCE: function "gvc1100_muxsel" has inline asm
KLEE: WARNING ONCE: function "picolo_tetra_muxsel" has inline asm
KLEE: WARNING ONCE: function "sigmaSQ_muxsel" has inline asm
KLEE: WARNING ONCE: function "sigmaSLC_muxsel" has inline asm
KLEE: WARNING ONCE: function "tibetCS16_muxsel" has inline asm
KLEE: WARNING ONCE: function "geovision_muxsel" has inline asm
KLEE: WARNING ONCE: function "td3116_latch_value" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_enable" has inline asm
KLEE: WARNING ONCE: function "bttv_read_gpio" has inline asm
KLEE: WARNING ONCE: function "bttv_write_gpio" has inline asm
KLEE: WARNING ONCE: function "bttv_dma_free" has inline asm
KLEE: WARNING ONCE: function "bttv_set_dma" has inline asm
KLEE: WARNING ONCE: function "bttv_risc_packed" has inline asm
KLEE: WARNING ONCE: function "bttv_s_ctrl" has inline asm
KLEE: WARNING ONCE: function "bt848_sat" has inline asm
KLEE: WARNING ONCE: function "audio_mux_gpio" has inline asm
KLEE: WARNING ONCE: function "bttv_tda9880_setnorm" has inline asm
KLEE: WARNING ONCE: function "bttv_read" has inline asm
KLEE: WARNING ONCE: function "bttv_field_count" has inline asm
KLEE: WARNING ONCE: function "disclaim_video_lines" has inline asm
KLEE: WARNING ONCE: function "set_tvnorm" has inline asm
KLEE: WARNING ONCE: function "bttv_vbi_fmt_reset" has inline asm
KLEE: WARNING ONCE: function "video_mux" has inline asm
KLEE: WARNING ONCE: function "set_pll" has inline asm
KLEE: WARNING ONCE: function "bttv_queue" has inline asm
KLEE: WARNING ONCE: function "init_bt848" has inline asm
KLEE: WARNING ONCE: function "init_irqreg" has inline asm
KLEE: WARNING ONCE: function "bttv_s_fmt_vid_cap" has inline asm
KLEE: WARNING ONCE: function "bttv_s_fmt_vid_overlay" has inline asm
KLEE: WARNING ONCE: function "bttv_qbuf" has inline asm
KLEE: WARNING ONCE: function "bttv_streamon" has inline asm
KLEE: WARNING ONCE: function "bttv_streamoff" has inline asm
KLEE: WARNING ONCE: function "bttv_querystd" has inline asm
KLEE: WARNING ONCE: function "bttv_enum_input" has inline asm
KLEE: WARNING ONCE: function "bttv_g_tuner" has inline asm
KLEE: WARNING ONCE: function "bttv_g_register" has inline asm
KLEE: WARNING ONCE: function "bttv_s_register" has inline asm
KLEE: WARNING ONCE: function "limit_scaled_size_lock" has inline asm
KLEE: WARNING ONCE: function "bttv_overlay_risc" has inline asm
KLEE: WARNING ONCE: function "bttv_risc_overlay" has inline asm
KLEE: WARNING ONCE: function "try_fmt" has inline asm
KLEE: WARNING ONCE: function "verify_window_lock" has inline asm
KLEE: WARNING ONCE: function "bttv_probe" has inline asm
KLEE: WARNING ONCE: function "bttv_remove" has inline asm
KLEE: WARNING ONCE: function "bttv_suspend" has inline asm
KLEE: WARNING ONCE: function "bttv_resume" has inline asm
KLEE: WARNING ONCE: function "bttv_buffer_activate_video" has inline asm
KLEE: WARNING ONCE: function "bttv_buffer_activate_vbi" has inline asm
KLEE: WARNING ONCE: function "bttv_apply_geo" has inline asm
KLEE: WARNING ONCE: function "bttv_ir_stop" has inline asm
KLEE: WARNING ONCE: function "bttv_irq_timeout" has inline asm
KLEE: WARNING ONCE: function "bttv_irq" has inline asm
KLEE: WARNING ONCE: function "bttv_init_card1" has inline asm
KLEE: WARNING ONCE: function "init_bttv_i2c" has inline asm
KLEE: WARNING ONCE: function "bttv_init_card2" has inline asm
KLEE: WARNING ONCE: function "vdev_init" has inline asm
KLEE: WARNING ONCE: function "bttv_input_init" has inline asm
KLEE: WARNING ONCE: function "bttv_input_timer" has inline asm
KLEE: WARNING ONCE: function "ir_handle_key" has inline asm
KLEE: WARNING ONCE: function "lt9415_audio" has inline asm
KLEE: WARNING ONCE: function "kodicom4400r_write" has inline asm
KLEE: WARNING ONCE: function "gv800s_write" has inline asm
KLEE: WARNING ONCE: function "boot_msp34xx" has inline asm
KLEE: WARNING ONCE: function "bttv_input_irq" has inline asm
KLEE: WARNING ONCE: function "bttv_buffer_risc" has inline asm
KLEE: WARNING ONCE: function "bttv_risc_planar" has inline asm
KLEE: WARNING ONCE: function "bttv_tea575x_set_pins" has inline asm
KLEE: WARNING ONCE: function "bttv_tea575x_get_pins" has inline asm
KLEE: WARNING ONCE: function "bttv_tea575x_set_direction" has inline asm
KLEE: WARNING ONCE: function "bttv_i2c_xfer" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_setsda" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_setscl" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_getsda" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_getscl" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_bits" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_inout" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_tracking" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_read" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_write" has inline asm
KLEE: WARNING ONCE: function "main" 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-P_kpn6/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "avermedia_tvphone_audio" has inline asm
KLEE: WARNING ONCE: function "avermedia_tv_stereo_audio" has inline asm
KLEE: WARNING ONCE: function "winview_volume" has inline asm
KLEE: WARNING ONCE: function "terratv_audio" has inline asm
KLEE: WARNING ONCE: function "PXC200_muxsel" has inline asm
KLEE: WARNING ONCE: function "winfast2000_audio" has inline asm
KLEE: WARNING ONCE: function "gvbctv3pci_audio" has inline asm
KLEE: WARNING ONCE: function "fv2000s_audio" has inline asm
KLEE: WARNING ONCE: function "pvbt878p9b_audio" has inline asm
KLEE: WARNING ONCE: function "rv605_muxsel" has inline asm
KLEE: WARNING ONCE: function "windvr_audio" has inline asm
KLEE: WARNING ONCE: function "gvbctv5pci_audio" has inline asm
KLEE: WARNING ONCE: function "eagle_muxsel" has inline asm
KLEE: WARNING ONCE: function "adtvk503_audio" has inline asm
KLEE: WARNING ONCE: function "xguard_muxsel" has inline asm
KLEE: WARNING ONCE: function "phytec_muxsel" has inline asm
KLEE: WARNING ONCE: function "gvc1100_muxsel" has inline asm
KLEE: WARNING ONCE: function "picolo_tetra_muxsel" has inline asm
KLEE: WARNING ONCE: function "sigmaSQ_muxsel" has inline asm
KLEE: WARNING ONCE: function "sigmaSLC_muxsel" has inline asm
KLEE: WARNING ONCE: function "tibetCS16_muxsel" has inline asm
KLEE: WARNING ONCE: function "geovision_muxsel" has inline asm
KLEE: WARNING ONCE: function "td3116_latch_value" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_enable" has inline asm
KLEE: WARNING ONCE: function "bttv_read_gpio" has inline asm
KLEE: WARNING ONCE: function "bttv_write_gpio" has inline asm
KLEE: WARNING ONCE: function "bttv_dma_free" has inline asm
KLEE: WARNING ONCE: function "bttv_set_dma" has inline asm
KLEE: WARNING ONCE: function "bttv_risc_packed" has inline asm
KLEE: WARNING ONCE: function "bttv_s_ctrl" has inline asm
KLEE: WARNING ONCE: function "bt848_sat" has inline asm
KLEE: WARNING ONCE: function "audio_mux_gpio" has inline asm
KLEE: WARNING ONCE: function "bttv_tda9880_setnorm" has inline asm
KLEE: WARNING ONCE: function "bttv_read" has inline asm
KLEE: WARNING ONCE: function "bttv_field_count" has inline asm
KLEE: WARNING ONCE: function "disclaim_video_lines" has inline asm
KLEE: WARNING ONCE: function "set_tvnorm" has inline asm
KLEE: WARNING ONCE: function "bttv_vbi_fmt_reset" has inline asm
KLEE: WARNING ONCE: function "video_mux" has inline asm
KLEE: WARNING ONCE: function "set_pll" has inline asm
KLEE: WARNING ONCE: function "bttv_queue" has inline asm
KLEE: WARNING ONCE: function "init_bt848" has inline asm
KLEE: WARNING ONCE: function "init_irqreg" has inline asm
KLEE: WARNING ONCE: function "bttv_s_fmt_vid_cap" has inline asm
KLEE: WARNING ONCE: function "bttv_s_fmt_vid_overlay" has inline asm
KLEE: WARNING ONCE: function "bttv_qbuf" has inline asm
KLEE: WARNING ONCE: function "bttv_streamon" has inline asm
KLEE: WARNING ONCE: function "bttv_streamoff" has inline asm
KLEE: WARNING ONCE: function "bttv_querystd" has inline asm
KLEE: WARNING ONCE: function "bttv_enum_input" has inline asm
KLEE: WARNING ONCE: function "bttv_g_tuner" has inline asm
KLEE: WARNING ONCE: function "bttv_g_register" has inline asm
KLEE: WARNING ONCE: function "bttv_s_register" has inline asm
KLEE: WARNING ONCE: function "limit_scaled_size_lock" has inline asm
KLEE: WARNING ONCE: function "bttv_overlay_risc" has inline asm
KLEE: WARNING ONCE: function "bttv_risc_overlay" has inline asm
KLEE: WARNING ONCE: function "try_fmt" has inline asm
KLEE: WARNING ONCE: function "verify_window_lock" has inline asm
KLEE: WARNING ONCE: function "bttv_probe" has inline asm
KLEE: WARNING ONCE: function "bttv_remove" has inline asm
KLEE: WARNING ONCE: function "bttv_suspend" has inline asm
KLEE: WARNING ONCE: function "bttv_resume" has inline asm
KLEE: WARNING ONCE: function "bttv_buffer_activate_video" has inline asm
KLEE: WARNING ONCE: function "bttv_buffer_activate_vbi" has inline asm
KLEE: WARNING ONCE: function "bttv_apply_geo" has inline asm
KLEE: WARNING ONCE: function "bttv_ir_stop" has inline asm
KLEE: WARNING ONCE: function "bttv_irq_timeout" has inline asm
KLEE: WARNING ONCE: function "bttv_irq" has inline asm
KLEE: WARNING ONCE: function "bttv_init_card1" has inline asm
KLEE: WARNING ONCE: function "init_bttv_i2c" has inline asm
KLEE: WARNING ONCE: function "bttv_init_card2" has inline asm
KLEE: WARNING ONCE: function "vdev_init" has inline asm
KLEE: WARNING ONCE: function "bttv_input_init" has inline asm
KLEE: WARNING ONCE: function "bttv_input_timer" has inline asm
KLEE: WARNING ONCE: function "ir_handle_key" has inline asm
KLEE: WARNING ONCE: function "lt9415_audio" has inline asm
KLEE: WARNING ONCE: function "kodicom4400r_write" has inline asm
KLEE: WARNING ONCE: function "gv800s_write" has inline asm
KLEE: WARNING ONCE: function "boot_msp34xx" has inline asm
KLEE: WARNING ONCE: function "bttv_input_irq" has inline asm
KLEE: WARNING ONCE: function "bttv_buffer_risc" has inline asm
KLEE: WARNING ONCE: function "bttv_risc_planar" has inline asm
KLEE: WARNING ONCE: function "bttv_tea575x_set_pins" has inline asm
KLEE: WARNING ONCE: function "bttv_tea575x_get_pins" has inline asm
KLEE: WARNING ONCE: function "bttv_tea575x_set_direction" has inline asm
KLEE: WARNING ONCE: function "bttv_i2c_xfer" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_setsda" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_setscl" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_getsda" has inline asm
KLEE: WARNING ONCE: function "bttv_bit_getscl" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_bits" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_inout" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_tracking" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_read" has inline asm
KLEE: WARNING ONCE: function "bttv_gpio_write" has inline asm
KLEE: WARNING ONCE: function "main" 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: 2.91294598579
