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--qxl--qxl.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.: 349 882 4737 31949
Removed infinite loop in qxl_gem_object_create_with_handle
Removed infinite loop in arch_local_save_flags___0
Removed infinite loop in arch_local_save_flags
Removed infinite loop in qxl_mode_dumb_mmap
Removed infinite loop in qxl_send_monitors_config
Removed infinite loop in qxl_write_monitors_config_for_encoder
Removed infinite loop in qxl_move_null
Removed infinite loop in qxlfb_create
Removed infinite loop in ldv_stop
Removed infinite loop in qxl_get_handle_for_primary_fb
INFO: Compilation, preparation and instrumentation time: 1.06962108612
Removed calls to 'drm_err' (function is undefined)
Removed calls to 'drm_ut_debug_printk' (function is undefined)
Removed calls to 'ttm_eu_backoff_reservation' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'ttm_bo_del_sub_from_lru' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function drm_gem_handle_create as symbolic
Removed calls to 'drm_gem_object_free' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function drm_gem_object_init as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'drm_gem_object_release' (function is undefined)
Defining function ttm_bo_init as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function idr_replace as symbolic
Removed calls to 'fence_init' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'reservation_object_add_shared_fence' (function is undefined)
Removed calls to 'ttm_bo_add_to_lru' (function is undefined)
Removed calls to 'ww_mutex_unlock' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function debug_locks_off as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to 'ttm_mem_io_free' (function is undefined)
Removed calls to 'ttm_mem_io_unlock' (function is undefined)
Removed calls to 'ttm_bo_kunmap' (function is undefined)
Defining function ttm_mem_io_lock as symbolic
Defining function ttm_mem_io_reserve as symbolic
Defining function ttm_bo_kmap as symbolic
Removed calls to 'idr_preload' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'fence_release' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function fence_signal as symbolic
Defining function vsnprintf as symbolic
Defining function idr_alloc as symbolic
Defining function schedule_timeout as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
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 'drm_kms_helper_poll_init' (function is undefined)
Removed calls to 'drm_vblank_cleanup' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Defining function drm_pci_set_busid as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'ttm_bo_unref' (function is undefined)
Defining function drm_gem_prime_handle_to_fd as symbolic
Defining function drm_gem_prime_fd_to_handle as symbolic
Defining function drm_gem_prime_export as symbolic
Defining function drm_gem_prime_import as symbolic
Defining function drm_gem_dumb_destroy as symbolic
Defining function drm_gem_object_lookup as symbolic
Defining function drm_debugfs_remove_files as symbolic
Defining function drm_debugfs_create_files as symbolic
Defining function queue_work_on as symbolic
Defining function flush_work as symbolic
Defining function ttm_eu_reserve_buffers as symbolic
Defining function ttm_bo_validate as symbolic
Defining function reservation_object_reserve_shared as symbolic
Removed calls to 'usleep_range' (function is undefined)
Defining function ttm_bo_wait as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function mutex_trylock as symbolic
Defining function idr_find_slowpath as symbolic
Removed calls to 'drm_mode_config_cleanup' (function is undefined)
Removed calls to 'drm_global_item_unref' (function is undefined)
Defining function ttm_bo_clean_mm as symbolic
Defining function ttm_bo_device_release as symbolic
Defining function printk as symbolic
Removed calls to 'framebuffer_release' (function is undefined)
Removed calls to 'drm_fb_helper_fini' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'drm_framebuffer_cleanup' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Defining function unregister_framebuffer as symbolic
Defining function drm_vblank_init as symbolic
Removed calls to 'drm_mode_config_init' (function is undefined)
Removed calls to 'drm_object_attach_property' (function is undefined)
Defining function drm_mode_create_suggested_offset_properties as symbolic
Removed calls to 'drm_fb_helper_prepare' (function is undefined)
Defining function drm_fb_helper_init as symbolic
Defining function drm_fb_helper_single_add_all_connectors as symbolic
Defining function drm_fb_helper_initial_config as symbolic
Defining function drm_connector_init as symbolic
Defining function drm_encoder_init as symbolic
Defining function drm_mode_connector_attach_encoder as symbolic
Defining function drm_connector_register as symbolic
Defining function drm_crtc_init as symbolic
Defining function drm_mode_crtc_set_gamma_size as symbolic
Defining function drm_property_create_range as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function drm_irq_install as symbolic
Removed calls to 'drm_modeset_lock_all' (function is undefined)
Removed calls to 'drm_modeset_unlock_all' (function is undefined)
Removed calls to 'drm_kms_helper_hotplug_event' (function is undefined)
Defining function drm_helper_hpd_irq_event as symbolic
Defining function drm_object_property_set_value as symbolic
Defining function crc32_le as symbolic
Defining function ttm_bo_device_init as symbolic
Defining function ttm_bo_init_mm as symbolic
Defining function drm_mm_dump_table as symbolic
Removed calls to 'ttm_mem_global_release' (function is undefined)
Defining function drm_global_item_ref as symbolic
Defining function ttm_bo_global_init as symbolic
Defining function ttm_mem_global_init as symbolic
Defining function ioremap_nocache as symbolic
Defining function ioremap_wc as symbolic
Defining function drm_read as symbolic
Defining function drm_poll as symbolic
Defining function drm_ioctl as symbolic
Defining function drm_open as symbolic
Defining function drm_release as symbolic
Defining function ttm_bo_mmap as symbolic
Removed calls to 'drm_put_dev' (function is undefined)
Defining function drm_get_pci_dev as symbolic
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'drm_helper_resume_force_mode' (function is undefined)
Removed calls to 'console_lock' (function is undefined)
Removed calls to 'fb_set_suspend' (function is undefined)
Removed calls to 'console_unlock' (function is undefined)
Removed calls to 'drm_kms_helper_poll_enable' (function is undefined)
Removed calls to 'drm_kms_helper_poll_disable' (function is undefined)
Defining function pci_save_state as symbolic
Defining function ttm_bo_evict_mm as symbolic
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Removed calls to 'drm_helper_mode_fill_fb_struct' (function is undefined)
Defining function drm_framebuffer_init as symbolic
Removed calls to 'drm_crtc_cleanup' (function is undefined)
Defining function drm_crtc_helper_set_config as symbolic
Removed calls to 'drm_send_vblank_event' (function is undefined)
Removed calls to 'drm_vblank_put' (function is undefined)
Defining function drm_vblank_get as symbolic
Defining function drm_helper_probe_single_connector_modes_nomerge as symbolic
Removed calls to 'drm_connector_unregister' (function is undefined)
Removed calls to 'drm_connector_cleanup' (function is undefined)
Removed calls to 'drm_encoder_cleanup' (function is undefined)
Removed calls to 'drm_mode_probed_add' (function is undefined)
Defining function drm_cvt_mode as symbolic
Removed calls to 'ttm_pool_unpopulate' (function is undefined)
Defining function drm_vma_node_is_allowed as symbolic
Defining function ttm_bo_move_memcpy as symbolic
Defining function ttm_pool_populate as symbolic
Defining function ttm_dma_tt_init as symbolic
Removed calls to 'ttm_dma_tt_fini' (function is undefined)
Removed calls to 'drm_fb_get_bpp_depth' (function is undefined)
Removed calls to 'drm_fb_helper_fill_fix' (function is undefined)
Removed calls to 'drm_fb_helper_fill_var' (function is undefined)
Removed calls to 'fb_deferred_io_init' (function is undefined)
Defining function drm_mode_legacy_fb_format as symbolic
Defining function vmalloc as symbolic
Defining function framebuffer_alloc as symbolic
Defining function fb_alloc_cmap as symbolic
Defining function drm_fb_helper_check_var as symbolic
Defining function drm_fb_helper_set_par as symbolic
Defining function drm_fb_helper_setcmap as symbolic
Defining function drm_fb_helper_blank as symbolic
Defining function drm_fb_helper_pan_display as symbolic
Removed calls to 'sys_fillrect' (function is undefined)
Removed calls to 'sys_copyarea' (function is undefined)
Removed calls to 'sys_imageblit' (function is undefined)
Defining function drm_fb_helper_debug_enter as symbolic
Defining function drm_fb_helper_debug_leave as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Defining function rcu_read_lock_held as symbolic
Defining function seq_printf as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function __copy_user_nocache as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'drm_pci_exit' (function is undefined)
Removed calls to 'drm_helper_connector_dpms' (function is undefined)
Defining function ldv_suspend_late_20 as symbolic
Defining function ldv_restore_early_20 as symbolic
Defining function ldv_resume_early_20 as symbolic
Defining function ldv_thaw_early_20 as symbolic
Defining function ldv_resume_noirq_20 as symbolic
Defining function ldv_freeze_noirq_20 as symbolic
Defining function ldv_prepare_20 as symbolic
Defining function ldv_freeze_late_20 as symbolic
Defining function ldv_thaw_noirq_20 as symbolic
Defining function ldv_poweroff_noirq_20 as symbolic
Defining function ldv_poweroff_late_20 as symbolic
Defining function ldv_restore_noirq_20 as symbolic
Defining function ldv_suspend_noirq_20 as symbolic
Defining function ldv_complete_20 as symbolic
Defining function ldv_shutdown_19 as symbolic
Defining function ldv_release_15 as symbolic
Defining function ldv_bind_15 as symbolic
Defining function ldv_connect_15 as symbolic
Defining function ldv_probe_12 as symbolic
Defining function ldv_probe_16 as symbolic
Defining function vgacon_text_force as symbolic
Defining function drm_pci_init as symbolic
Defining function ldv_probe_17 as symbolic
Defining function ldv_probe_11 as symbolic
Defining function queue_delayed_work_on as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __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.01001000404
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 444 859 3265 17873
INFO: Starting verification
KLEE: WARNING ONCE: function "qxl_execbuffer_ioctl" has inline asm
KLEE: WARNING ONCE: function "qxl_gem_object_create_with_handle" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_kunmap_atomic_page" has inline asm
KLEE: WARNING ONCE: function "qxl_release_fence_buffer_objects" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "qxl_ring_push" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_kmap_atomic_page" has inline asm
KLEE: WARNING ONCE: function "qxl_release_alloc" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_ref" has inline asm
KLEE: WARNING ONCE: function "qxl_release_free" has inline asm
KLEE: WARNING ONCE: function "qxl_io_log" has inline asm
KLEE: WARNING ONCE: function "qxl_driver_load" has inline asm
KLEE: WARNING ONCE: function "qxl_irq_handler" has inline asm
KLEE: WARNING ONCE: function "qxl_mode_dumb_mmap" has inline asm
KLEE: WARNING ONCE: function "qxl_surface_id_alloc" has inline asm
KLEE: WARNING ONCE: function "wait_for_io_cmd_user" has inline asm
KLEE: WARNING ONCE: function "qxl_pm_restore" has inline asm
KLEE: WARNING ONCE: function "qxl_send_monitors_config" has inline asm
KLEE: WARNING ONCE: function "qxl_enc_commit" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_move" has inline asm
KLEE: WARNING ONCE: function "qxl_fb_find_or_create_single" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference" has inline asm
KLEE: WARNING ONCE: function "qxl_debugfs_buffers_info" has inline asm
KLEE: WARNING ONCE: function "qxl_fence_wait" has inline asm
KLEE: WARNING ONCE: function "qxl_io_reset" has inline asm
KLEE: WARNING ONCE: function "qxl_io_notify_oom" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "qxl_get_handle_for_primary_fb" has inline asm
KLEE: WARNING ONCE: function "qxl_io_flush_release" has inline asm
KLEE: WARNING: undefined reference to function: drm_helper_connector_dpms
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: undefined reference to function: ttm_bo_global_release
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-Bwidy0/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "qxl_execbuffer_ioctl" has inline asm
KLEE: WARNING ONCE: function "qxl_gem_object_create_with_handle" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_kunmap_atomic_page" has inline asm
KLEE: WARNING ONCE: function "qxl_release_fence_buffer_objects" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "qxl_ring_push" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_kmap_atomic_page" has inline asm
KLEE: WARNING ONCE: function "qxl_release_alloc" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_ref" has inline asm
KLEE: WARNING ONCE: function "qxl_release_free" has inline asm
KLEE: WARNING ONCE: function "qxl_io_log" has inline asm
KLEE: WARNING ONCE: function "qxl_driver_load" has inline asm
KLEE: WARNING ONCE: function "qxl_irq_handler" has inline asm
KLEE: WARNING ONCE: function "qxl_mode_dumb_mmap" has inline asm
KLEE: WARNING ONCE: function "qxl_surface_id_alloc" has inline asm
KLEE: WARNING ONCE: function "wait_for_io_cmd_user" has inline asm
KLEE: WARNING ONCE: function "qxl_pm_restore" has inline asm
KLEE: WARNING ONCE: function "qxl_send_monitors_config" has inline asm
KLEE: WARNING ONCE: function "qxl_enc_commit" has inline asm
KLEE: WARNING ONCE: function "qxl_bo_move" has inline asm
KLEE: WARNING ONCE: function "qxl_fb_find_or_create_single" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference" has inline asm
KLEE: WARNING ONCE: function "qxl_debugfs_buffers_info" has inline asm
KLEE: WARNING ONCE: function "qxl_fence_wait" has inline asm
KLEE: WARNING ONCE: function "qxl_io_reset" has inline asm
KLEE: WARNING ONCE: function "qxl_io_notify_oom" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "qxl_get_handle_for_primary_fb" has inline asm
KLEE: WARNING ONCE: function "qxl_io_flush_release" has inline asm
KLEE: WARNING: undefined reference to function: drm_helper_connector_dpms
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: undefined reference to function: ttm_bo_global_release
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 2.38520789146
