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-32_7a-drivers--gpu--drm--amd--amdkfd--amdkfd.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.: 593 849 5657 43570
Removed infinite loop in kgd2kfd_suspend
Removed infinite loop in kgd2kfd_resume
Removed infinite loop in iommu_invalid_ppr_cb
Removed infinite loop in kfd_unbind_process_from_device
Removed infinite loop in pqm_uninit
Removed infinite loop in dbgdev_wave_control_set_registers
Removed infinite loop in pqm_destroy_queue
Removed infinite loop in get_queue_by_qid
Removed infinite loop in kernel_queue_uninit
Removed infinite loop in kfd_dbgmgr_uninitialize
Removed infinite loop in device_queue_manager_uninit
Removed infinite loop in kfd_topology_remove_device
Removed infinite loop in kfd_remove_sysfs_node_entry
Removed infinite loop in kfd_release_topology_device
Removed infinite loop in kfd_build_sysfs_node_entry
Removed infinite loop in kfd_gtt_sa_init
Removed infinite loop in kfd_doorbell_init
Removed infinite loop in kfd_topology_add_device
Removed infinite loop in device_queue_manager_init
Removed infinite loop in create_queue_cpsch
Removed infinite loop in initialize_cpsch
Removed infinite loop in start_cpsch
Removed infinite loop in stop_cpsch
Removed infinite loop in destroy_queue_cpsch
Removed infinite loop in update_queue
Removed infinite loop in get_mqd_manager_nocpsch
Removed infinite loop in register_process_nocpsch
Removed infinite loop in unregister_process_nocpsch
Removed infinite loop in uninitialize_nocpsch
Removed infinite loop in create_kernel_queue_cpsch
Removed infinite loop in destroy_kernel_queue_cpsch
Removed infinite loop in create_queue_nocpsch
Removed infinite loop in destroy_queue_nocpsch
Removed infinite loop in initialize_nocpsch
Removed infinite loop in register_process_cik
Removed infinite loop in get_first_pipe
Removed infinite loop in get_pipes_num
Removed infinite loop in init_pipelines
Removed infinite loop in kfd_gtt_sa_allocate
Removed infinite loop in kfd_gtt_sa_free
Removed infinite loop in compute_sh_mem_bases_64bit
Removed infinite loop in init_scheduler
Removed infinite loop in create_compute_queue_nocpsch
Removed infinite loop in init_interrupts
Removed infinite loop in destroy_queues_cpsch
Removed infinite loop in execute_queues_cpsch
Removed infinite loop in pm_send_runlist
Removed infinite loop in pm_create_runlist_ib
Removed infinite loop in pm_create_runlist
Removed infinite loop in pm_release_ib
Removed infinite loop in pm_allocate_runlist_ib
Removed infinite loop in pm_create_map_process
Removed infinite loop in inc_wptr
Removed infinite loop in pm_create_map_queue
Removed infinite loop in pm_calc_rlib_size
Removed infinite loop in pm_send_unmap_queue
Removed infinite loop in pm_send_query_status
Removed infinite loop in amdkfd_fence_wait_timeout
Removed infinite loop in mqd_manager_init_cik
Removed infinite loop in init_mqd
Removed infinite loop in uninit_mqd
Removed infinite loop in update_mqd
Removed infinite loop in init_mqd_hiq
Removed infinite loop in update_mqd_hiq
Removed infinite loop in init_mqd_sdma
Removed infinite loop in uninit_mqd_sdma
Removed infinite loop in update_mqd_sdma
Removed infinite loop in get_sdma_mqd
Removed infinite loop in pm_uninit
Removed infinite loop in pm_init
Removed infinite loop in set_sched_resources
Removed infinite loop in pm_send_set_resources
Removed infinite loop in kernel_queue_init
Removed infinite loop in initialize
Removed infinite loop in uninitialize
Removed infinite loop in acquire_packet_buffer
Removed infinite loop in submit_packet
Removed infinite loop in rollback_packet
Removed infinite loop in kfd_release_kernel_doorbell
Removed infinite loop in kfd_get_kernel_doorbell
Removed infinite loop in init_queue
Removed infinite loop in kfd_assign_gpu
Removed infinite loop in lookup_device_info
Removed infinite loop in kfd_create_process
Removed infinite loop in pqm_init
Removed infinite loop in kfd_pasid_free
Removed infinite loop in kfd_dbgmgr_wave_control
Removed infinite loop in kfd_dbgmgr_address_watch
Removed infinite loop in kfd_dbgmgr_unregister
Removed infinite loop in kfd_dbgmgr_create
Removed infinite loop in kfd_dbgmgr_register
Removed infinite loop in kfd_dbgdev_init
Removed infinite loop in dbgdev_register_nodiq
Removed infinite loop in dbgdev_unregister_nodiq
Removed infinite loop in dbgdev_wave_control_nodiq
Removed infinite loop in dbgdev_address_watch_nodiq
Removed infinite loop in dbgdev_register_diq
Removed infinite loop in dbgdev_unregister_diq
Removed infinite loop in dbgdev_wave_control_diq
Removed infinite loop in dbgdev_address_watch_diq
Removed infinite loop in dbgdev_address_watch_set_registers
Removed infinite loop in dbgdev_diq_submit_ib
Removed infinite loop in pqm_create_queue
Removed infinite loop in pqm_get_kernel_queue
Removed infinite loop in find_available_queue_slot
Removed infinite loop in dbgdev_address_watch_disable_nodiq
Removed infinite loop in pqm_update_queue
Removed infinite loop in kfd_process_notifier_release
Removed infinite loop in kfd_process_destroy_delayed
Removed infinite loop in ldv_stop
Removed infinite loop in kfd_parse_subtype
Removed infinite loop in kfd_parse_subtype_cu
Removed infinite loop in kfd_parse_subtype_mem
Removed infinite loop in kfd_parse_subtype_cache
Removed infinite loop in kfd_parse_subtype_iolink
Removed infinite loop in kfd_populated_cu_info_cpu
Removed infinite loop in kfd_populated_cu_info_gpu
INFO: Compilation, preparation and instrumentation time: 1.46134090424
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to '__srcu_read_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function send_sig as symbolic
Defining function wake_up_process as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function __srcu_read_lock as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'amd_iommu_free_device' (function is undefined)
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function kfd_get_pasid_limit as symbolic
Defining function amd_iommu_init_device as symbolic
Defining function amd_iommu_set_invalidate_ctx_cb as symbolic
Defining function amd_iommu_set_invalid_ppr_cb as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function find_vma as symbolic
Defining function printk as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function queue_work_on as symbolic
Defining function ___ratelimit as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'sysfs_remove_file_ns' (function is undefined)
Removed calls to 'kobject_del' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Defining function kobject_init_and_add as symbolic
Defining function kobject_create_and_add as symbolic
Defining function sysfs_create_file_ns as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function find_next_zero_bit as symbolic
Defining function find_first_bit as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function amd_iommu_bind_pasid as symbolic
Removed calls to 'write_kernel_doorbell' (function is undefined)
Defining function find_first_zero_bit as symbolic
Defining function amd_iommu_device_info as symbolic
Defining function find_next_bit as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'mmu_notifier_unregister_no_release' (function is undefined)
Defining function __mmu_notifier_register as symbolic
Defining function __phys_addr as symbolic
Defining function remap_pfn_range as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'getrawmonotonic64' (function is undefined)
Defining function schedule_timeout_interruptible as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function __get_free_pages as symbolic
Defining function ns_to_timespec as symbolic
Defining function ktime_get_with_offset as symbolic
Defining function snprintf as symbolic
Defining function cpufreq_quick_get_max as symbolic
Removed calls to 'synchronize_srcu' (function is undefined)
Removed calls to 'mmu_notifier_call_srcu' (function is undefined)
Removed calls to '__mmdrop' (function is undefined)
Removed calls to 'amd_iommu_unbind_pasid' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'process_srcu' (function is undefined)
Removed calls to 'delayed_work_timer_fn' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function acpi_get_table as symbolic
Defining function acpi_format_exception as symbolic
Defining function __class_create as symbolic
Defining function device_create as symbolic
Defining function __register_chrdev as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function ldv_probe_4 as symbolic
Defining function ldv_release_11 as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __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.36459112167
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 692 741 3241 25128
INFO: Starting verification
KLEE: WARNING ONCE: function "kgd2kfd_device_init" has inline asm
KLEE: WARNING ONCE: function "kgd2kfd_suspend" has inline asm
KLEE: WARNING ONCE: function "kgd2kfd_resume" has inline asm
KLEE: WARNING ONCE: function "iommu_invalid_ppr_cb" has inline asm
KLEE: WARNING ONCE: function "kfd_unbind_process_from_device" has inline asm
KLEE: WARNING ONCE: function "pqm_uninit" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_reset_wavefronts" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_control_set_registers" has inline asm
KLEE: WARNING ONCE: function "pqm_destroy_queue" has inline asm
KLEE: WARNING ONCE: function "get_queue_by_qid" has inline asm
KLEE: WARNING ONCE: function "kernel_queue_uninit" has inline asm
KLEE: WARNING ONCE: function "device_queue_manager_uninit" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_remove_device" has inline asm
KLEE: WARNING ONCE: function "kfd_remove_sysfs_node_entry" has inline asm
KLEE: WARNING ONCE: function "kfd_release_topology_device" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_update_sysfs" has inline asm
KLEE: WARNING ONCE: function "interrupt_wq" has inline asm
KLEE: WARNING ONCE: function "kfd_doorbell_init" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_add_device" has inline asm
KLEE: WARNING ONCE: function "device_queue_manager_init" has inline asm
KLEE: WARNING ONCE: function "create_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "initialize_cpsch" has inline asm
KLEE: WARNING ONCE: function "start_cpsch" has inline asm
KLEE: WARNING ONCE: function "stop_cpsch" has inline asm
KLEE: WARNING ONCE: function "destroy_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "update_queue" has inline asm
KLEE: WARNING ONCE: function "get_mqd_manager_nocpsch" has inline asm
KLEE: WARNING ONCE: function "register_process_nocpsch" has inline asm
KLEE: WARNING ONCE: function "unregister_process_nocpsch" has inline asm
KLEE: WARNING ONCE: function "uninitialize_nocpsch" has inline asm
KLEE: WARNING ONCE: function "create_kernel_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "destroy_kernel_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "create_queue_nocpsch" has inline asm
KLEE: WARNING ONCE: function "destroy_queue_nocpsch" has inline asm
KLEE: WARNING ONCE: function "initialize_nocpsch" has inline asm
KLEE: WARNING ONCE: function "register_process_cik" has inline asm
KLEE: WARNING ONCE: function "get_first_pipe" has inline asm
KLEE: WARNING ONCE: function "get_pipes_num" has inline asm
KLEE: WARNING ONCE: function "init_pipelines" has inline asm
KLEE: WARNING ONCE: function "kfd_gtt_sa_allocate" has inline asm
KLEE: WARNING ONCE: function "kfd_gtt_sa_free" has inline asm
KLEE: WARNING ONCE: function "init_interrupts" has inline asm
KLEE: WARNING ONCE: function "destroy_queues_cpsch" has inline asm
KLEE: WARNING ONCE: function "execute_queues_cpsch" has inline asm
KLEE: WARNING ONCE: function "pm_send_runlist" has inline asm
KLEE: WARNING ONCE: function "pm_release_ib" has inline asm
KLEE: WARNING ONCE: function "pm_create_map_queue" has inline asm
KLEE: WARNING ONCE: function "pm_create_runlist" has inline asm
KLEE: WARNING ONCE: function "pm_send_unmap_queue" has inline asm
KLEE: WARNING ONCE: function "pm_send_query_status" has inline asm
KLEE: WARNING ONCE: function "amdkfd_fence_wait_timeout" has inline asm
KLEE: WARNING ONCE: function "mqd_manager_init_cik" has inline asm
KLEE: WARNING ONCE: function "init_mqd" has inline asm
KLEE: WARNING ONCE: function "uninit_mqd" has inline asm
KLEE: WARNING ONCE: function "update_mqd" has inline asm
KLEE: WARNING ONCE: function "init_mqd_hiq" has inline asm
KLEE: WARNING ONCE: function "update_mqd_hiq" has inline asm
KLEE: WARNING ONCE: function "init_mqd_sdma" has inline asm
KLEE: WARNING ONCE: function "uninit_mqd_sdma" has inline asm
KLEE: WARNING ONCE: function "update_mqd_sdma" has inline asm
KLEE: WARNING ONCE: function "pm_uninit" has inline asm
KLEE: WARNING ONCE: function "pm_init" has inline asm
KLEE: WARNING ONCE: function "pm_send_set_resources" has inline asm
KLEE: WARNING ONCE: function "kernel_queue_init" has inline asm
KLEE: WARNING ONCE: function "initialize" has inline asm
KLEE: WARNING ONCE: function "uninitialize" has inline asm
KLEE: WARNING ONCE: function "acquire_packet_buffer" has inline asm
KLEE: WARNING ONCE: function "submit_packet" has inline asm
KLEE: WARNING ONCE: function "rollback_packet" has inline asm
KLEE: WARNING ONCE: function "kfd_release_kernel_doorbell" has inline asm
KLEE: WARNING ONCE: function "kfd_get_kernel_doorbell" has inline asm
KLEE: WARNING ONCE: function "kfd_ioctl" has inline asm
KLEE: WARNING ONCE: function "kfd_mmap" has inline asm
KLEE: WARNING ONCE: function "kfd_open" has inline asm
KLEE: WARNING ONCE: function "is_compat_task" has inline asm
KLEE: WARNING ONCE: function "kfd_create_process" has inline asm
KLEE: WARNING ONCE: function "kfd_pasid_alloc" has inline asm
KLEE: WARNING ONCE: function "pqm_init" has inline asm
KLEE: WARNING ONCE: function "kfd_pasid_free" has inline asm
KLEE: WARNING ONCE: function "kfd_event_mmap" has inline asm
KLEE: WARNING ONCE: function "kfd_ioctl_create_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_ioctl_update_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_wave_control" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_address_watch" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_unregister" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_create" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_register" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgdev_init" has inline asm
KLEE: WARNING ONCE: function "dbgdev_register_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_register_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_unregister_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_unregister_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_control_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_control_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_address_watch_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_address_watch_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_address_watch_set_registers" has inline asm
KLEE: WARNING ONCE: function "dbgdev_diq_submit_ib" has inline asm
KLEE: WARNING ONCE: function "pqm_create_queue" has inline asm
KLEE: WARNING ONCE: function "pqm_get_kernel_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_wait_on_events" has inline asm
KLEE: WARNING ONCE: function "destroy_event" has inline asm
KLEE: WARNING ONCE: function "allocate_free_slot" has inline asm
KLEE: WARNING ONCE: function "pqm_update_queue" has inline asm
KLEE: WARNING ONCE: function "node_show" has inline asm
KLEE: WARNING ONCE: function "kfd_process_notifier_release" has inline asm
KLEE: WARNING ONCE: function "get_sdma_mqd" has inline asm
KLEE: WARNING ONCE: function "init_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_pasid_init" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_init" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: process_srcu
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-EjAb9K/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "kgd2kfd_device_init" has inline asm
KLEE: WARNING ONCE: function "kgd2kfd_suspend" has inline asm
KLEE: WARNING ONCE: function "kgd2kfd_resume" has inline asm
KLEE: WARNING ONCE: function "iommu_invalid_ppr_cb" has inline asm
KLEE: WARNING ONCE: function "kfd_unbind_process_from_device" has inline asm
KLEE: WARNING ONCE: function "pqm_uninit" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_reset_wavefronts" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_control_set_registers" has inline asm
KLEE: WARNING ONCE: function "pqm_destroy_queue" has inline asm
KLEE: WARNING ONCE: function "get_queue_by_qid" has inline asm
KLEE: WARNING ONCE: function "kernel_queue_uninit" has inline asm
KLEE: WARNING ONCE: function "device_queue_manager_uninit" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_remove_device" has inline asm
KLEE: WARNING ONCE: function "kfd_remove_sysfs_node_entry" has inline asm
KLEE: WARNING ONCE: function "kfd_release_topology_device" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_update_sysfs" has inline asm
KLEE: WARNING ONCE: function "interrupt_wq" has inline asm
KLEE: WARNING ONCE: function "kfd_doorbell_init" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_add_device" has inline asm
KLEE: WARNING ONCE: function "device_queue_manager_init" has inline asm
KLEE: WARNING ONCE: function "create_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "initialize_cpsch" has inline asm
KLEE: WARNING ONCE: function "start_cpsch" has inline asm
KLEE: WARNING ONCE: function "stop_cpsch" has inline asm
KLEE: WARNING ONCE: function "destroy_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "update_queue" has inline asm
KLEE: WARNING ONCE: function "get_mqd_manager_nocpsch" has inline asm
KLEE: WARNING ONCE: function "register_process_nocpsch" has inline asm
KLEE: WARNING ONCE: function "unregister_process_nocpsch" has inline asm
KLEE: WARNING ONCE: function "uninitialize_nocpsch" has inline asm
KLEE: WARNING ONCE: function "create_kernel_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "destroy_kernel_queue_cpsch" has inline asm
KLEE: WARNING ONCE: function "create_queue_nocpsch" has inline asm
KLEE: WARNING ONCE: function "destroy_queue_nocpsch" has inline asm
KLEE: WARNING ONCE: function "initialize_nocpsch" has inline asm
KLEE: WARNING ONCE: function "register_process_cik" has inline asm
KLEE: WARNING ONCE: function "get_first_pipe" has inline asm
KLEE: WARNING ONCE: function "get_pipes_num" has inline asm
KLEE: WARNING ONCE: function "init_pipelines" has inline asm
KLEE: WARNING ONCE: function "kfd_gtt_sa_allocate" has inline asm
KLEE: WARNING ONCE: function "kfd_gtt_sa_free" has inline asm
KLEE: WARNING ONCE: function "init_interrupts" has inline asm
KLEE: WARNING ONCE: function "destroy_queues_cpsch" has inline asm
KLEE: WARNING ONCE: function "execute_queues_cpsch" has inline asm
KLEE: WARNING ONCE: function "pm_send_runlist" has inline asm
KLEE: WARNING ONCE: function "pm_release_ib" has inline asm
KLEE: WARNING ONCE: function "pm_create_map_queue" has inline asm
KLEE: WARNING ONCE: function "pm_create_runlist" has inline asm
KLEE: WARNING ONCE: function "pm_send_unmap_queue" has inline asm
KLEE: WARNING ONCE: function "pm_send_query_status" has inline asm
KLEE: WARNING ONCE: function "amdkfd_fence_wait_timeout" has inline asm
KLEE: WARNING ONCE: function "mqd_manager_init_cik" has inline asm
KLEE: WARNING ONCE: function "init_mqd" has inline asm
KLEE: WARNING ONCE: function "uninit_mqd" has inline asm
KLEE: WARNING ONCE: function "update_mqd" has inline asm
KLEE: WARNING ONCE: function "init_mqd_hiq" has inline asm
KLEE: WARNING ONCE: function "update_mqd_hiq" has inline asm
KLEE: WARNING ONCE: function "init_mqd_sdma" has inline asm
KLEE: WARNING ONCE: function "uninit_mqd_sdma" has inline asm
KLEE: WARNING ONCE: function "update_mqd_sdma" has inline asm
KLEE: WARNING ONCE: function "pm_uninit" has inline asm
KLEE: WARNING ONCE: function "pm_init" has inline asm
KLEE: WARNING ONCE: function "pm_send_set_resources" has inline asm
KLEE: WARNING ONCE: function "kernel_queue_init" has inline asm
KLEE: WARNING ONCE: function "initialize" has inline asm
KLEE: WARNING ONCE: function "uninitialize" has inline asm
KLEE: WARNING ONCE: function "acquire_packet_buffer" has inline asm
KLEE: WARNING ONCE: function "submit_packet" has inline asm
KLEE: WARNING ONCE: function "rollback_packet" has inline asm
KLEE: WARNING ONCE: function "kfd_release_kernel_doorbell" has inline asm
KLEE: WARNING ONCE: function "kfd_get_kernel_doorbell" has inline asm
KLEE: WARNING ONCE: function "kfd_ioctl" has inline asm
KLEE: WARNING ONCE: function "kfd_mmap" has inline asm
KLEE: WARNING ONCE: function "kfd_open" has inline asm
KLEE: WARNING ONCE: function "is_compat_task" has inline asm
KLEE: WARNING ONCE: function "kfd_create_process" has inline asm
KLEE: WARNING ONCE: function "kfd_pasid_alloc" has inline asm
KLEE: WARNING ONCE: function "pqm_init" has inline asm
KLEE: WARNING ONCE: function "kfd_pasid_free" has inline asm
KLEE: WARNING ONCE: function "kfd_event_mmap" has inline asm
KLEE: WARNING ONCE: function "kfd_ioctl_create_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_ioctl_update_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_wave_control" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_address_watch" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_unregister" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_create" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgmgr_register" has inline asm
KLEE: WARNING ONCE: function "kfd_dbgdev_init" has inline asm
KLEE: WARNING ONCE: function "dbgdev_register_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_register_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_unregister_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_unregister_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_control_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_wave_control_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_address_watch_nodiq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_address_watch_diq" has inline asm
KLEE: WARNING ONCE: function "dbgdev_address_watch_set_registers" has inline asm
KLEE: WARNING ONCE: function "dbgdev_diq_submit_ib" has inline asm
KLEE: WARNING ONCE: function "pqm_create_queue" has inline asm
KLEE: WARNING ONCE: function "pqm_get_kernel_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_wait_on_events" has inline asm
KLEE: WARNING ONCE: function "destroy_event" has inline asm
KLEE: WARNING ONCE: function "allocate_free_slot" has inline asm
KLEE: WARNING ONCE: function "pqm_update_queue" has inline asm
KLEE: WARNING ONCE: function "node_show" has inline asm
KLEE: WARNING ONCE: function "kfd_process_notifier_release" has inline asm
KLEE: WARNING ONCE: function "get_sdma_mqd" has inline asm
KLEE: WARNING ONCE: function "init_queue" has inline asm
KLEE: WARNING ONCE: function "kfd_pasid_init" has inline asm
KLEE: WARNING ONCE: function "kfd_topology_init" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: process_srcu
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 3.23833703995
