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--gpu--drm--drm.ko-entry_point_false-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.: 1671 1314 13678 93756
Removed infinite loop in sg_page
Removed infinite loop in drm_gem_object_free
Removed infinite loop in store_vblank
Removed infinite loop in drm_gem_private_object_init
Removed infinite loop in drm_mm_remove_node
Removed infinite loop in _drm_vma_offset_add_rb
Removed infinite loop in drm_mm_search_free_generic
Removed infinite loop in drm_mm_insert_helper
Removed infinite loop in drm_mm_hole_node_start
Removed infinite loop in drm_gem_get_pages
Removed infinite loop in drm_crtc_index
Removed infinite loop in arch_local_save_flags
Removed infinite loop in drm_vblank_enable
Removed infinite loop in drm_handle_vblank_events
Removed infinite loop in drm_mm_reserve_node
Removed infinite loop in drm_mm_search_free_in_range_generic
Removed infinite loop in drm_mm_insert_helper_range
Removed infinite loop in drm_mm_scan_add_block
Removed infinite loop in drm_mm_scan_remove_block
Removed infinite loop in drm_connector_index
Removed infinite loop in drm_plane_cleanup
Removed infinite loop in drm_plane_index
Removed infinite loop in drm_global_item_unref
Removed infinite loop in sg_page___0
Removed infinite loop in arch_local_save_flags___0
Removed infinite loop in dma_unmap_page
Removed infinite loop in wbinvd
Removed infinite loop in dma_map_page
Removed infinite loop in drm_mode_cursor_universal
Removed infinite loop in drm_stub_open
Removed infinite loop in get_page
Removed infinite loop in dma_map_sg_attrs
Removed infinite loop in dma_unmap_sg_attrs
Removed infinite loop in ldv_stop
Removed infinite loop in drm_global_release
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 3.28011989594
Removed calls to 'vfree' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function arch_phys_wc_add as symbolic
Defining function ioremap_wc as symbolic
Defining function vmalloc_user as symbolic
Defining function printk as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function __phys_addr as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'arch_phys_wc_del' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function krealloc as symbolic
Defining function capable as symbolic
Defining function wbinvd_on_all_cpus as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__sg_page_iter_start' (function is undefined)
Defining function __sg_page_iter_next as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'put_pid' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to 'iput' (function is undefined)
Removed calls to 'simple_release_fs' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'idr_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function idr_for_each as symbolic
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'dma_buf_put' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function idr_find_slowpath as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'device_del' (function is undefined)
Defining function idr_replace as symbolic
Removed calls to 'debugfs_remove' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'agp_free_memory' (function is undefined)
Removed calls to 'agp_backend_release' (function is undefined)
Defining function agp_unbind_memory as symbolic
Removed calls to 'free_irq' (function is undefined)
Defining function vga_client_register as symbolic
Defining function ktime_get as symbolic
Defining function ns_to_timeval as symbolic
Defining function ktime_get_with_offset as symbolic
Removed calls to 'ww_mutex_unlock' (function is undefined)
Defining function debug_locks_off as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'debug_check_no_locks_freed' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function __ww_mutex_lock as symbolic
Defining function __ww_mutex_lock_interruptible as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function mod_timer as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Defining function copy_user_enhanced_fast_string as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Defining function shmem_file_setup as symbolic
Removed calls to 'idr_preload' (function is undefined)
Defining function idr_alloc as symbolic
Removed calls to 'rb_insert_color' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'kvfree' (function is undefined)
Defining function shmem_read_mapping_page_gfp as symbolic
Defining function __vmalloc as symbolic
Removed calls to 'mark_page_accessed' (function is undefined)
Defining function set_page_dirty as symbolic
Removed calls to 'fput' (function is undefined)
Defining function lock_is_held as symbolic
Defining function vm_get_page_prot as symbolic
Defining function pgprot_writecombine as symbolic
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
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
Defining function request_threaded_irq as symbolic
Defining function ktime_mono_to_any as symbolic
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function schedule_timeout as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function vmalloc as symbolic
Defining function vmap as symbolic
Removed calls to 'vunmap' (function is undefined)
Defining function vzalloc as symbolic
Removed calls to 'device_initialize' (function is undefined)
Defining function dev_set_name as symbolic
Defining function simple_pin_fs as symbolic
Defining function alloc_anon_inode as symbolic
Defining function device_add as symbolic
Defining function sprintf as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function kvasprintf as symbolic
Defining function remap_pfn_range as symbolic
Defining function agp_backend_acquire as symbolic
Removed calls to 'agp_enable' (function is undefined)
Defining function agp_allocate_memory as symbolic
Defining function agp_bind_memory as symbolic
Defining function kasprintf as symbolic
Removed calls to 'pci_disable_device' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function agp_copy_info as symbolic
Defining function pci_find_capability as symbolic
Defining function pcie_capability_read_dword as symbolic
Defining function __pci_register_driver as symbolic
Defining function pci_dev_get as symbolic
Defining function pci_get_subsys as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function kobject_uevent_env as symbolic
Defining function device_register as symbolic
Defining function seq_printf as symbolic
Defining function snprintf as symbolic
Defining function kmemdup as symbolic
Defining function ida_simple_get as symbolic
Defining function fb_get_options as symbolic
Defining function simple_strtol as symbolic
Removed calls to 'ida_remove' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Defining function device_create_with_groups as symbolic
Defining function idr_get_next as symbolic
Defining function of_get_videomode as symbolic
Removed calls to 'list_sort' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Defining function memchr_inv as symbolic
Removed calls to 'dev_warn' (function is undefined)
Defining function i2c_transfer as symbolic
Defining function hdmi_avi_infoframe_init as symbolic
Defining function hdmi_vendor_infoframe_init as symbolic
Removed calls to 'i2c_unregister_device' (function is undefined)
Defining function __request_module as symbolic
Defining function i2c_new_device as symbolic
Defining function dma_buf_export as symbolic
Defining function dma_buf_fd as symbolic
Removed calls to 'dma_buf_unmap_attachment' (function is undefined)
Removed calls to 'dma_buf_detach' (function is undefined)
Defining function dma_buf_attach as symbolic
Defining function dma_buf_map_attachment as symbolic
Defining function dma_buf_get as symbolic
Defining function sg_alloc_table_from_pages as symbolic
Defining function sg_next as symbolic
Defining function queue_work_on as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function dma_set_mask as symbolic
Removed calls to 'of_node_put' (function is undefined)
Defining function of_graph_get_next_endpoint as symbolic
Defining function of_graph_get_remote_port as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'block_all_signals' (function is undefined)
Removed calls to 'unblock_all_signals' (function is undefined)
Defining function default_wake_function as symbolic
Defining function vmalloc_to_page as symbolic
Defining function vmalloc_32 as symbolic
Defining function send_sig as symbolic
Defining function vm_mmap as symbolic
Defining function sscanf as symbolic
Defining function kstrdup as symbolic
Defining function pid_vnr as symbolic
Defining function from_kuid_munged as symbolic
Defining function arch_phys_wc_index as symbolic
Defining function mount_pseudo as symbolic
Defining function simple_statfs as symbolic
Defining function simple_dname as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'dump_page' (function is undefined)
Defining function __get_page_tail as symbolic
Defining function show_class_attr_string as symbolic
Defining function sysfs_streq as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function pid_task as symbolic
Defining function seq_puts as symbolic
Defining function seq_write as symbolic
Defining function memdup_user as symbolic
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Removed calls to 'sg_free_table' (function is undefined)
Removed calls to 'debug_dma_map_sg' (function is undefined)
Defining function compat_alloc_user_space as symbolic
Defining function ___ratelimit as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'kill_anon_super' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'ida_destroy' (function is undefined)
Removed calls to 'ida_init' (function is undefined)
Removed calls to 'trace_seq_printf' (function is undefined)
Defining function ldv_release_30 as symbolic
Defining function trace_event_raw_init as symbolic
Defining function trace_event_reg as symbolic
Defining function trace_define_field as symbolic
Defining function trace_raw_output_prep as symbolic
Defining function ldv_release_15 as symbolic
Defining function ldv_probe_15 as symbolic
Defining function ldv_open_3 as symbolic
Defining function ldv_close_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function __class_create as symbolic
Defining function class_create_file_ns as symbolic
Defining function __register_chrdev as symbolic
Defining function ldv_suspend_late_25 as symbolic
Defining function ldv_resume_early_25 as symbolic
Defining function ldv_thaw_early_25 as symbolic
Defining function ldv_resume_noirq_25 as symbolic
Defining function ldv_freeze_noirq_25 as symbolic
Defining function ldv_prepare_25 as symbolic
Defining function ldv_freeze_late_25 as symbolic
Defining function ldv_thaw_noirq_25 as symbolic
Defining function ldv_thaw_25 as symbolic
Defining function ldv_suspend_noirq_25 as symbolic
Defining function ldv_complete_25 as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  strncmp
  strncpy
  __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: 2.72721505165
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1987 1094 7518 47882
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "drm_addmap_core" has inline asm
KLEE: WARNING ONCE: function "drm_pci_alloc" has inline asm
KLEE: WARNING ONCE: function "__drm_legacy_pci_free" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_addbufs_agp" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_addbufs_pci" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_pages" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_page" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_sg" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_virt_range" has inline asm
KLEE: WARNING ONCE: function "drm_open" has inline asm
KLEE: WARNING ONCE: function "kref_get___0" has inline asm
KLEE: WARNING ONCE: function "drm_master_put" has inline asm
KLEE: WARNING ONCE: function "drm_dev_unref" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference_unlocked" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_free" has inline asm
KLEE: WARNING ONCE: function "drm_release" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_lock_free" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_put" has inline asm
KLEE: WARNING ONCE: function "drm_sg_cleanup" has inline asm
KLEE: WARNING ONCE: function "store_vblank" has inline asm
KLEE: WARNING ONCE: function "drm_property_unreference_blob_locked" has inline asm
KLEE: WARNING ONCE: function "drm_framebuffer_unreference" has inline asm
KLEE: WARNING ONCE: function "kref_get___1" has inline asm
KLEE: WARNING ONCE: function "drm_modeset_acquire_init" has inline asm
KLEE: WARNING ONCE: function "drm_read" has inline asm
KLEE: WARNING ONCE: function "drm_gem_private_object_init" has inline asm
KLEE: WARNING ONCE: function "drm_gem_handle_create_tail" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_reference" has inline asm
KLEE: WARNING ONCE: function "drm_mm_remove_node" has inline asm
KLEE: WARNING ONCE: function "drm_vma_offset_add" has inline asm
KLEE: WARNING ONCE: function "drm_mm_insert_node_generic" has inline asm
KLEE: WARNING ONCE: function "drm_mm_hole_node_start" has inline asm
KLEE: WARNING ONCE: function "drm_gem_get_pages" has inline asm
KLEE: WARNING ONCE: function "drm_vm_open_locked" has inline asm
KLEE: WARNING ONCE: function "drm_gem_vm_close" has inline asm
KLEE: WARNING ONCE: function "drm_ioctl" has inline asm
KLEE: WARNING ONCE: function "drm_crtc_index" has inline asm
KLEE: WARNING ONCE: function "send_vblank_event" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_get" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_enable" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_off" has inline asm
KLEE: WARNING ONCE: function "drm_crtc_vblank_reset" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_on" has inline asm
KLEE: WARNING ONCE: function "drm_handle_vblank" has inline asm
KLEE: WARNING ONCE: function "drm_lock_take" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_idlelock_release" has inline asm
KLEE: WARNING ONCE: function "drm_minor_alloc" has inline asm
KLEE: WARNING ONCE: function "drm_mm_reserve_node" has inline asm
KLEE: WARNING ONCE: function "drm_mm_insert_node_in_range_generic" has inline asm
KLEE: WARNING ONCE: function "drm_mm_scan_add_block" has inline asm
KLEE: WARNING ONCE: function "drm_mm_scan_remove_block" has inline asm
KLEE: WARNING ONCE: function "drm_framebuffer_lookup" has inline asm
KLEE: WARNING ONCE: function "drm_mode_put_tile_group" has inline asm
KLEE: WARNING ONCE: function "drm_connector_index" has inline asm
KLEE: WARNING ONCE: function "drm_plane_cleanup" has inline asm
KLEE: WARNING ONCE: function "drm_plane_index" has inline asm
KLEE: WARNING ONCE: function "drm_property_create_bitmask" has inline asm
KLEE: WARNING ONCE: function "drm_property_unreference_blob" has inline asm
KLEE: WARNING ONCE: function "drm_property_lookup_blob" has inline asm
KLEE: WARNING ONCE: function "drm_rotation_simplify" has inline asm
KLEE: WARNING ONCE: function "drm_mode_get_tile_group" has inline asm
KLEE: WARNING ONCE: function "drm_global_item_unref" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference_unlocked___0" has inline asm
KLEE: WARNING ONCE: function "drm_gem_prime_handle_to_fd" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_reference___0" has inline asm
KLEE: WARNING ONCE: function "drm_prime_add_buf_handle" has inline asm
KLEE: WARNING ONCE: function "drm_gem_prime_import" has inline asm
KLEE: WARNING ONCE: function "drm_gem_prime_fd_to_handle" has inline asm
KLEE: WARNING ONCE: function "sg_page___0" has inline asm
KLEE: WARNING ONCE: function "drm_flip_work_queue" has inline asm
KLEE: WARNING ONCE: function "drm_ati_pcigart_init" has inline asm
KLEE: WARNING ONCE: function "drm_getclient" has inline asm
KLEE: WARNING ONCE: function "drm_gem_flink_ioctl" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_addbufs" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_markbufs" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_freebufs" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_switchctx" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_newctx" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_lock" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_unlock" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_sg_alloc" has inline asm
KLEE: WARNING ONCE: function "drm_wait_vblank" has inline asm
KLEE: WARNING ONCE: function "drm_mode_getresources" has inline asm
KLEE: WARNING ONCE: function "drm_mode_setcrtc" has inline asm
KLEE: WARNING ONCE: function "drm_mode_getconnector" has inline asm
KLEE: WARNING ONCE: function "drm_mode_getplane_res" has inline asm
KLEE: WARNING ONCE: function "drm_mode_atomic_ioctl" has inline asm
KLEE: WARNING ONCE: function "drm_mode_cursor_common" has inline asm
KLEE: WARNING ONCE: function "get_properties" has inline asm
KLEE: WARNING ONCE: function "get_page" has inline asm
KLEE: WARNING ONCE: function "drm_clients_info" has inline asm
KLEE: WARNING ONCE: function "drm_gem_map_detach" has inline asm
KLEE: WARNING ONCE: function "drm_gem_map_dma_buf" has inline asm
KLEE: WARNING ONCE: function "compat_drm_version" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getunique" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getmap" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getclient" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getstats" has inline asm
KLEE: WARNING ONCE: function "compat_drm_setunique" has inline asm
KLEE: WARNING ONCE: function "compat_drm_addmap" has inline asm
KLEE: WARNING ONCE: function "compat_drm_addbufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_markbufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_infobufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_mapbufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_freebufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_rmmap" has inline asm
KLEE: WARNING ONCE: function "compat_drm_setsareactx" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getsareactx" has inline asm
KLEE: WARNING ONCE: function "compat_drm_resctx" has inline asm
KLEE: WARNING ONCE: function "compat_drm_dma" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_enable" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_info" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_alloc" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_free" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_bind" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_unbind" has inline asm
KLEE: WARNING ONCE: function "compat_drm_sg_alloc" has inline asm
KLEE: WARNING ONCE: function "compat_drm_sg_free" has inline asm
KLEE: WARNING ONCE: function "compat_drm_wait_vblank" has inline asm
KLEE: WARNING ONCE: function "compat_drm_update_draw" has inline asm
KLEE: WARNING ONCE: function "drm_global_release" has inline asm
KLEE: WARNING: undefined reference to variable: agp_find_bridge
KLEE: WARNING: undefined reference to function: kill_anon_super
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(agp_find_bridge) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-f0Jekd/klee-out-0"
KLEE: Using STP solver backend
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "drm_addmap_core" has inline asm
KLEE: WARNING ONCE: function "drm_pci_alloc" has inline asm
KLEE: WARNING ONCE: function "__drm_legacy_pci_free" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_addbufs_agp" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_addbufs_pci" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_pages" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_page" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_sg" has inline asm
KLEE: WARNING ONCE: function "drm_clflush_virt_range" has inline asm
KLEE: WARNING ONCE: function "drm_open" has inline asm
KLEE: WARNING ONCE: function "kref_get___0" has inline asm
KLEE: WARNING ONCE: function "drm_master_put" has inline asm
KLEE: WARNING ONCE: function "drm_dev_unref" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference_unlocked" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_free" has inline asm
KLEE: WARNING ONCE: function "drm_release" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_lock_free" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_put" has inline asm
KLEE: WARNING ONCE: function "drm_sg_cleanup" has inline asm
KLEE: WARNING ONCE: function "store_vblank" has inline asm
KLEE: WARNING ONCE: function "drm_property_unreference_blob_locked" has inline asm
KLEE: WARNING ONCE: function "drm_framebuffer_unreference" has inline asm
KLEE: WARNING ONCE: function "kref_get___1" has inline asm
KLEE: WARNING ONCE: function "drm_modeset_acquire_init" has inline asm
KLEE: WARNING ONCE: function "drm_read" has inline asm
KLEE: WARNING ONCE: function "drm_gem_private_object_init" has inline asm
KLEE: WARNING ONCE: function "drm_gem_handle_create_tail" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_reference" has inline asm
KLEE: WARNING ONCE: function "drm_mm_remove_node" has inline asm
KLEE: WARNING ONCE: function "drm_vma_offset_add" has inline asm
KLEE: WARNING ONCE: function "drm_mm_insert_node_generic" has inline asm
KLEE: WARNING ONCE: function "drm_mm_hole_node_start" has inline asm
KLEE: WARNING ONCE: function "drm_gem_get_pages" has inline asm
KLEE: WARNING ONCE: function "drm_vm_open_locked" has inline asm
KLEE: WARNING ONCE: function "drm_gem_vm_close" has inline asm
KLEE: WARNING ONCE: function "drm_ioctl" has inline asm
KLEE: WARNING ONCE: function "drm_crtc_index" has inline asm
KLEE: WARNING ONCE: function "send_vblank_event" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_get" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_enable" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_off" has inline asm
KLEE: WARNING ONCE: function "drm_crtc_vblank_reset" has inline asm
KLEE: WARNING ONCE: function "drm_vblank_on" has inline asm
KLEE: WARNING ONCE: function "drm_handle_vblank" has inline asm
KLEE: WARNING ONCE: function "drm_lock_take" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_idlelock_release" has inline asm
KLEE: WARNING ONCE: function "drm_minor_alloc" has inline asm
KLEE: WARNING ONCE: function "drm_mm_reserve_node" has inline asm
KLEE: WARNING ONCE: function "drm_mm_insert_node_in_range_generic" has inline asm
KLEE: WARNING ONCE: function "drm_mm_scan_add_block" has inline asm
KLEE: WARNING ONCE: function "drm_mm_scan_remove_block" has inline asm
KLEE: WARNING ONCE: function "drm_framebuffer_lookup" has inline asm
KLEE: WARNING ONCE: function "drm_mode_put_tile_group" has inline asm
KLEE: WARNING ONCE: function "drm_connector_index" has inline asm
KLEE: WARNING ONCE: function "drm_plane_cleanup" has inline asm
KLEE: WARNING ONCE: function "drm_plane_index" has inline asm
KLEE: WARNING ONCE: function "drm_property_create_bitmask" has inline asm
KLEE: WARNING ONCE: function "drm_property_unreference_blob" has inline asm
KLEE: WARNING ONCE: function "drm_property_lookup_blob" has inline asm
KLEE: WARNING ONCE: function "drm_rotation_simplify" has inline asm
KLEE: WARNING ONCE: function "drm_mode_get_tile_group" has inline asm
KLEE: WARNING ONCE: function "drm_global_item_unref" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference_unlocked___0" has inline asm
KLEE: WARNING ONCE: function "drm_gem_prime_handle_to_fd" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_reference___0" has inline asm
KLEE: WARNING ONCE: function "drm_prime_add_buf_handle" has inline asm
KLEE: WARNING ONCE: function "drm_gem_prime_import" has inline asm
KLEE: WARNING ONCE: function "drm_gem_prime_fd_to_handle" has inline asm
KLEE: WARNING ONCE: function "sg_page___0" has inline asm
KLEE: WARNING ONCE: function "drm_flip_work_queue" has inline asm
KLEE: WARNING ONCE: function "drm_ati_pcigart_init" has inline asm
KLEE: WARNING ONCE: function "drm_getclient" has inline asm
KLEE: WARNING ONCE: function "drm_gem_flink_ioctl" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_addbufs" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_markbufs" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_freebufs" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_switchctx" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_newctx" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_lock" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_unlock" has inline asm
KLEE: WARNING ONCE: function "drm_legacy_sg_alloc" has inline asm
KLEE: WARNING ONCE: function "drm_wait_vblank" has inline asm
KLEE: WARNING ONCE: function "drm_mode_getresources" has inline asm
KLEE: WARNING ONCE: function "drm_mode_setcrtc" has inline asm
KLEE: WARNING ONCE: function "drm_mode_getconnector" has inline asm
KLEE: WARNING ONCE: function "drm_mode_getplane_res" has inline asm
KLEE: WARNING ONCE: function "drm_mode_atomic_ioctl" has inline asm
KLEE: WARNING ONCE: function "drm_mode_cursor_common" has inline asm
KLEE: WARNING ONCE: function "get_properties" has inline asm
KLEE: WARNING ONCE: function "get_page" has inline asm
KLEE: WARNING ONCE: function "drm_clients_info" has inline asm
KLEE: WARNING ONCE: function "drm_gem_map_detach" has inline asm
KLEE: WARNING ONCE: function "drm_gem_map_dma_buf" has inline asm
KLEE: WARNING ONCE: function "compat_drm_version" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getunique" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getmap" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getclient" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getstats" has inline asm
KLEE: WARNING ONCE: function "compat_drm_setunique" has inline asm
KLEE: WARNING ONCE: function "compat_drm_addmap" has inline asm
KLEE: WARNING ONCE: function "compat_drm_addbufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_markbufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_infobufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_mapbufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_freebufs" has inline asm
KLEE: WARNING ONCE: function "compat_drm_rmmap" has inline asm
KLEE: WARNING ONCE: function "compat_drm_setsareactx" has inline asm
KLEE: WARNING ONCE: function "compat_drm_getsareactx" has inline asm
KLEE: WARNING ONCE: function "compat_drm_resctx" has inline asm
KLEE: WARNING ONCE: function "compat_drm_dma" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_enable" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_info" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_alloc" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_free" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_bind" has inline asm
KLEE: WARNING ONCE: function "compat_drm_agp_unbind" has inline asm
KLEE: WARNING ONCE: function "compat_drm_sg_alloc" has inline asm
KLEE: WARNING ONCE: function "compat_drm_sg_free" has inline asm
KLEE: WARNING ONCE: function "compat_drm_wait_vblank" has inline asm
KLEE: WARNING ONCE: function "compat_drm_update_draw" has inline asm
KLEE: WARNING ONCE: function "drm_global_release" has inline asm
KLEE: WARNING: undefined reference to variable: agp_find_bridge
KLEE: WARNING: undefined reference to function: kill_anon_super
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(agp_find_bridge) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 6.8653011322
