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--mgag200--mgag200.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.: 127 383 2529 17221
Removed infinite loop in mga_crtc_cursor_set
Removed infinite loop in mga_crtc_cursor_move
Removed infinite loop in arch_local_save_flags
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.628308057785
Defining function drm_mode_object_find as symbolic
Defining function drm_helper_probe_single_connector_modes as symbolic
Removed calls to 'drm_connector_cleanup' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'ttm_pool_unpopulate' (function is undefined)
Removed calls to 'drm_err' (function is undefined)
Defining function drm_vma_node_is_allowed as symbolic
Defining function ttm_bo_move_memcpy as symbolic
Removed calls to 'drm_gem_object_release' (function is undefined)
Defining function ttm_pool_populate as symbolic
Defining function ttm_tt_init as symbolic
Removed calls to 'drm_framebuffer_cleanup' (function is undefined)
Removed calls to 'drm_gem_object_free' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function drm_gem_object_lookup as symbolic
Removed calls to 'drm_helper_mode_fill_fb_struct' (function is undefined)
Defining function drm_framebuffer_init as symbolic
Removed calls to 'iowrite8' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'ttm_bo_kunmap' (function is undefined)
Removed calls to 'drm_crtc_cleanup' (function is undefined)
Defining function drm_crtc_helper_set_config as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'ttm_bo_del_sub_from_lru' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'ttm_bo_add_to_lru' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'ww_mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function ttm_bo_kmap as symbolic
Defining function ioread32 as symbolic
Defining function ttm_bo_validate as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'drm_ut_debug_printk' (function is undefined)
Defining function ioread8 as symbolic
Defining function printk as symbolic
Defining function pci_bus_write_config_dword as symbolic
Removed calls to 'drm_encoder_cleanup' (function is undefined)
Removed calls to 'iowrite16' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'drm_mode_config_init' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'drm_mode_config_cleanup' (function is undefined)
Defining function drm_pci_set_busid as symbolic
Removed calls to 'ttm_bo_unref' (function is undefined)
Defining function drm_gem_dumb_destroy as symbolic
Defining function drm_gem_handle_create as symbolic
Defining function drm_gem_object_init as symbolic
Defining function ttm_bo_dma_acc_size as symbolic
Defining function ttm_bo_init as symbolic
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 'vfree' (function is undefined)
Removed calls to 'drm_framebuffer_unregister_private' (function is undefined)
Removed calls to 'drm_global_item_unref' (function is undefined)
Removed calls to 'arch_phys_wc_del' (function is undefined)
Defining function ttm_bo_device_release as symbolic
Defining function unregister_framebuffer as symbolic
Defining function drm_mode_connector_attach_encoder as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'drm_fb_helper_prepare' (function is undefined)
Removed calls to 'drm_helper_disable_unused_functions' (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_connector_register as symbolic
Defining function snprintf as symbolic
Defining function i2c_bit_add_bus as symbolic
Defining function drm_encoder_init as symbolic
Defining function drm_crtc_init as symbolic
Defining function drm_mode_crtc_set_gamma_size as symbolic
Defining function ttm_bo_device_init as symbolic
Defining function ttm_bo_init_mm as symbolic
Defining function arch_phys_wc_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 __devm_request_region as symbolic
Defining function pcim_iomap as symbolic
Defining function remove_conflicting_framebuffers as symbolic
Defining function pci_iomap as symbolic
Defining function ioread16 as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function devm_kmalloc as symbolic
Defining function drm_read as symbolic
Defining function drm_poll as symbolic
Defining function drm_ioctl as symbolic
Defining function drm_compat_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 'drm_fb_helper_fill_fix' (function is undefined)
Removed calls to 'drm_fb_helper_fill_var' (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)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'ttm_tt_fini' (function is undefined)
Defining function drm_get_edid as symbolic
Defining function drm_mode_connector_update_edid_property as symbolic
Defining function drm_add_edid_modes as symbolic
Defining function ldv_probe_15 as symbolic
Removed calls to 'drm_helper_connector_dpms' (function is undefined)
Defining function ldv_probe_8 as symbolic
Defining function ldv_probe_13 as symbolic
Defining function ldv_probe_10 as symbolic
Defining function ldv_release_12 as symbolic
Defining function ldv_bind_12 as symbolic
Defining function ldv_connect_12 as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'drm_pci_exit' (function is undefined)
Defining function ldv_shutdown_5 as symbolic
Defining function vgacon_text_force as symbolic
Defining function drm_pci_init as symbolic
Defining function ldv_probe_2 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: 0.641471147537
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 204 392 1610 8969
INFO: Starting verification
KLEE: WARNING ONCE: function "mga_crtc_cursor_set" has inline asm
KLEE: WARNING ONCE: function "mga_crtc_cursor_move" has inline asm
KLEE: WARNING ONCE: function "drm_gem_object_unreference" has inline asm
KLEE: WARNING ONCE: function "mga_dirty_update" has inline asm
KLEE: WARNING: undefined reference to function: drm_helper_connector_dpms
KLEE: WARNING: undefined reference to function: ttm_bo_global_release
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_1ab4c115-ca8b-4d3a-af83-33cfa52b8268/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13560 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17655 states (over memory cap)
KLEE: WARNING: killing 16867 states (over memory cap)
KLEE: WARNING: killing 16661 states (over memory cap)
KLEE: WARNING: killing 16622 states (over memory cap)
KLEE: WARNING: killing 16753 states (over memory cap)
KLEE: WARNING: killing 17451 states (over memory cap)
KLEE: WARNING: killing 16509 states (over memory cap)
KLEE: WARNING: killing 16231 states (over memory cap)
KLEE: WARNING: killing 17655 states (over memory cap)
KLEE: WARNING: killing 17785 states (over memory cap)
KLEE: WARNING: killing 18484 states (over memory cap)
KLEE: WARNING: killing 18859 states (over memory cap)
KLEE: WARNING: killing 20292 states (over memory cap)
KLEE: WARNING: killing 19126 states (over memory cap)
KLEE: WARNING: killing 20152 states (over memory cap)
KLEE: WARNING: killing 21011 states (over memory cap)
KLEE: WARNING: killing 20258 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:5849: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21430 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8524: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20596 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:11944: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21532 states (over memory cap)
KLEE: WARNING: killing 21017 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:5280: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21550 states (over memory cap)
KLEE: WARNING: killing 19685 states (over memory cap)
KLEE: WARNING: killing 21492 states (over memory cap)
KLEE: WARNING: killing 21067 states (over memory cap)
KLEE: WARNING: killing 20400 states (over memory cap)
KLEE: WARNING: killing 20047 states (over memory cap)
KLEE: WARNING: killing 19938 states (over memory cap)
KLEE: WARNING: killing 19901 states (over memory cap)
KLEE: WARNING: killing 19723 states (over memory cap)
KLEE: WARNING: killing 21358 states (over memory cap)
KLEE: WARNING: killing 19666 states (over memory cap)
KLEE: WARNING: killing 19568 states (over memory cap)
KLEE: WARNING: killing 19934 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8636: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18961 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8695: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20582 states (over memory cap)
KLEE: WARNING: killing 20156 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8323: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:7775: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20914 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8276: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:6659: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20414 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8365: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20081 states (over memory cap)
KLEE: WARNING: killing 21069 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:11762: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20194 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:7867: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20318 states (over memory cap)
KLEE: WARNING: killing 20926 states (over memory cap)
KLEE: WARNING: killing 20365 states (over memory cap)
KLEE: WARNING: killing 19412 states (over memory cap)
KLEE: WARNING: killing 20774 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:8848: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21448 states (over memory cap)
KLEE: WARNING: killing 20181 states (over memory cap)
KLEE: WARNING: killing 20006 states (over memory cap)
KLEE: WARNING: killing 21137 states (over memory cap)
KLEE: WARNING: killing 19879 states (over memory cap)
KLEE: WARNING: killing 20241 states (over memory cap)
KLEE: WARNING: killing 20367 states (over memory cap)
KLEE: WARNING: killing 20038 states (over memory cap)
KLEE: WARNING: killing 20317 states (over memory cap)
KLEE: WARNING: killing 19989 states (over memory cap)
KLEE: WARNING: killing 21033 states (over memory cap)
KLEE: WARNING: killing 19631 states (over memory cap)
KLEE: WARNING: killing 20906 states (over memory cap)
KLEE: WARNING: killing 20198 states (over memory cap)
KLEE: WARNING: killing 20712 states (over memory cap)
KLEE: WARNING: killing 19783 states (over memory cap)
KLEE: WARNING: killing 20592 states (over memory cap)
KLEE: WARNING: killing 20342 states (over memory cap)
KLEE: WARNING: killing 20555 states (over memory cap)
KLEE: WARNING: killing 20148 states (over memory cap)
KLEE: WARNING: killing 19900 states (over memory cap)
KLEE: WARNING: killing 20113 states (over memory cap)
KLEE: WARNING: killing 20162 states (over memory cap)
KLEE: WARNING: killing 20434 states (over memory cap)
KLEE: WARNING: killing 20718 states (over memory cap)
KLEE: WARNING: killing 20172 states (over memory cap)
KLEE: WARNING: killing 20670 states (over memory cap)
KLEE: WARNING: killing 19745 states (over memory cap)
KLEE: WARNING: killing 20779 states (over memory cap)
KLEE: WARNING: killing 19261 states (over memory cap)
KLEE: WARNING: killing 21420 states (over memory cap)
KLEE: WARNING: killing 19225 states (over memory cap)
KLEE: WARNING: killing 20780 states (over memory cap)
KLEE: WARNING: killing 20609 states (over memory cap)
KLEE: WARNING: killing 20812 states (over memory cap)
KLEE: WARNING: killing 20043 states (over memory cap)
KLEE: WARNING: killing 20174 states (over memory cap)
KLEE: WARNING: killing 20000 states (over memory cap)
KLEE: WARNING: killing 21175 states (over memory cap)
KLEE: WARNING: killing 20706 states (over memory cap)
KLEE: WARNING: killing 20090 states (over memory cap)
KLEE: WARNING: killing 20812 states (over memory cap)
KLEE: WARNING: killing 19603 states (over memory cap)
KLEE: WARNING: killing 20183 states (over memory cap)
KLEE: WARNING: killing 19639 states (over memory cap)
KLEE: WARNING: killing 20651 states (over memory cap)
KLEE: WARNING: killing 21514 states (over memory cap)
KLEE: WARNING: killing 20311 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:10275: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20883 states (over memory cap)
KLEE: WARNING: killing 19841 states (over memory cap)
KLEE: WARNING: killing 20563 states (over memory cap)
KLEE: WARNING: killing 20103 states (over memory cap)
KLEE: WARNING: killing 19566 states (over memory cap)
KLEE: WARNING: killing 20729 states (over memory cap)
KLEE: WARNING: killing 20858 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-InYtOe/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c:9930: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20472 states (over memory cap)
KLEE: WARNING: killing 20600 states (over memory cap)
KLEE: WARNING: killing 19625 states (over memory cap)
KLEE: WARNING: killing 19677 states (over memory cap)
KLEE: WARNING: killing 20108 states (over memory cap)
KLEE: WARNING: killing 20014 states (over memory cap)
KLEE: WARNING: killing 20934 states (over memory cap)
KLEE: WARNING: killing 19971 states (over memory cap)
KLEE: WARNING: killing 20748 states (over memory cap)
KLEE: WARNING: killing 20372 states (over memory cap)
KLEE: WARNING: killing 20426 states (over memory cap)
KLEE: WARNING: killing 20043 states (over memory cap)
KLEE: WARNING: killing 19881 states (over memory cap)
KLEE: WARNING: killing 21093 states (over memory cap)
KLEE: WARNING: killing 21440 states (over memory cap)
KLEE: WARNING: killing 19759 states (over memory cap)
KLEE: WARNING: killing 20974 states (over memory cap)
KLEE: WARNING: killing 20383 states (over memory cap)
KLEE: WARNING: killing 20503 states (over memory cap)
KLEE: WARNING: killing 20129 states (over memory cap)
KLEE: WARNING: killing 20256 states (over memory cap)
KLEE: WARNING: killing 19948 states (over memory cap)
KLEE: WARNING: killing 20285 states (over memory cap)
KLEE: WARNING: killing 20346 states (over memory cap)
KLEE: WARNING: killing 20465 states (over memory cap)
KLEE: WARNING: killing 20230 states (over memory cap)
KLEE: WARNING: killing 20435 states (over memory cap)
KLEE: WARNING: killing 20269 states (over memory cap)
KLEE: WARNING: killing 19964 states (over memory cap)
KLEE: WARNING: killing 19442 states (over memory cap)
KLEE: WARNING: killing 19709 states (over memory cap)
KLEE: WARNING: killing 20335 states (over memory cap)
KLEE: WARNING: killing 20534 states (over memory cap)
KLEE: WARNING: killing 21441 states (over memory cap)
KLEE: WARNING: killing 20221 states (over memory cap)
KLEE: WARNING: killing 20780 states (over memory cap)
KLEE: WARNING: killing 20331 states (over memory cap)
KLEE: WARNING: killing 20317 states (over memory cap)
KLEE: WARNING: killing 20012 states (over memory cap)
KLEE: WARNING: killing 20557 states (over memory cap)
KLEE: WARNING: killing 20973 states (over memory cap)
KLEE: WARNING: killing 20384 states (over memory cap)
