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--misc--sgi-gru--gru.ko-entry_point_true-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.: 362 476 3796 22756
Removed infinite loop in gru_load_context
Removed infinite loop in gru_load_mm_tracker
Removed infinite loop in paravirt_read_tsc___1
Removed infinite loop in paravirt_read_tsc
Removed infinite loop in gru_unload_context
Removed infinite loop in gru_unload_mm_tracker
Removed infinite loop in gru_free_gru_context
Removed infinite loop in reserve_resources
Removed infinite loop in gru_update_cch
Removed infinite loop in gru_send_message_gpa
Removed infinite loop in gru_get_cpu_resources
Removed infinite loop in send_message_failure
Removed infinite loop in send_noop_message
Removed infinite loop in gru_get_cb_exception_detail
Removed infinite loop in quicktest2
Removed infinite loop in paravirt_read_tsc___0
Removed infinite loop in pte_val
Removed infinite loop in pmd_val
Removed infinite loop in pud_val
Removed infinite loop in pgd_val
Removed infinite loop in ldv_stop
Removed infinite loop in gru_chiplet_cpu_to_mmr
Removed infinite loop in gru_kservices_exit
INFO: Compilation, preparation and instrumentation time: 0.790396928787
Removed calls to 'list_del' (function is undefined)
Defining function printk as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function schedule_timeout as symbolic
Removed calls to 'up_write' (function is undefined)
Defining function remap_pfn_range as symbolic
Removed calls to 'panic' (function is undefined)
Defining function find_first_bit as symbolic
Defining function find_next_bit as symbolic
Defining function zap_vma_ptes as symbolic
Removed calls to 'mmu_notifier_unregister' (function is undefined)
Defining function down_write_trylock as symbolic
Defining function mutex_trylock as symbolic
Defining function find_first_zero_bit as symbolic
Defining function __phys_addr as symbolic
Removed calls to 'up_read' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'downgrade_write' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function __mmu_notifier_register as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function noop_llseek as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function __bitmap_weight as symbolic
Defining function find_vma as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to 'put_page' (function is undefined)
Defining function get_user_pages as symbolic
Defining function capable as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function kstrtoul_from_user as symbolic
Defining function seq_release as symbolic
Defining function seq_open as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Defining function ldv_open_9 as symbolic
Defining function ldv_open_10 as symbolic
Defining function ldv_release_10 as symbolic
Defining function misc_deregister as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'proc_remove' (function is undefined)
Removed calls to 'uv_teardown_irq' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function down_read_trylock as symbolic
Defining function uv_setup_irq as symbolic
Defining function request_threaded_irq as symbolic
Defining function __alloc_pages_nodemask as symbolic
Defining function proc_mkdir as symbolic
Defining function proc_create_data as symbolic
Defining function misc_register as symbolic
Defining function is_uv_system as symbolic
Defining function ldv_probe_8 as symbolic
Defining function snprintf as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __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.938950061798
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 496 313 1857 13338
INFO: Starting verification
KLEE: WARNING ONCE: function "gru_vma_close" has inline asm
KLEE: WARNING ONCE: function "gru_fault" has inline asm
KLEE: WARNING ONCE: function "gru_find_thread_state" has inline asm
KLEE: WARNING ONCE: function "gru_check_context_placement" has inline asm
KLEE: WARNING ONCE: function "gru_assign_gru_context" has inline asm
KLEE: WARNING ONCE: function "gru_steal_context" has inline asm
KLEE: WARNING ONCE: function "gru_load_context" has inline asm
KLEE: WARNING ONCE: function "gru_wrap_asid" has inline asm
KLEE: WARNING ONCE: function "gru_flush_all_tlb" has inline asm
KLEE: WARNING ONCE: function "wait_instruction_complete" has inline asm
KLEE: WARNING ONCE: function "gru_prefetch_context" has inline asm
KLEE: WARNING ONCE: function "get_cycles___1" has inline asm
KLEE: WARNING ONCE: function "get_lock_tgh_handle" has inline asm
KLEE: WARNING ONCE: function "gru_check_chiplet_assignment" has inline asm
KLEE: WARNING ONCE: function "gru_unload_context" has inline asm
KLEE: WARNING ONCE: function "gts_drop" has inline asm
KLEE: WARNING ONCE: function "gru_drop_mmu_notifier" has inline asm
KLEE: WARNING ONCE: function "reserve_resources" has inline asm
KLEE: WARNING ONCE: function "gru_update_cch" has inline asm
KLEE: WARNING ONCE: function "uv_soc_phys_ram_to_gpa" has inline asm
KLEE: WARNING ONCE: function "gru_send_message_gpa" has inline asm
KLEE: WARNING ONCE: function "gru_get_cpu_resources" has inline asm
KLEE: WARNING ONCE: function "gru_wait_proc" has inline asm
KLEE: WARNING ONCE: function "gru_unlock_kernel_context" has inline asm
KLEE: WARNING ONCE: function "gru_retry_exception" has inline asm
KLEE: WARNING ONCE: function "gru_get_cb_exception_detail" has inline asm
KLEE: WARNING ONCE: function "gru_lock_kernel_context" has inline asm
KLEE: WARNING ONCE: function "gru_alloc_gts" has inline asm
KLEE: WARNING ONCE: function "gru_register_mmu_notifier" has inline asm
KLEE: WARNING ONCE: function "gru_get_next_message" has inline asm
KLEE: WARNING ONCE: function "gru_read_gpa" has inline asm
KLEE: WARNING ONCE: function "gru_copy_gpa" has inline asm
KLEE: WARNING ONCE: function "gru_file_unlocked_ioctl" has inline asm
KLEE: WARNING ONCE: function "gru_file_mmap" has inline asm
KLEE: WARNING ONCE: function "gru_alloc_vma_data" has inline asm
KLEE: WARNING ONCE: function "gru_find_vma" has inline asm
KLEE: WARNING ONCE: function "gru_set_context_option" has inline asm
KLEE: WARNING ONCE: function "gru_get_exception_detail" has inline asm
KLEE: WARNING ONCE: function "gru_user_unload_context" has inline asm
KLEE: WARNING ONCE: function "gru_user_flush_tlb" has inline asm
KLEE: WARNING ONCE: function "gru_handle_user_call_os" has inline asm
KLEE: WARNING ONCE: function "gru_get_gseg_statistics" has inline asm
KLEE: WARNING ONCE: function "gru_ktest" has inline asm
KLEE: WARNING ONCE: function "gru_dump_chiplet_request" has inline asm
KLEE: WARNING ONCE: function "gru_find_lock_gts" has inline asm
KLEE: WARNING ONCE: function "gru_try_dropin" has inline asm
KLEE: WARNING ONCE: function "gru_vtop" has inline asm
KLEE: WARNING ONCE: function "tfh_write_only" has inline asm
KLEE: WARNING ONCE: function "tfh_write_restart" has inline asm
KLEE: WARNING ONCE: function "gru_flush_tlb_range" has inline asm
KLEE: WARNING ONCE: function "tgh_invalidate" has inline asm
KLEE: WARNING ONCE: function "gru_alloc_thread_state" has inline asm
KLEE: WARNING ONCE: function "gru_release" has inline asm
KLEE: WARNING ONCE: function "gru_invalidate_page" has inline asm
KLEE: WARNING ONCE: function "gru_invalidate_range_start" has inline asm
KLEE: WARNING ONCE: function "gru_invalidate_range_end" has inline asm
KLEE: WARNING ONCE: function "gru_seq_show" has inline asm
KLEE: WARNING ONCE: function "gru_cpu_fault_map_id" has inline asm
KLEE: WARNING ONCE: function "cch_allocate" has inline asm
KLEE: WARNING ONCE: function "cch_start" has inline asm
KLEE: WARNING ONCE: function "cch_interrupt_sync" has inline asm
KLEE: WARNING ONCE: function "cch_deallocate" has inline asm
KLEE: WARNING ONCE: function "cch_interrupt" has inline asm
KLEE: WARNING ONCE: function "gru_wait_async_cbr" has inline asm
KLEE: WARNING ONCE: function "gru_check_status_proc" has inline asm
KLEE: WARNING ONCE: function "tfh_user_polling_mode" has inline asm
KLEE: WARNING ONCE: function "tfh_exception" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "gru_kservices_exit" has inline asm
KLEE: WARNING ONCE: function "gru_tgh_flush_init" has inline asm
KLEE: WARNING ONCE: function "gru1_intr" has inline asm
KLEE: WARNING ONCE: function "gru0_intr" has inline asm
KLEE: WARNING ONCE: function "gru_intr" has inline asm
KLEE: WARNING ONCE: function "gru_chiplet_cpu_to_mmr" has inline asm
KLEE: WARNING ONCE: function "gru_get_cb_exception_detail_str" has inline asm
KLEE: WARNING ONCE: function "tfh_restart" has inline asm
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_6df35bf5-6f96-46d2-a5da-cc29f2efe36f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MiYZmZ/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c:4731: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-MiYZmZ/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c:7922: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19472 states (over memory cap)
KLEE: WARNING: killing 16044 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MiYZmZ/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c:6388: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15626 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MiYZmZ/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c:14344: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14399 states (over memory cap)
KLEE: WARNING: killing 14960 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 15543 states (over memory cap)
KLEE: WARNING: killing 15134 states (over memory cap)
KLEE: WARNING: killing 15431 states (over memory cap)
KLEE: WARNING: killing 16100 states (over memory cap)
KLEE: WARNING: killing 17202 states (over memory cap)
KLEE: WARNING: killing 16539 states (over memory cap)
KLEE: WARNING: killing 17264 states (over memory cap)
KLEE: WARNING: killing 18097 states (over memory cap)
KLEE: WARNING: killing 16215 states (over memory cap)
KLEE: WARNING: killing 16826 states (over memory cap)
KLEE: WARNING: killing 15800 states (over memory cap)
KLEE: WARNING: killing 16521 states (over memory cap)
KLEE: WARNING: killing 15436 states (over memory cap)
KLEE: WARNING: killing 15833 states (over memory cap)
KLEE: WARNING: killing 16761 states (over memory cap)
KLEE: WARNING: killing 15952 states (over memory cap)
KLEE: WARNING: killing 15981 states (over memory cap)
KLEE: WARNING: killing 16377 states (over memory cap)
KLEE: WARNING: killing 16622 states (over memory cap)
KLEE: WARNING: killing 16650 states (over memory cap)
KLEE: WARNING: killing 17160 states (over memory cap)
KLEE: WARNING: killing 15512 states (over memory cap)
KLEE: WARNING: killing 16012 states (over memory cap)
KLEE: WARNING: killing 15834 states (over memory cap)
KLEE: WARNING: killing 15662 states (over memory cap)
KLEE: WARNING: killing 16624 states (over memory cap)
KLEE: WARNING: killing 16297 states (over memory cap)
KLEE: WARNING: killing 16482 states (over memory cap)
KLEE: WARNING: killing 16984 states (over memory cap)
KLEE: WARNING: killing 16659 states (over memory cap)
KLEE: WARNING: killing 16689 states (over memory cap)
KLEE: WARNING: killing 15788 states (over memory cap)
KLEE: WARNING: killing 16233 states (over memory cap)
KLEE: WARNING: killing 15910 states (over memory cap)
KLEE: WARNING: killing 16248 states (over memory cap)
KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: MO53[8192] allocated at global:gru_base
KLEE: WARNING: killing 16893 states (over memory cap)
KLEE: WARNING: killing 17061 states (over memory cap)
KLEE: WARNING: killing 16424 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15768 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MiYZmZ/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c:14854: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16568 states (over memory cap)
KLEE: WARNING: killing 16811 states (over memory cap)
KLEE: WARNING: killing 16796 states (over memory cap)
KLEE: WARNING: killing 15850 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 16323 states (over memory cap)
KLEE: WARNING: killing 16610 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MiYZmZ/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c:15547: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 16764 states (over memory cap)
KLEE: WARNING: killing 15779 states (over memory cap)
KLEE: WARNING: killing 16065 states (over memory cap)
KLEE: WARNING: killing 16353 states (over memory cap)
KLEE: WARNING: killing 15676 states (over memory cap)
KLEE: WARNING: killing 16876 states (over memory cap)
KLEE: WARNING: killing 16561 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 16773 states (over memory cap)
KLEE: WARNING: killing 16856 states (over memory cap)
KLEE: WARNING: killing 16135 states (over memory cap)
KLEE: WARNING: killing 16670 states (over memory cap)
KLEE: WARNING: killing 16356 states (over memory cap)
KLEE: WARNING: killing 15993 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 15687 states (over memory cap)
KLEE: WARNING: killing 16520 states (over memory cap)
KLEE: WARNING: killing 16357 states (over memory cap)
KLEE: WARNING: killing 17144 states (over memory cap)
KLEE: WARNING: killing 16434 states (over memory cap)
KLEE: WARNING: killing 15417 states (over memory cap)
KLEE: WARNING: killing 15698 states (over memory cap)
KLEE: WARNING: killing 16376 states (over memory cap)
KLEE: WARNING: killing 16508 states (over memory cap)
KLEE: WARNING: killing 16897 states (over memory cap)
KLEE: WARNING: killing 16086 states (over memory cap)
KLEE: WARNING: killing 15721 states (over memory cap)
KLEE: WARNING: killing 16104 states (over memory cap)
KLEE: WARNING: killing 16587 states (over memory cap)
KLEE: WARNING: killing 16076 states (over memory cap)
KLEE: WARNING: killing 15860 states (over memory cap)
KLEE: WARNING: killing 16539 states (over memory cap)
KLEE: WARNING: killing 15679 states (over memory cap)
KLEE: WARNING: killing 15813 states (over memory cap)
KLEE: WARNING: killing 16582 states (over memory cap)
KLEE: WARNING: killing 16966 states (over memory cap)
KLEE: WARNING: killing 16562 states (over memory cap)
KLEE: WARNING: killing 16208 states (over memory cap)
KLEE: WARNING: killing 16436 states (over memory cap)
KLEE: WARNING: killing 16278 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
KLEE: WARNING: killing 15800 states (over memory cap)
KLEE: WARNING: killing 15737 states (over memory cap)
KLEE: WARNING: killing 16113 states (over memory cap)
KLEE: WARNING: killing 17177 states (over memory cap)
KLEE: WARNING: killing 16094 states (over memory cap)
KLEE: WARNING: killing 15784 states (over memory cap)
KLEE: WARNING: killing 16117 states (over memory cap)
KLEE: WARNING: killing 16341 states (over memory cap)
KLEE: WARNING: killing 16284 states (over memory cap)
KLEE: WARNING: killing 15682 states (over memory cap)
KLEE: WARNING: killing 16929 states (over memory cap)
KLEE: WARNING: killing 16725 states (over memory cap)
KLEE: WARNING: killing 16273 states (over memory cap)
KLEE: WARNING: killing 17234 states (over memory cap)
KLEE: WARNING: killing 15431 states (over memory cap)
KLEE: WARNING: killing 15558 states (over memory cap)
KLEE: WARNING: killing 15346 states (over memory cap)
KLEE: WARNING: killing 16250 states (over memory cap)
KLEE: WARNING: killing 15846 states (over memory cap)
KLEE: WARNING: killing 16074 states (over memory cap)
KLEE: WARNING: killing 16638 states (over memory cap)
KLEE: WARNING: killing 16434 states (over memory cap)
KLEE: WARNING: killing 15510 states (over memory cap)
KLEE: WARNING: killing 16261 states (over memory cap)
KLEE: WARNING: killing 16444 states (over memory cap)
KLEE: WARNING: killing 16480 states (over memory cap)
KLEE: WARNING: killing 16266 states (over memory cap)
KLEE: WARNING: killing 16546 states (over memory cap)
KLEE: WARNING: killing 15576 states (over memory cap)
KLEE: WARNING: killing 15941 states (over memory cap)
KLEE: WARNING: killing 16498 states (over memory cap)
KLEE: WARNING: killing 16243 states (over memory cap)
KLEE: WARNING: killing 16331 states (over memory cap)
KLEE: WARNING: killing 16557 states (over memory cap)
KLEE: WARNING: killing 16538 states (over memory cap)
KLEE: WARNING: killing 16768 states (over memory cap)
KLEE: WARNING: killing 15507 states (over memory cap)
KLEE: WARNING: killing 15922 states (over memory cap)
KLEE: WARNING: killing 16331 states (over memory cap)
KLEE: WARNING: killing 15937 states (over memory cap)
KLEE: WARNING: killing 16495 states (over memory cap)
KLEE: WARNING: killing 15910 states (over memory cap)
KLEE: WARNING: killing 15794 states (over memory cap)
KLEE: WARNING: killing 15876 states (over memory cap)
KLEE: WARNING: killing 16469 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 16300 states (over memory cap)
KLEE: WARNING: killing 16002 states (over memory cap)
KLEE: WARNING: killing 16416 states (over memory cap)
