bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.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.: 367 859 6739 33199
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.30862784386
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)
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 zap_vma_ptes as symbolic
Removed calls to 'mmu_notifier_unregister' (function is undefined)
Removed calls to 'ldv_mmu_notifier_unregister' (function is undefined)
Defining function down_write_trylock 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 'ldv_after_alloc' (function is undefined)
Removed calls to '__mutex_init' (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 ldv___mmu_notifier_register as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_read_lock_held as symbolic
Defining function external_allocated_data as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function __bitmap_weight as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
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 'free_pages' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'proc_remove' (function is undefined)
Defining function misc_deregister as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'uv_teardown_irq' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function is_uv_system as symbolic
Removed calls to '__init_rwsem' (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 snprintf as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  __memcpy
  __memset
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 1.25968909264
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 544 638 2936 17578
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_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_ktest" has inline asm
KLEE: WARNING ONCE: function "gru_dump_chiplet_request" has inline asm
KLEE: WARNING ONCE: function "gru_wait_async_cbr" has inline asm
KLEE: WARNING ONCE: function "gru_find_lock_gts" has inline asm
KLEE: WARNING ONCE: function "gru_unlock_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_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 "ldv_EMGentry_exit_gru_exit_20_2" has inline asm
KLEE: WARNING ONCE: function "gru_chiplet_cpu_to_mmr" has inline asm
KLEE: WARNING ONCE: function "gru_kservices_exit" has inline asm
KLEE: WARNING ONCE: function "ldv_EMGentry_init_gru_init_20_10" 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_get_cb_exception_detail_str" has inline asm
KLEE: WARNING ONCE: function "tfh_restart" has inline asm
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:5555: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
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_ce266ebd-45cc-4de4-bfba-e04db350f545/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: MO63[8192] allocated at global:gru_base
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:5583: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:15047: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:5805: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:15271: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:11808: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:11223: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NdKjHe/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko_false-unreach-call.cil.c:5589: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
