bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.7.3/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.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.: 350 811 5132 40637
Removed infinite loop in vmw_fifo_reserve
Removed infinite loop in vmw_fifo_commit
Removed infinite loop in vmw_fence_obj_unreference
Removed infinite loop in vmw_surface_evict
Removed infinite loop in vmw_execbuf_fence_commands
Removed infinite loop in vmw_resource_alloc_id
Removed infinite loop in vmw_query_bo_switch_prepare
Removed infinite loop in vmw_kms_fb_create
Removed infinite loop in vmw_user_lookup_handle
Removed infinite loop in vmw_framebuffer_dmabuf_pin
Removed infinite loop in vmw_bo_pin
Removed infinite loop in vmw_overlay_update_stream
Removed infinite loop in vmw_overlay_stop
Removed infinite loop in vmw_overlay_send_stop
Removed infinite loop in vmw_query_bo_switch_commit
Removed infinite loop in vmw_clear_validations
Removed infinite loop in vmw_execbuf_copy_fence_user
Removed infinite loop in do_surface_dirty_sou
Removed infinite loop in vmw_master_set
Removed infinite loop in vmw_3d_resource_dec
Removed infinite loop in vmw_fb_on
Removed infinite loop in vmw_release_device
Removed infinite loop in vmw_fence_fifo_down
Removed infinite loop in vmw_fence_manager_takedown
Removed infinite loop in vmw_kms_close_legacy_display_system
Removed infinite loop in vmw_dmabuf_init
Removed infinite loop in vmw_fence_event_ioctl
Removed infinite loop in vmw_kms_readback
Removed infinite loop in vmw_kms_present
Removed infinite loop in vmw_surface_init
Removed infinite loop in vmw_overlay_unref
Removed infinite loop in vmw_ldu_del_active
Removed infinite loop in vmw_ldu_commit_list
Removed infinite loop in vmw_ldu_add_active
Removed infinite loop in vmw_kms_screen_object_update_implicit_fb
Removed infinite loop in vmw_sou_fifo_create
Removed infinite loop in vmw_sou_add_active
INFO: Compilation, preparation and instrumentation time: 1.37040185928
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function drm_err as symbolic
Removed calls to 'vfree' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function ioread32 as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function vmalloc as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function printk as symbolic
Defining function ttm_pool_populate as symbolic
Removed calls to 'warn_slowpath_null' (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 '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function schedule_work as symbolic
Defining function ttm_tt_init as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ida_init' (function is undefined)
Removed calls to 'ida_destroy' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'ida_remove' (function is undefined)
Defining function ida_pre_get as symbolic
Defining function ida_get_new as symbolic
Removed calls to 'ttm_bo_unref' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to 'ttm_base_object_unref' (function is undefined)
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'ttm_eu_fence_buffer_objects' (function is undefined)
Removed calls to 'ttm_eu_backoff_reservation' (function is undefined)
Defining function ttm_bo_create as symbolic
Defining function ttm_eu_reserve_buffers as symbolic
Defining function ttm_bo_validate as symbolic
Removed calls to 'ttm_mem_global_free' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'getrawmonotonic' (function is undefined)
Removed calls to 'set_normalized_timespec' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function ns_to_timespec as symbolic
Defining function ttm_mem_global_alloc as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function ttm_base_object_init as symbolic
Defining function idr_pre_get as symbolic
Defining function idr_get_new_above as symbolic
Defining function ttm_base_object_lookup as symbolic
Defining function idr_find as symbolic
Removed calls to 'ttm_bo_kunmap' (function is undefined)
Removed calls to 'ttm_bo_unreserve' (function is undefined)
Defining function ttm_bo_reserve as symbolic
Defining function ttm_bo_kmap as symbolic
Defining function capable as symbolic
Removed calls to 'drm_fb_get_bpp_depth' (function is undefined)
Defining function drm_framebuffer_init as symbolic
Defining function drm_master_get as symbolic
Removed calls to 'ttm_write_unlock' (function is undefined)
Defining function ttm_write_lock as symbolic
Removed calls to 'drm_ut_debug_printk' (function is undefined)
Removed calls to 'drm_framebuffer_cleanup' (function is undefined)
Removed calls to 'ttm_read_unlock' (function is undefined)
Defining function ttm_read_lock as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function ttm_ref_object_base_unref as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function mutex_lock_interruptible as symbolic
Removed calls to 'drm_master_put' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'ttm_object_device_release' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'drm_global_item_unref' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'ttm_object_file_release' (function is undefined)
Defining function ttm_vt_lock as symbolic
Defining function ttm_bo_evict_mm as symbolic
Defining function ttm_vt_unlock as symbolic
Defining function schedule_delayed_work as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Defining function ttm_bo_wait as symbolic
Removed calls to 'ttm_lock_init' (function is undefined)
Defining function unregister_pm_notifier as symbolic
Defining function drm_irq_uninstall as symbolic
Removed calls to 'fb_deferred_io_cleanup' (function is undefined)
Removed calls to 'framebuffer_release' (function is undefined)
Removed calls to 'drm_mode_config_cleanup' (function is undefined)
Defining function ttm_bo_clean_mm as symbolic
Defining function ttm_bo_device_release as symbolic
Defining function mtrr_del as symbolic
Defining function cancel_work_sync as symbolic
Removed calls to 'drm_vblank_cleanup' (function is undefined)
Defining function unregister_framebuffer as symbolic
Defining function ttm_object_file_init as symbolic
Defining function ttm_bo_device_init as symbolic
Defining function ttm_bo_init_mm as symbolic
Defining function ioremap_wc as symbolic
Defining function ttm_object_device_init as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_request_region as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'drm_mode_config_init' (function is undefined)
Removed calls to 'fb_deferred_io_init' (function is undefined)
Defining function drm_irq_install as symbolic
Removed calls to 'ttm_suspend_lock' (function is undefined)
Removed calls to 'ttm_bo_swapout_all' (function is undefined)
Removed calls to 'ttm_suspend_unlock' (function is undefined)
Defining function register_pm_notifier as symbolic
Defining function framebuffer_alloc as symbolic
Defining function register_framebuffer as symbolic
Defining function ttm_bo_acc_size as symbolic
Defining function ttm_bo_init as symbolic
Removed calls to 'drm_connector_attach_property' (function is undefined)
Defining function drm_vblank_init as symbolic
Defining function drm_mode_create_dirty_info_property 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_crtc_init as symbolic
Defining function drm_mode_crtc_set_gamma_size as symbolic
Defining function ttm_round_pot as symbolic
Defining function mtrr_add 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 drm_mode_object_find as symbolic
Defining function ttm_ref_object_add as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function noop_llseek as symbolic
Defining function drm_compat_ioctl as symbolic
Defining function drm_open as symbolic
Defining function drm_release as symbolic
Defining function drm_fasync as symbolic
Defining function ttm_bo_mmap as symbolic
Defining function drm_ioctl as symbolic
Defining function drm_poll as symbolic
Defining function drm_read as symbolic
Removed calls to 'drm_put_dev' (function is undefined)
Defining function dev_get_drvdata as symbolic
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)
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_save_state as symbolic
Removed calls to 'cfb_fillrect' (function is undefined)
Removed calls to 'cfb_copyarea' (function is undefined)
Removed calls to 'cfb_imageblit' (function is undefined)
Removed calls to 'ttm_tt_fini' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function alloc_pages_current as symbolic
Removed calls to 'drm_mode_probed_add' (function is undefined)
Removed calls to 'drm_mode_destroy' (function is undefined)
Removed calls to 'drm_mode_connector_list_update' (function is undefined)
Removed calls to 'drm_crtc_cleanup' (function is undefined)
Removed calls to 'drm_encoder_cleanup' (function is undefined)
Removed calls to 'drm_connector_cleanup' (function is undefined)
Defining function drm_mode_duplicate as symbolic
Defining function drm_mode_vrefresh as symbolic
Defining function flush_delayed_work_sync as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Removed calls to 'drm_pci_exit' (function is undefined)
Defining function drm_pci_init as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.22552990913
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 649 779 3730 23514
INFO: Starting verification
KLEE: WARNING ONCE: function "vmw_fifo_reserve" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_commit" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_ping_host" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_wait" has inline asm
KLEE: WARNING ONCE: function "vmw_fence_obj_reference" has inline asm
KLEE: WARNING ONCE: function "vmw_fence_obj_unreference" has inline asm
KLEE: WARNING ONCE: function "vmw_fence_obj_wait" has inline asm
KLEE: WARNING ONCE: function "vmw_seqno_waiter_add" has inline asm
KLEE: WARNING ONCE: function "vmw_seqno_waiter_remove" has inline asm
KLEE: WARNING ONCE: function "vmw_cmd_end_query" has inline asm
KLEE: WARNING ONCE: function "vmw_user_surface_lookup_handle" has inline asm
KLEE: WARNING ONCE: function "vmw_surface_validate" has inline asm
KLEE: WARNING ONCE: function "vmw_resource_unreference" has inline asm
KLEE: WARNING ONCE: function "vmw_surface_do_validate" has inline asm
KLEE: WARNING ONCE: function "vmw_surface_evict" has inline asm
KLEE: WARNING ONCE: function "vmw_execbuf_fence_commands" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_send_fence" has inline asm
KLEE: WARNING ONCE: function "vmw_fallback_wait" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_idle" has inline asm
KLEE: WARNING ONCE: function "vmw_resource_alloc_id" has inline asm
KLEE: WARNING ONCE: function "vmw_user_dmabuf_lookup" has inline asm
KLEE: WARNING ONCE: function "vmw_bo_to_validate_list" has inline asm
KLEE: WARNING ONCE: function "vmw_context_check" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_fb_create" has inline asm
KLEE: WARNING ONCE: function "vmw_user_lookup_handle" has inline asm
KLEE: WARNING ONCE: function "vmw_framebuffer_dmabuf_pin" has inline asm
KLEE: WARNING ONCE: function "vmw_execbuf_release_pinned_bo" has inline asm
KLEE: WARNING ONCE: function "vmw_bo_pin" has inline asm
KLEE: WARNING ONCE: function "vmw_overlay_update_stream" has inline asm
KLEE: WARNING ONCE: function "vmw_overlay_stop" has inline asm
KLEE: WARNING ONCE: function "vmw_execbuf_process" has inline asm
KLEE: WARNING ONCE: function "vmw_clear_validations" has inline asm
KLEE: WARNING ONCE: function "vmw_execbuf_copy_fence_user" has inline asm
KLEE: WARNING ONCE: function "vmw_wait_seqno" has inline asm
KLEE: WARNING ONCE: function "do_surface_dirty_sou" has inline asm
KLEE: WARNING ONCE: function "vmw_driver_load" has inline asm
KLEE: WARNING ONCE: function "vmw_irq_handler" has inline asm
KLEE: WARNING ONCE: function "vmw_irq_preinstall" has inline asm
KLEE: WARNING ONCE: function "vmw_irq_uninstall" has inline asm
KLEE: WARNING ONCE: function "vmw_master_set" has inline asm
KLEE: WARNING ONCE: function "vmw_master_drop" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_restore_vga" has inline asm
KLEE: WARNING ONCE: function "vmw_3d_resource_dec" has inline asm
KLEE: WARNING ONCE: function "vmw_fb_on" has inline asm
KLEE: WARNING ONCE: function "vmw_fb_set_par" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_write_svga" has inline asm
KLEE: WARNING ONCE: function "vmw_fence_fifo_down" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_release" has inline asm
KLEE: WARNING ONCE: function "vmw_3d_resource_inc" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_save_vga" has inline asm
KLEE: WARNING ONCE: function "vmw_fifo_init" has inline asm
KLEE: WARNING ONCE: function "vmw_fence_manager_takedown" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_close_legacy_display_system" has inline asm
KLEE: WARNING ONCE: function "vmw_fb_init" has inline asm
KLEE: WARNING ONCE: function "vmw_dmabuf_init" has inline asm
KLEE: WARNING ONCE: function "vmw_du_connector_detect" has inline asm
KLEE: WARNING ONCE: function "vmw_goal_waiter_remove" has inline asm
KLEE: WARNING ONCE: function "vmw_dmabuf_alloc_ioctl" has inline asm
KLEE: WARNING ONCE: function "vmw_stream_claim_ioctl" has inline asm
KLEE: WARNING ONCE: function "vmw_context_define_ioctl" has inline asm
KLEE: WARNING ONCE: function "vmw_surface_define_ioctl" has inline asm
KLEE: WARNING ONCE: function "vmw_fence_event_ioctl" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_readback" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_present" has inline asm
KLEE: WARNING ONCE: function "vmw_goal_waiter_add" has inline asm
KLEE: WARNING ONCE: function "vmw_surface_init" has inline asm
KLEE: WARNING ONCE: function "vmw_resource_lookup" has inline asm
KLEE: WARNING ONCE: function "vmw_overlay_unref" has inline asm
KLEE: WARNING ONCE: function "vmw_gmr_unbind" has inline asm
KLEE: WARNING ONCE: function "vmw_gmr_bind" has inline asm
KLEE: WARNING ONCE: function "vmw_du_crtc_gamma_set" has inline asm
KLEE: WARNING ONCE: function "vmw_ldu_crtc_set_config" has inline asm
KLEE: WARNING ONCE: function "vmw_ldu_commit_list" has inline asm
KLEE: WARNING ONCE: function "vmw_sou_crtc_set_config" has inline asm
KLEE: WARNING ONCE: function "vmw_kms_screen_object_update_implicit_fb" has inline asm
KLEE: WARNING ONCE: function "vmw_resource_reference" has inline asm
KLEE: WARNING: undefined reference to function: ttm_bo_global_release
KLEE: WARNING: undefined reference to function: ttm_pool_unpopulate
KLEE: WARNING ONCE: flushing 9504 bytes on read, may be slow and/or crash: MO81[9504] allocated at global:
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:9326: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:25731: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:6560: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:6497: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:9331: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:15976: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:6573: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_06d12dc8-d23d-4054-bd43-0bd0e9c82222/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_06d12dc8-d23d-4054-bd43-0bd0e9c82222/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:25739: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:15774: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ddyzre/main17_false-unreach-call_drivers-gpu-drm-vmwgfx-vmwgfx-ko--32_7a--linux-3.5.c:25745: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_06d12dc8-d23d-4054-bd43-0bd0e9c82222/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_06d12dc8-d23d-4054-bd43-0bd0e9c82222/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
