bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 1494 1217 19420 126111
Removed infinite loop in i915_gem_entervt_ioctl
Removed infinite loop in i915_gem_do_execbuffer
Removed infinite loop in i915_add_request
Removed infinite loop in i915_gem_object_move_to_active
Removed infinite loop in i915_wait_request
Removed infinite loop in i915_gem_object_move_to_flushing
Removed infinite loop in i915_gem_object_move_to_inactive
Removed infinite loop in i915_gem_object_wait_rendering
Removed infinite loop in i915_gem_object_set_to_gtt_domain
Removed infinite loop in i915_gem_object_pin
Removed infinite loop in i915_gem_object_unpin
Removed infinite loop in i915_gem_evict_everything
Removed infinite loop in i915_gem_object_bind_to_gtt
Removed infinite loop in i915_gem_evict_something
Removed infinite loop in i915_gem_object_get_pages_gtt
Removed infinite loop in i915_gem_object_put_pages_gtt
Removed infinite loop in i915_gem_object_set_to_cpu_domain
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in intel_pin_and_fence_fb_obj
Removed infinite loop in intel_overlay_switch_off
Removed infinite loop in intel_overlay_do_put_image
Removed infinite loop in intel_overlay_on
Removed infinite loop in intel_overlay_continue
Removed infinite loop in intel_overlay_do_wait_request
Removed infinite loop in intel_overlay_off
Removed infinite loop in intel_overlay_off_tail
Removed infinite loop in i915_gem_object_set_cpu_read_domain_range
Removed infinite loop in i915_gem_restore_gtt_mappings
Removed infinite loop in ldv_module_put_and_exit
Removed infinite loop in intel_crtc_init
Removed infinite loop in intel_enable_pll
Removed infinite loop in intel_enable_pch_pll
Removed infinite loop in intel_enable_transcoder
Removed infinite loop in ironlake_crtc_disable
Removed infinite loop in intel_disable_pch_pll
Removed infinite loop in ironlake_crtc_mode_set
Removed infinite loop in intel_cleanup_overlay
Removed infinite loop in i915_gem_init_object
INFO: Compilation, preparation and instrumentation time: 4.18732500076
Removed calls to 'drm_ut_debug_printk' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'drm_core_ioremap_wc' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'mark_page_accessed' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'intel_gtt_chipset_flush' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'shmem_truncate_range' (function is undefined)
Removed calls to 'drm_mode_set_crtcinfo' (function is undefined)
Defining function drm_err as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function drm_gem_object_lookup as symbolic
Defining function kref_put as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function mod_timer as symbolic
Defining function queue_delayed_work as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'kref_get' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function autoremove_wake_function as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'drm_clflush_pages' (function is undefined)
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Removed calls to 'drm_mm_put_block' (function is undefined)
Removed calls to 'unmap_mapping_range' (function is undefined)
Defining function drm_mm_search_free_in_range as symbolic
Defining function drm_mm_search_free as symbolic
Defining function drm_mm_get_block_range_generic as symbolic
Removed calls to 'drm_mm_init_scan_with_range' (function is undefined)
Removed calls to 'drm_mm_init_scan' (function is undefined)
Removed calls to 'intel_gtt_insert_sg_entries' (function is undefined)
Removed calls to 'intel_gtt_insert_pages' (function is undefined)
Defining function set_page_dirty as symbolic
Defining function intel_gtt_map_memory as symbolic
Defining function shmem_read_mapping_page_gfp as symbolic
Defining function drm_mm_scan_remove_block as symbolic
Defining function drm_mm_scan_add_block as symbolic
Removed calls to 'drm_gem_object_release' (function is undefined)
Defining function drm_ht_remove_item as symbolic
Defining function drm_mm_get_block_generic as symbolic
Removed calls to 'intel_gtt_clear_range' (function is undefined)
Removed calls to 'intel_gtt_unmap_memory' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Defining function wait_for_completion_interruptible as symbolic
Defining function ioread32 as symbolic
Defining function _copy_from_user as symbolic
Defining function __vmalloc as symbolic
Defining function i2c_transfer as symbolic
Defining function compat_alloc_user_space as symbolic
Defining function drm_ioctl as symbolic
Defining function seq_printf as symbolic
Defining function seq_write as symbolic
Removed calls to 'getrawmonotonic' (function is undefined)
Removed calls to 'set_normalized_timespec' (function is undefined)
Defining function jiffies_to_msecs as symbolic
Defining function default_llseek as symbolic
Defining function simple_strtoul as symbolic
Defining function printk as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function queue_work as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function snprintf as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to 'drm_framebuffer_cleanup' (function is undefined)
Defining function drm_gem_handle_create as symbolic
Defining function drm_fb_helper_hotplug_event as symbolic
Defining function drm_framebuffer_init as symbolic
Defining function drm_helper_mode_fill_fb_struct as symbolic
Removed calls to 'drm_crtc_cleanup' (function is undefined)
Defining function drm_crtc_helper_set_config as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function drm_vblank_get as symbolic
Defining function cancel_work_sync as symbolic
Defining function drm_pci_alloc as symbolic
Defining function set_memory_wc as symbolic
Removed calls to 'drm_vblank_pre_modeset' (function is undefined)
Removed calls to 'drm_vblank_post_modeset' (function is undefined)
Defining function drm_helper_probe_single_connector_modes as symbolic
Removed calls to 'drm_sysfs_connector_remove' (function is undefined)
Removed calls to 'drm_connector_cleanup' (function is undefined)
Removed calls to 'drm_helper_disable_unused_functions' (function is undefined)
Defining function drm_get_encoder_name as symbolic
Defining function drm_get_connector_name as symbolic
Defining function drm_crtc_helper_set_mode as symbolic
Defining function drm_gem_object_init as symbolic
Defining function drm_get_edid as symbolic
Removed calls to 'drm_encoder_cleanup' (function is undefined)
Defining function drm_mode_connector_update_edid_property as symbolic
Defining function drm_add_edid_modes as symbolic
Defining function acpi_lid_notifier_unregister as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_byte as symbolic
Removed calls to 'drm_mode_probed_add' (function is undefined)
Defining function drm_mode_duplicate as symbolic
Defining function drm_connector_property_set_value as symbolic
Defining function drm_detect_monitor_audio as symbolic
Defining function i2c_del_adapter as symbolic
Defining function drm_detect_hdmi_monitor as symbolic
Removed calls to 'drm_mode_destroy' (function is undefined)
Removed calls to 'drm_property_destroy' (function is undefined)
Defining function usecs_to_jiffies as symbolic
Defining function i2c_bit_add_bus as symbolic
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 'vga_switcheroo_client_fb_set' (function is undefined)
Defining function framebuffer_alloc as symbolic
Defining function fb_alloc_cmap as symbolic
Defining function ioremap_wc 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
Defining function drm_fb_helper_debug_enter as symbolic
Defining function drm_fb_helper_debug_leave as symbolic
Defining function drm_mode_vrefresh as symbolic
Defining function drm_mode_create as symbolic
Defining function drm_mode_object_find as symbolic
Defining function drm_ht_insert_item as symbolic
Defining function do_mmap_pgoff as symbolic
Defining function get_user_pages as symbolic
Defining function __copy_user_nocache as symbolic
Defining function drm_irq_uninstall as symbolic
Defining function del_timer_sync as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'drm_core_ioremapfree' (function is undefined)
Defining function drm_irq_install as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function drm_mm_init as symbolic
Removed calls to 'drm_pci_free' (function is undefined)
Defining function default_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function drm_getsarea as symbolic
Removed calls to 'pci_dev_put' (function is undefined)
Defining function pci_get_class as symbolic
Removed calls to 'drm_kms_helper_poll_disable' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function pci_save_state as symbolic
Defining function dev_err as symbolic
Removed calls to 'iounmap' (function is undefined)
Defining function unregister_acpi_notifier as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'drm_mode_config_reset' (function is undefined)
Removed calls to 'drm_kms_helper_poll_enable' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function drm_helper_resume_force_mode as symbolic
Defining function register_acpi_notifier as symbolic
Defining function acpi_bus_get_device as symbolic
Defining function acpi_is_video_device as symbolic
Defining function dev_printk as symbolic
Defining function acpi_evaluate_integer as symbolic
Defining function ioremap_cache as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function mutex_trylock as symbolic
Defining function get_seconds as symbolic
Defining function ldv_undefined_int as symbolic
Removed calls to 'drm_kms_helper_poll_init' (function is undefined)
Removed calls to 'vga_switcheroo_unregister_client' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'unregister_shrinker' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Defining function pci_iomap as symbolic
Defining function intel_gtt_get as symbolic
Defining function mtrr_add as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'register_shrinker' (function is undefined)
Defining function pci_enable_msi_block as symbolic
Defining function drm_vblank_init as symbolic
Defining function acpi_video_register as symbolic
Defining function mtrr_del as symbolic
Defining function release_resource as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function __symbol_get as symbolic
Removed calls to 'pci_unmap_rom' (function is undefined)
Removed calls to 'drm_mode_debug_printmodeline' (function is undefined)
Defining function vga_client_register as symbolic
Defining function vga_switcheroo_register_client as symbolic
Removed calls to 'drm_mode_config_init' (function is undefined)
Removed calls to 'drm_crtc_init' (function is undefined)
Removed calls to 'vga_put' (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 pci_bus_read_config_word as symbolic
Removed calls to 'drm_connector_init' (function is undefined)
Removed calls to 'drm_encoder_init' (function is undefined)
Defining function drm_mode_create_tv_properties as symbolic
Defining function drm_connector_attach_property as symbolic
Defining function drm_sysfs_connector_add as symbolic
Defining function drm_mode_connector_attach_encoder as symbolic
Removed calls to 'drm_mode_set_name' (function is undefined)
Defining function drm_property_create as symbolic
Defining function drm_property_add_enum as symbolic
Defining function i2c_add_adapter as symbolic
Defining function i2c_dp_aux_add_bus as symbolic
Defining function dmi_check_system as symbolic
Defining function drm_mode_create_scaling_mode_property as symbolic
Defining function acpi_lid_notifier_register as symbolic
Defining function acpi_lid_open as symbolic
Defining function vga_get as symbolic
Defining function drm_mode_crtc_set_gamma_size as symbolic
Removed calls to 'drm_vblank_off' (function is undefined)
Defining function dev_get_drvdata as symbolic
Defining function acpi_get_name as symbolic
Defining function acpi_get_handle as symbolic
Defining function acpi_evaluate_object as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_map_rom as symbolic
Defining function pnp_range_reserved as symbolic
Defining function pcibios_align_resource as symbolic
Defining function pci_bus_alloc_resource as symbolic
Defining function drm_handle_vblank as symbolic
Removed calls to 'drm_vblank_put' (function is undefined)
Defining function drm_vblank_count_and_time as symbolic
Defining function ns_to_timeval as symbolic
Defining function schedule_work as symbolic
Removed calls to 'drm_helper_hpd_irq_event' (function is undefined)
Removed calls to 'complete_all' (function is undefined)
Defining function kobject_uevent_env as symbolic
Defining function drm_calc_vbltimestamp_from_scanoutpos as symbolic
Defining function dma_supported as symbolic
Defining function pci_get_domain_bus_and_slot as symbolic
Removed calls to 'acpi_video_unregister' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'drm_mm_takedown' (function is undefined)
Removed calls to 'fb_dealloc_cmap' (function is undefined)
Removed calls to 'framebuffer_release' (function is undefined)
Removed calls to 'drm_fb_helper_fini' (function is undefined)
Removed calls to 'drm_kms_helper_poll_fini' (function is undefined)
Removed calls to 'drm_mode_config_cleanup' (function is undefined)
Defining function set_memory_wb as symbolic
Defining function unregister_framebuffer as symbolic
Defining function vga_switcheroo_process_delayed_switch as symbolic
Defining function drm_fb_helper_restore_fbdev_mode as symbolic
Defining function drm_debugfs_create_files as symbolic
Defining function debugfs_create_file as symbolic
Removed calls to 'debugfs_remove' (function is undefined)
Defining function drm_debugfs_remove_files as symbolic
Defining function drm_gem_handle_delete as symbolic
Defining function vm_insert_pfn as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function drm_compat_ioctl as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 3.93767595291
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1373 889 8429 66017
INFO: Starting verification
KLEE: WARNING ONCE: function "i915_irq_wait" has inline asm
KLEE: WARNING ONCE: function "i915_gem_throttle_ioctl" has inline asm
KLEE: WARNING ONCE: function "i915_gem_entervt_ioctl" has inline asm
KLEE: WARNING ONCE: function "i915_gem_pread_ioctl" has inline asm
KLEE: WARNING ONCE: function "i915_gem_pwrite_ioctl" has inline asm
KLEE: WARNING ONCE: function "i915_gem_mmap_ioctl" has inline asm
KLEE: WARNING ONCE: function "intel_overlay_put_image" has inline asm
KLEE: WARNING ONCE: function "i915_gem_do_execbuffer" has inline asm
KLEE: WARNING ONCE: function "fault_in_pages_readable" has inline asm
KLEE: WARNING ONCE: function "i915_gem_execbuffer_relocate_entry" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_wait_rendering" has inline asm
KLEE: WARNING ONCE: function "i915_add_request" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_move_to_active" has inline asm
KLEE: WARNING ONCE: function "intel_increase_pllclock" has inline asm
KLEE: WARNING ONCE: function "i915_read32___6" has inline asm
KLEE: WARNING ONCE: function "i915_write32___4" has inline asm
KLEE: WARNING ONCE: function "intel_wait_for_vblank" has inline asm
KLEE: WARNING ONCE: function "__gen6_gt_wait_for_fifo" has inline asm
KLEE: WARNING ONCE: function "gen6_gt_force_wake_get" has inline asm
KLEE: WARNING ONCE: function "gen6_gt_force_wake_put" has inline asm
KLEE: WARNING ONCE: function "__gen6_gt_force_wake_get" has inline asm
KLEE: WARNING ONCE: function "i915_wait_request" has inline asm
KLEE: WARNING ONCE: function "i915_read32" has inline asm
KLEE: WARNING ONCE: function "i915_gem_retire_requests_ring" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_move_to_inactive" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_set_to_gtt_domain" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_pin" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_get_fence" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_unpin" has inline asm
KLEE: WARNING ONCE: function "i915_gem_evict_everything" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_flush_fence" has inline asm
KLEE: WARNING ONCE: function "i915_write64" has inline asm
KLEE: WARNING ONCE: function "i915_write32" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_bind_to_gtt" has inline asm
KLEE: WARNING ONCE: function "i915_gem_evict_something" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_do_bit_17_swizzle" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_put_pages_gtt" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_save_bit_17_swizzle" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_set_to_cpu_domain" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_flush_gtt_write_domain" has inline asm
KLEE: WARNING ONCE: function "i915_read32___13" has inline asm
KLEE: WARNING ONCE: function "compat_i915_batchbuffer" has inline asm
KLEE: WARNING ONCE: function "compat_i915_irq_emit" has inline asm
KLEE: WARNING ONCE: function "compat_i915_getparam" has inline asm
KLEE: WARNING ONCE: function "compat_i915_alloc" has inline asm
KLEE: WARNING ONCE: function "compat_i915_cmdbuffer" has inline asm
KLEE: WARNING ONCE: function "i915_read32___2" has inline asm
KLEE: WARNING ONCE: function "i915_mch_val" has inline asm
KLEE: WARNING ONCE: function "i915_read32___0" has inline asm
KLEE: WARNING ONCE: function "i915_read16___0" has inline asm
KLEE: WARNING ONCE: function "i915_handle_error" has inline asm
KLEE: WARNING ONCE: function "i915_read64" has inline asm
KLEE: WARNING ONCE: function "i915_error_object_create" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "intel_crtc_cursor_set" has inline asm
KLEE: WARNING ONCE: function "intel_crtc_page_flip" has inline asm
KLEE: WARNING ONCE: function "i845_update_cursor" has inline asm
KLEE: WARNING ONCE: function "i915_gem_attach_phys_object" has inline asm
KLEE: WARNING ONCE: function "i915_gem_detach_phys_object" has inline asm
KLEE: WARNING ONCE: function "intel_wait_for_pipe_off" has inline asm
KLEE: WARNING ONCE: function "intel_pipe_set_base" has inline asm
KLEE: WARNING ONCE: function "intel_pipe_set_base_atomic" has inline asm
KLEE: WARNING ONCE: function "intel_update_fbc" has inline asm
KLEE: WARNING ONCE: function "intel_pin_and_fence_fb_obj" has inline asm
KLEE: WARNING ONCE: function "intel_crt_detect" has inline asm
KLEE: WARNING ONCE: function "intel_ironlake_crt_detect_hotplug" has inline asm
KLEE: WARNING ONCE: function "i915_read32___7" has inline asm
KLEE: WARNING ONCE: function "intel_crt_load_detect" has inline asm
KLEE: WARNING ONCE: function "i915_write32___5" has inline asm
KLEE: WARNING ONCE: function "i915_read8___1" has inline asm
KLEE: WARNING ONCE: function "intel_lvds_dpms" has inline asm
KLEE: WARNING ONCE: function "intel_lvds_prepare" has inline asm
KLEE: WARNING ONCE: function "intel_lvds_commit" has inline asm
KLEE: WARNING ONCE: function "i915_read32___8" has inline asm
KLEE: WARNING ONCE: function "intel_lvds_enable" has inline asm
KLEE: WARNING ONCE: function "i915_write32___6" has inline asm
KLEE: WARNING ONCE: function "intel_panel_get_max_backlight" has inline asm
KLEE: WARNING ONCE: function "intel_panel_set_backlight" has inline asm
KLEE: WARNING ONCE: function "i915_read32___10" has inline asm
KLEE: WARNING ONCE: function "i915_write32___8" has inline asm
KLEE: WARNING ONCE: function "intel_dp_prepare" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_panel_vdd_on" has inline asm
KLEE: WARNING ONCE: function "intel_dp_start_link_train" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_panel_on" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_panel_vdd_off" has inline asm
KLEE: WARNING ONCE: function "intel_dp_complete_link_train" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_backlight_on" has inline asm
KLEE: WARNING ONCE: function "intel_dp_link_down" has inline asm
KLEE: WARNING ONCE: function "intel_dp_set_link_train" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_backlight_off" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_panel_off" has inline asm
KLEE: WARNING ONCE: function "ironlake_edp_pll_off" has inline asm
KLEE: WARNING ONCE: function "intel_hdmi_dpms" has inline asm
KLEE: WARNING ONCE: function "intel_hdmi_mode_set" has inline asm
KLEE: WARNING ONCE: function "i915_write32___9" has inline asm
KLEE: WARNING ONCE: function "i915_read32___11" has inline asm
KLEE: WARNING ONCE: function "intel_sdvo_write_sdvox" has inline asm
KLEE: WARNING ONCE: function "gmbus_xfer" has inline asm
KLEE: WARNING ONCE: function "i915_write32___12" has inline asm
KLEE: WARNING ONCE: function "i915_read32___14" has inline asm
KLEE: WARNING ONCE: function "set_data" has inline asm
KLEE: WARNING ONCE: function "set_clock" has inline asm
KLEE: WARNING ONCE: function "get_data" has inline asm
KLEE: WARNING ONCE: function "get_clock" has inline asm
KLEE: WARNING ONCE: function "intel_i2c_reset" has inline asm
KLEE: WARNING ONCE: function "intel_tv_detect_type" has inline asm
KLEE: WARNING ONCE: function "i915_disable_pipestat" has inline asm
KLEE: WARNING ONCE: function "i915_enable_pipestat" has inline asm
KLEE: WARNING ONCE: function "intel_tv_dpms" has inline asm
KLEE: WARNING ONCE: function "intel_tv_mode_set" has inline asm
KLEE: WARNING ONCE: function "i915_write32___11" has inline asm
KLEE: WARNING ONCE: function "render_ring_get_irq" has inline asm
KLEE: WARNING ONCE: function "render_ring_put_irq" has inline asm
KLEE: WARNING ONCE: function "gen6_bsd_ring_write_tail" has inline asm
KLEE: WARNING ONCE: function "gen6_ring_get_irq" has inline asm
KLEE: WARNING ONCE: function "bsd_ring_get_irq" has inline asm
KLEE: WARNING ONCE: function "bsd_ring_put_irq" has inline asm
KLEE: WARNING ONCE: function "blt_ring_put_irq" has inline asm
KLEE: WARNING ONCE: function "intel_overlay_switch_off" has inline asm
KLEE: WARNING ONCE: function "intel_overlay_do_wait_request" has inline asm
KLEE: WARNING ONCE: function "intel_overlay_off_tail" has inline asm
KLEE: WARNING ONCE: function "i915_gem_object_set_cpu_read_domain_range" has inline asm
KLEE: WARNING ONCE: function "intel_ring_setup_status_page" has inline asm
KLEE: WARNING ONCE: function "i915_write32___0" has inline asm
KLEE: WARNING ONCE: function "i915_read8___0" has inline asm
KLEE: WARNING ONCE: function "i915_write8" has inline asm
KLEE: WARNING ONCE: function "ironlake_disable_drps" has inline asm
KLEE: WARNING ONCE: function "gen6_disable_rps" has inline asm
KLEE: WARNING ONCE: function "i915_read16___2" has inline asm
KLEE: WARNING ONCE: function "ironlake_set_drps" has inline asm
KLEE: WARNING ONCE: function "i915_write16___0" has inline asm
KLEE: WARNING ONCE: function "i915_gem_restore_gtt_mappings" has inline asm
KLEE: WARNING ONCE: function "i915_restore_state" has inline asm
KLEE: WARNING ONCE: function "ironlake_enable_display_irq" has inline asm
KLEE: WARNING ONCE: function "ironlake_disable_fbc" has inline asm
KLEE: WARNING ONCE: function "ironlake_enable_drps" has inline asm
KLEE: WARNING ONCE: function "intel_init_emon" has inline asm
KLEE: WARNING ONCE: function "gen6_enable_rps" has inline asm
KLEE: WARNING ONCE: function "i8xx_disable_fbc" has inline asm
KLEE: WARNING ONCE: function "i915_reset" has inline asm
KLEE: WARNING ONCE: function "i915_driver_load" has inline asm
KLEE: WARNING ONCE: function "intel_setup_bios" has inline asm
KLEE: WARNING ONCE: function "i915_read16" has inline asm
KLEE: WARNING ONCE: function "intel_modeset_init" has inline asm
KLEE: WARNING ONCE: function "ironlake_crtc_mode_set" has inline asm
KLEE: WARNING ONCE: function "i9xx_crtc_mode_set" has inline asm
KLEE: WARNING ONCE: function "ironlake_enable_fbc" has inline asm
KLEE: WARNING ONCE: function "ibx_init_clock_gating" has inline asm
KLEE: WARNING ONCE: function "cpt_init_clock_gating" has inline asm
KLEE: WARNING ONCE: function "ironlake_update_wm" has inline asm
KLEE: WARNING ONCE: function "ironlake_fdi_link_train" has inline asm
KLEE: WARNING ONCE: function "ironlake_init_clock_gating" has inline asm
KLEE: WARNING ONCE: function "sandybridge_update_wm" has inline asm
KLEE: WARNING ONCE: function "gen6_fdi_link_train" has inline asm
KLEE: WARNING ONCE: function "gen6_init_clock_gating" has inline asm
KLEE: WARNING ONCE: function "ivb_manual_fdi_link_train" has inline asm
KLEE: WARNING ONCE: function "ivybridge_init_clock_gating" has inline asm
KLEE: WARNING ONCE: function "pineview_update_wm" has inline asm
KLEE: WARNING ONCE: function "i965_update_wm" has inline asm
KLEE: WARNING ONCE: function "intel_lvds_init" has inline asm
KLEE: WARNING ONCE: function "intel_crt_init" has inline asm
KLEE: WARNING ONCE: function "intel_sdvo_init" has inline asm
KLEE: WARNING ONCE: function "intel_tv_init" has inline asm
KLEE: WARNING ONCE: function "intel_idle_update" has inline asm
KLEE: WARNING ONCE: function "intel_crtc_mode_get" has inline asm
KLEE: WARNING ONCE: function "i9xx_crtc_enable" has inline asm
KLEE: WARNING ONCE: function "i9xx_crtc_disable" has inline asm
KLEE: WARNING ONCE: function "intel_crtc_wait_for_pending_flips" has inline asm
KLEE: WARNING ONCE: function "ironlake_crtc_enable" has inline asm
KLEE: WARNING ONCE: function "ironlake_fdi_disable" has inline asm
KLEE: WARNING ONCE: function "ironlake_crtc_disable" has inline asm
KLEE: WARNING ONCE: function "ironlake_compute_srwm" has inline asm
KLEE: WARNING ONCE: function "i915_read16___1" has inline asm
KLEE: WARNING ONCE: function "i915_read32___9" has inline asm
KLEE: WARNING ONCE: function "ivybridge_irq_handler" has inline asm
KLEE: WARNING ONCE: function "ironlake_irq_preinstall" has inline asm
KLEE: WARNING ONCE: function "ivybridge_irq_postinstall" has inline asm
KLEE: WARNING ONCE: function "ironlake_irq_uninstall" has inline asm
KLEE: WARNING ONCE: function "ironlake_irq_handler" has inline asm
KLEE: WARNING ONCE: function "ironlake_irq_postinstall" has inline asm
KLEE: WARNING ONCE: function "i915_driver_irq_preinstall" has inline asm
KLEE: WARNING ONCE: function "i915_driver_irq_postinstall" has inline asm
KLEE: WARNING ONCE: function "i915_driver_irq_uninstall" has inline asm
KLEE: WARNING ONCE: function "i915_driver_irq_handler" has inline asm
KLEE: WARNING ONCE: function "do_intel_finish_page_flip" has inline asm
KLEE: WARNING ONCE: function "intel_opregion_asle_intr" has inline asm
KLEE: WARNING ONCE: function "ironlake_disable_display_irq" has inline asm
KLEE: WARNING ONCE: function "i915_write16" has inline asm
KLEE: WARNING ONCE: function "gen6_pm_rps_work" has inline asm
KLEE: WARNING ONCE: function "intel_modeset_cleanup" has inline asm
KLEE: WARNING ONCE: function "intel_cleanup_overlay" has inline asm
KLEE: WARNING ONCE: function "i915_gem_fault" has inline asm
KLEE: WARNING ONCE: function "i915_gem_init_object" has inline asm
KLEE: WARNING: undefined reference to function: cfb_copyarea
KLEE: WARNING: undefined reference to function: cfb_fillrect
KLEE: WARNING: undefined reference to function: cfb_imageblit
KLEE: WARNING: undefined reference to function: drm_gem_object_free
KLEE: WARNING: undefined reference to function: drm_helper_connector_dpms
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_70c1f618-a3d7-4912-ba16-2b65368b3dc8/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_70c1f618-a3d7-4912-ba16-2b65368b3dc8/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 4256 bytes on read, may be slow and/or crash: MO73[4256] allocated at global:sdvo_tv_modes
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:35661: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58650: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58505: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:35661: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:35661: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58703: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58605: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58650: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58444: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58703: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58506: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXwxOJ/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i:58605: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
