theory CToCRefine

theorem spec_refine:
  notes if_split[split del]
  shows
  "spec_statefn_simulates id (kernel_all_global_addresses.\<Gamma> symbol_table)
     (kernel_all_substitute.\<Gamma> symbol_table domain)" apply (simp add: kernel_all_global_addresses.\<Gamma>_def kernel_all_substitute.\<Gamma>_def) apply (intro spec_statefn_simulates_lookup_tree_Node spec_statefn_simulates_lookup_tree_Leaf) apply (tactic \<open>ALLGOALS (asm_simp_tac (put_simpset HOL_ss @{context} addsimps @{thms switch.simps fst_conv snd_conv}
                  addsimprocs [unfold_bodies] |> Splitter.del_split @{thm if_split}))
              THEN ALLGOALS (TRY o resolve_tac @{context} @{thms exec_statefn_simulates_refl})\<close>) apply (tactic \<open>ALLGOALS (REPEAT_ALL_NEW (resolve_tac @{context} @{thms exec_statefn_simulates_comI
                      exec_statefn_simulates_additionals}))\<close>) apply (unfold id_apply) apply (tactic \<open>ALLGOALS (TRY o resolve_tac @{context} @{thms refl bij_id})\<close>) apply (tactic \<open>ALLGOALS (TRY o (resolve_tac @{context} @{thms subsetI} THEN' resolve_tac @{context} @{thms CollectI}
           THEN' REPEAT_ALL_NEW (eresolve_tac @{context} @{thms IntE CollectE conjE exE h_t_valid_c_guard conjI} ORELSE' assume_tac @{context})))\<close>) 
  (*
    apply (tactic {* ALLGOALS (TRY o ((REPEAT_ALL_NEW (rtac @{thm c_guard_field}) THEN' etac @{thm h_t_valid_c_guard})
                          THEN_ALL_NEW simp_tac @{simpset}
                          THEN_ALL_NEW simp_tac @{simpset}
                          THEN_ALL_NEW K no_tac))  *})
  *)
   apply (rule bij_id[simplified id_def])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_statefn_simulates id (kernel_all_global_addresses.\<Gamma> symbol_table) (kernel_all_substitute.\<Gamma> symbol_table domain) proof (prove)
goal (1 subgoal):
 1. spec_statefn_simulates id (lookup_tree (Tree.Node map_kernel_devices_'proc (kernel_all_global_addresses.map_kernel_devices_body symbol_table) (Tree.Node thread_state_ptr_set_tsType_'proc kernel_all_global_addresses.thread_state_ptr_set_tsType_body (Tree.Node seL4_Fault_UserException_get_code_'proc kernel_all_global_addresses.seL4_Fault_UserException_get_code_body (Tree.Node pde_pde_invalid_get_stored_asid_valid_'proc kernel_all_global_addresses.pde_pde_invalid_get_stored_asid_valid_body (Tree.Node thread_state_ptr_set_blockingIPCCanGrant_'proc kernel_all_global_addresses.thread_state_ptr_set_blockingIPCCanGrant_body (Tree.Node cap_small_frame_cap_get_capFMappedASIDHigh_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFMappedASIDHigh_body (Tree.Node cap_page_directory_cap_ptr_set_capPDIsMapped_'proc kernel_all_global_addresses.cap_page_directory_cap_ptr_set_capPDIsMapped_body (Tree.Node thread_state_ptr_set_blockingIPCCanGrantReply_'proc kernel_all_global_addresses.thread_state_ptr_set_blockingIPCCanGrantReply_body (Tree.Node cap_page_directory_cap_ptr_set_capPDMappedASID_'proc kernel_all_global_addresses.cap_page_directory_cap_ptr_set_capPDMappedASID_body (Tree.Node mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_'proc kernel_all_global_addresses.mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_body Leaf Leaf) Leaf) (Tree.Node lookup_fault_missing_capability_get_bitsLeft_'proc kernel_all_global_addresses.lookup_fault_missing_capability_get_bitsLeft_body (Tree.Node thread_state_ptr_get_blockingIPCCanGrantReply_'proc kernel_all_global_addresses.thread_state_ptr_get_blockingIPCCanGrantReply_body Leaf Leaf) Leaf)) (Tree.Node generic_frame_cap_ptr_set_capFMappedAddress_'proc kernel_all_global_addresses.generic_frame_cap_ptr_set_capFMappedAddress_body (Tree.Node seL4_Fault_UnknownSyscall_get_syscallNumber_'proc kernel_all_global_addresses.seL4_Fault_UnknownSyscall_get_syscallNumber_body (Tree.Node thread_state_ptr_mset_blockingObject_tsType_'proc kernel_all_global_addresses.thread_state_ptr_mset_blockingObject_tsType_body Leaf Leaf) Leaf) (Tree.Node cap_small_frame_cap_set_capFMappedASIDHigh_'proc kernel_all_global_addresses.cap_small_frame_cap_set_capFMappedASIDHigh_body (Tree.Node lookup_fault_guard_mismatch_get_guardFound_'proc kernel_all_global_addresses.lookup_fault_guard_mismatch_get_guardFound_body Leaf Leaf) Leaf))) (Tree.Node cap_small_frame_cap_set_capFMappedAddress_'proc kernel_all_global_addresses.cap_small_frame_cap_set_capFMappedAddress_body (Tree.Node cap_notification_cap_get_capNtfnCanReceive_'proc kernel_all_global_addresses.cap_notification_cap_get_capNtfnCanReceive_body (Tree.Node cap_notification_cap_set_capNtfnCanReceive_'proc kernel_all_global_addresses.cap_notification_cap_set_capNtfnCanReceive_body (Tree.Node cap_page_directory_cap_get_capPDMappedASID_'proc kernel_all_global_addresses.cap_page_directory_cap_get_capPDMappedASID_body Leaf Leaf) Leaf) (Tree.Node lookup_fault_depth_mismatch_get_bitsFound_'proc kernel_all_global_addresses.lookup_fault_depth_mismatch_get_bitsFound_body (Tree.Node lookup_fault_guard_mismatch_get_bitsFound_'proc kernel_all_global_addresses.lookup_fault_guard_mismatch_get_bitsFound_body Leaf Leaf) Leaf)) (Tree.Node cap_small_frame_cap_get_capFMappedASIDLow_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFMappedASIDLow_body (Tree.Node cap_small_frame_cap_get_capFMappedAddress_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFMappedAddress_body (Tree.Node cap_small_frame_cap_set_capFMappedASIDLow_'proc kernel_all_global_addresses.cap_small_frame_cap_set_capFMappedASIDLow_body Leaf Leaf) Leaf) (Tree.Node cap_page_table_cap_get_capPTMappedAddress_'proc kernel_all_global_addresses.cap_page_table_cap_get_capPTMappedAddress_body (Tree.Node cap_page_table_cap_set_capPTMappedAddress_'proc kernel_all_global_addresses.cap_page_table_cap_set_capPTMappedAddress_body Leaf Leaf) Leaf)))) (Tree.Node thread_state_ptr_set_blockingIPCIsCall_'proc kernel_all_global_addresses.thread_state_ptr_set_blockingIPCIsCall_body (Tree.Node seL4_Fault_VMFault_get_instructionFault_'proc kernel_all_global_addresses.seL4_Fault_VMFault_get_instructionFault_body (Tree.Node lookup_fault_depth_mismatch_get_bitsLeft_'proc kernel_all_global_addresses.lookup_fault_depth_mismatch_get_bitsLeft_body (Tree.Node lookup_fault_guard_mismatch_get_bitsLeft_'proc kernel_all_global_addresses.lookup_fault_guard_mismatch_get_bitsLeft_body (Tree.Node thread_state_ptr_get_blockingIPCCanGrant_'proc kernel_all_global_addresses.thread_state_ptr_get_blockingIPCCanGrant_body Leaf Leaf) Leaf) (Tree.Node cap_page_directory_cap_get_capPDIsMapped_'proc kernel_all_global_addresses.cap_page_directory_cap_get_capPDIsMapped_body (Tree.Node cap_page_table_cap_ptr_set_capPTIsMapped_'proc kernel_all_global_addresses.cap_page_table_cap_ptr_set_capPTIsMapped_body Leaf Leaf) Leaf)) (Tree.Node cap_page_directory_cap_get_capPDBasePtr_'proc kernel_all_global_addresses.cap_page_directory_cap_get_capPDBasePtr_body (Tree.Node generic_frame_cap_get_capFMappedAddress_'proc kernel_all_global_addresses.generic_frame_cap_get_capFMappedAddress_body (Tree.Node generic_frame_cap_set_capFMappedAddress_'proc kernel_all_global_addresses.generic_frame_cap_set_capFMappedAddress_body Leaf Leaf) Leaf) (Tree.Node cap_notification_cap_get_capNtfnCanSend_'proc kernel_all_global_addresses.cap_notification_cap_get_capNtfnCanSend_body (Tree.Node cap_notification_cap_set_capNtfnCanSend_'proc kernel_all_global_addresses.cap_notification_cap_set_capNtfnCanSend_body Leaf Leaf) Leaf))) (Tree.Node cap_small_frame_cap_get_capFMappedASID_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFMappedASID_body (Tree.Node notification_ptr_set_ntfnMsgIdentifier_'proc kernel_all_global_addresses.notification_ptr_set_ntfnMsgIdentifier_body (Tree.Node seL4_Fault_CapFault_get_inReceivePhase_'proc kernel_all_global_addresses.seL4_Fault_CapFault_get_inReceivePhase_body (Tree.Node thread_state_ptr_get_blockingIPCIsCall_'proc kernel_all_global_addresses.thread_state_ptr_get_blockingIPCIsCall_body Leaf Leaf) Leaf) (Tree.Node cap_small_frame_cap_set_capFMappedASID_'proc kernel_all_global_addresses.cap_small_frame_cap_set_capFMappedASID_body (Tree.Node notification_ptr_get_ntfnMsgIdentifier_'proc kernel_all_global_addresses.notification_ptr_get_ntfnMsgIdentifier_body Leaf Leaf) Leaf)) (Tree.Node thread_state_ptr_set_blockingIPCBadge_'proc kernel_all_global_addresses.thread_state_ptr_set_blockingIPCBadge_body (Tree.Node cap_page_table_cap_get_capPTMappedASID_'proc kernel_all_global_addresses.cap_page_table_cap_get_capPTMappedASID_body (Tree.Node cap_page_table_cap_set_capPTMappedASID_'proc kernel_all_global_addresses.cap_page_table_cap_set_capPTMappedASID_body Leaf Leaf) Leaf) (Tree.Node seL4_CapRights_get_capAllowGrantReply_'proc kernel_all_global_addresses.seL4_CapRights_get_capAllowGrantReply_body (Tree.Node thread_state_ptr_get_blockingIPCBadge_'proc kernel_all_global_addresses.thread_state_ptr_get_blockingIPCBadge_body Leaf Leaf) Leaf))))) (Tree.Node cap_page_table_cap_get_capPTBasePtr_'proc kernel_all_global_addresses.cap_page_table_cap_get_capPTBasePtr_body (Tree.Node cap_page_table_cap_get_capPTIsMapped_'proc kernel_all_global_addresses.cap_page_table_cap_get_capPTIsMapped_body (Tree.Node endpoint_ptr_mset_epQueue_tail_state_'proc kernel_all_global_addresses.endpoint_ptr_mset_epQueue_tail_state_body (Tree.Node cap_endpoint_cap_set_capCanGrantReply_'proc kernel_all_global_addresses.cap_endpoint_cap_set_capCanGrantReply_body (Tree.Node cap_notification_cap_get_capNtfnBadge_'proc kernel_all_global_addresses.cap_notification_cap_get_capNtfnBadge_body (Tree.Node cap_notification_cap_set_capNtfnBadge_'proc kernel_all_global_addresses.cap_notification_cap_set_capNtfnBadge_body Leaf Leaf) Leaf) (Tree.Node generic_frame_cap_get_capFMappedASID_'proc kernel_all_global_addresses.generic_frame_cap_get_capFMappedASID_body (Tree.Node cap_endpoint_cap_get_capCanGrantReply_'proc kernel_all_global_addresses.cap_endpoint_cap_get_capCanGrantReply_body Leaf Leaf) Leaf)) (Tree.Node cap_small_frame_cap_get_capFVMRights_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFVMRights_body (Tree.Node cap_small_frame_cap_set_capFVMRights_'proc kernel_all_global_addresses.cap_small_frame_cap_set_capFVMRights_body (Tree.Node cap_untyped_cap_ptr_set_capFreeIndex_'proc kernel_all_global_addresses.cap_untyped_cap_ptr_set_capFreeIndex_body Leaf Leaf) Leaf) (Tree.Node cap_page_table_cap_set_capPTIsMapped_'proc kernel_all_global_addresses.cap_page_table_cap_set_capPTIsMapped_body (Tree.Node cap_small_frame_cap_get_capFIsDevice_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFIsDevice_body Leaf Leaf) Leaf))) (Tree.Node notification_ptr_set_ntfnQueue_tail_'proc kernel_all_global_addresses.notification_ptr_set_ntfnQueue_tail_body (Tree.Node thread_state_ptr_set_blockingObject_'proc kernel_all_global_addresses.thread_state_ptr_set_blockingObject_body (Tree.Node cap_frame_cap_get_capFMappedASIDHigh_'proc kernel_all_global_addresses.cap_frame_cap_get_capFMappedASIDHigh_body (Tree.Node cap_frame_cap_set_capFMappedASIDHigh_'proc kernel_all_global_addresses.cap_frame_cap_set_capFMappedASIDHigh_body Leaf Leaf) Leaf) (Tree.Node seL4_Fault_UserException_get_number_'proc kernel_all_global_addresses.seL4_Fault_UserException_get_number_body (Tree.Node thread_state_ptr_get_blockingObject_'proc kernel_all_global_addresses.thread_state_ptr_get_blockingObject_body Leaf Leaf) Leaf)) (Tree.Node notification_ptr_get_ntfnQueue_head_'proc kernel_all_global_addresses.notification_ptr_get_ntfnQueue_head_body (Tree.Node notification_ptr_get_ntfnQueue_tail_'proc kernel_all_global_addresses.notification_ptr_get_ntfnQueue_tail_body (Tree.Node notification_ptr_set_ntfnQueue_head_'proc kernel_all_global_addresses.notification_ptr_set_ntfnQueue_head_body Leaf Leaf) Leaf) (Tree.Node cap_small_frame_cap_get_capFBasePtr_'proc kernel_all_global_addresses.cap_small_frame_cap_get_capFBasePtr_body (Tree.Node lookup_fault_missing_capability_new_'proc kernel_all_global_addresses.lookup_fault_missing_capability_new_body Leaf Leaf) Leaf)))) (Tree.Node pde_pde_invalid_get_stored_hw_asid_'proc kernel_all_global_addresses.pde_pde_invalid_get_stored_hw_asid_body (Tree.Node cap_cnode_cap_set_capCNodeGuardSize_'proc kernel_all_global_addresses.cap_cnode_cap_set_capCNodeGuardSize_body (Tree.Node cap_frame_cap_set_capFMappedASIDLow_'proc kernel_all_global_addresses.cap_frame_cap_set_capFMappedASIDLow_body (Tree.Node cap_frame_cap_set_capFMappedAddress_'proc kernel_all_global_addresses.cap_frame_cap_set_capFMappedAddress_body (Tree.Node cap_notification_cap_get_capNtfnPtr_'proc kernel_all_global_addresses.cap_notification_cap_get_capNtfnPtr_body Leaf Leaf) Leaf) (Tree.Node cap_frame_cap_get_capFMappedASIDLow_'proc kernel_all_global_addresses.cap_frame_cap_get_capFMappedASIDLow_body (Tree.Node cap_frame_cap_get_capFMappedAddress_'proc kernel_all_global_addresses.cap_frame_cap_get_capFMappedAddress_body Leaf Leaf) Leaf)) (Tree.Node vm_attributes_get_armPageCacheable_'proc kernel_all_global_addresses.vm_attributes_get_armPageCacheable_body (Tree.Node vm_attributes_get_armParityEnabled_'proc kernel_all_global_addresses.vm_attributes_get_armParityEnabled_body (Tree.Node cap_cnode_cap_get_capCNodeGuardSize_'proc kernel_all_global_addresses.cap_cnode_cap_get_capCNodeGuardSize_body Leaf Leaf) Leaf) (Tree.Node seL4_MessageInfo_get_capsUnwrapped_'proc kernel_all_global_addresses.seL4_MessageInfo_get_capsUnwrapped_body (Tree.Node seL4_MessageInfo_set_capsUnwrapped_'proc kernel_all_global_addresses.seL4_MessageInfo_set_capsUnwrapped_body Leaf Leaf) Leaf))) (Tree.Node cap_reply_cap_set_capReplyCanGrant_'proc kernel_all_global_addresses.cap_reply_cap_set_capReplyCanGrant_body (Tree.Node generic_frame_cap_get_capFIsDevice_'proc kernel_all_global_addresses.generic_frame_cap_get_capFIsDevice_body (Tree.Node generic_frame_cap_get_capFIsMapped_'proc kernel_all_global_addresses.generic_frame_cap_get_capFIsMapped_body (Tree.Node generic_frame_cap_get_capFVMRights_'proc kernel_all_global_addresses.generic_frame_cap_get_capFVMRights_body Leaf Leaf) Leaf) (Tree.Node cap_zombie_cap_get_capZombieNumber_'proc kernel_all_global_addresses.cap_zombie_cap_get_capZombieNumber_body (Tree.Node cap_zombie_cap_set_capZombieNumber_'proc kernel_all_global_addresses.cap_zombie_cap_set_capZombieNumber_body Leaf Leaf) Leaf)) (Tree.Node cap_endpoint_cap_get_capCanReceive_'proc kernel_all_global_addresses.cap_endpoint_cap_get_capCanReceive_body (Tree.Node cap_endpoint_cap_set_capCanReceive_'proc kernel_all_global_addresses.cap_endpoint_cap_set_capCanReceive_body (Tree.Node cap_reply_cap_get_capReplyCanGrant_'proc kernel_all_global_addresses.cap_reply_cap_get_capReplyCanGrant_body Leaf Leaf) Leaf) (Tree.Node vm_attributes_get_armExecuteNever_'proc kernel_all_global_addresses.vm_attributes_get_armExecuteNever_body Leaf Leaf)))))) (Tree.Node pde_pde_coarse_ptr_get_address_'proc kernel_all_global_addresses.pde_pde_coarse_ptr_get_address_body (Tree.Node seL4_CapRights_get_capAllowRead_'proc kernel_all_global_addresses.seL4_CapRights_get_capAllowRead_body (Tree.Node decodeARMPageDirectoryInvocation_'proc kernel_all_global_addresses.decodeARMPageDirectoryInvocation_body (Tree.Node seL4_CapRights_get_capAllowWrite_'proc kernel_all_global_addresses.seL4_CapRights_get_capAllowWrite_body (Tree.Node generic_frame_cap_get_capFBasePtr_'proc kernel_all_global_addresses.generic_frame_cap_get_capFBasePtr_body (Tree.Node notification_ptr_get_ntfnBoundTCB_'proc kernel_all_global_addresses.notification_ptr_get_ntfnBoundTCB_body (Tree.Node notification_ptr_set_ntfnBoundTCB_'proc kernel_all_global_addresses.notification_ptr_set_ntfnBoundTCB_body Leaf Leaf) Leaf) (Tree.Node cap_asid_pool_cap_get_capASIDBase_'proc kernel_all_global_addresses.cap_asid_pool_cap_get_capASIDBase_body (Tree.Node cap_asid_pool_cap_get_capASIDPool_'proc kernel_all_global_addresses.cap_asid_pool_cap_get_capASIDPool_body Leaf Leaf) Leaf)) (Tree.Node invokeIRQHandler_ClearIRQHandler_'proc (kernel_all_global_addresses.invokeIRQHandler_ClearIRQHandler_body symbol_table) (Tree.Node seL4_CNode_CapData_get_guardSize_'proc kernel_all_global_addresses.seL4_CNode_CapData_get_guardSize_body (Tree.Node seL4_CapRights_get_capAllowGrant_'proc kernel_all_global_addresses.seL4_CapRights_get_capAllowGrant_body Leaf Leaf) Leaf) (Tree.Node endpoint_ptr_set_epQueue_head_np_'proc kernel_all_global_addresses.endpoint_ptr_set_epQueue_head_np_body (Tree.Node invalidateTranslationSingleLocal_'proc kernel_all_global_addresses.invalidateTranslationSingleLocal_body Leaf Leaf) Leaf))) (Tree.Node cap_reply_cap_get_capReplyMaster_'proc kernel_all_global_addresses.cap_reply_cap_get_capReplyMaster_body (Tree.Node cap_untyped_cap_set_capFreeIndex_'proc kernel_all_global_addresses.cap_untyped_cap_set_capFreeIndex_body (Tree.Node cap_zombie_cap_get_capZombieBits_'proc kernel_all_global_addresses.cap_zombie_cap_get_capZombieBits_body (Tree.Node cap_zombie_cap_get_capZombieType_'proc kernel_all_global_addresses.cap_zombie_cap_get_capZombieType_body Leaf Leaf) Leaf) (Tree.Node cap_untyped_cap_get_capBlockSize_'proc kernel_all_global_addresses.cap_untyped_cap_get_capBlockSize_body (Tree.Node cap_untyped_cap_get_capFreeIndex_'proc kernel_all_global_addresses.cap_untyped_cap_get_capFreeIndex_body Leaf Leaf) Leaf)) (Tree.Node cap_endpoint_cap_set_capCanGrant_'proc kernel_all_global_addresses.cap_endpoint_cap_set_capCanGrant_body (Tree.Node cap_frame_cap_get_capFMappedASID_'proc kernel_all_global_addresses.cap_frame_cap_get_capFMappedASID_body (Tree.Node cap_frame_cap_set_capFMappedASID_'proc kernel_all_global_addresses.cap_frame_cap_set_capFMappedASID_body Leaf Leaf) Leaf) (Tree.Node seL4_Fault_CapFault_get_address_'proc kernel_all_global_addresses.seL4_Fault_CapFault_get_address_body (Tree.Node cap_endpoint_cap_get_capCanGrant_'proc kernel_all_global_addresses.cap_endpoint_cap_get_capCanGrant_body Leaf Leaf) Leaf)))) (Tree.Node cap_cnode_cap_set_capCNodeGuard_'proc kernel_all_global_addresses.cap_cnode_cap_set_capCNodeGuard_body (Tree.Node cap_zombie_cap_get_capZombiePtr_'proc kernel_all_global_addresses.cap_zombie_cap_get_capZombiePtr_body (Tree.Node mdb_node_ptr_set_mdbFirstBadged_'proc kernel_all_global_addresses.mdb_node_ptr_set_mdbFirstBadged_body (Tree.Node pde_pde_section_ptr_get_address_'proc kernel_all_global_addresses.pde_pde_section_ptr_get_address_body (Tree.Node performPageTableInvocationUnmap_'proc kernel_all_global_addresses.performPageTableInvocationUnmap_body Leaf Leaf) Leaf) (Tree.Node lookup_fault_depth_mismatch_new_'proc kernel_all_global_addresses.lookup_fault_depth_mismatch_new_body (Tree.Node lookup_fault_guard_mismatch_new_'proc kernel_all_global_addresses.lookup_fault_guard_mismatch_new_body Leaf Leaf) Leaf)) (Tree.Node cap_endpoint_cap_set_capCanSend_'proc kernel_all_global_addresses.cap_endpoint_cap_set_capCanSend_body (Tree.Node cap_endpoint_cap_set_capEPBadge_'proc kernel_all_global_addresses.cap_endpoint_cap_set_capEPBadge_body (Tree.Node cap_untyped_cap_get_capIsDevice_'proc kernel_all_global_addresses.cap_untyped_cap_get_capIsDevice_body Leaf Leaf) Leaf) (Tree.Node cap_endpoint_cap_get_capCanSend_'proc kernel_all_global_addresses.cap_endpoint_cap_get_capCanSend_body (Tree.Node cap_endpoint_cap_get_capEPBadge_'proc kernel_all_global_addresses.cap_endpoint_cap_get_capEPBadge_body Leaf Leaf) Leaf))) (Tree.Node thread_state_ptr_set_tcbQueued_'proc kernel_all_global_addresses.thread_state_ptr_set_tcbQueued_body (Tree.Node arch_clean_invalidate_L1_caches_'proc kernel_all_global_addresses.arch_clean_invalidate_L1_caches_body (Tree.Node cap_cnode_cap_get_capCNodeGuard_'proc kernel_all_global_addresses.cap_cnode_cap_get_capCNodeGuard_body (Tree.Node cap_cnode_cap_get_capCNodeRadix_'proc kernel_all_global_addresses.cap_cnode_cap_get_capCNodeRadix_body Leaf Leaf) Leaf) (Tree.Node thread_state_ptr_set_tsType_np_'proc kernel_all_global_addresses.thread_state_ptr_set_tsType_np_body (Tree.Node Arch_decodeIRQControlInvocation_'proc kernel_all_global_addresses.Arch_decodeIRQControlInvocation_body Leaf Leaf) Leaf)) (Tree.Node seL4_Fault_VMFault_get_address_'proc kernel_all_global_addresses.seL4_Fault_VMFault_get_address_body (Tree.Node seL4_MessageInfo_get_extraCaps_'proc kernel_all_global_addresses.seL4_MessageInfo_get_extraCaps_body (Tree.Node seL4_MessageInfo_set_extraCaps_'proc kernel_all_global_addresses.seL4_MessageInfo_set_extraCaps_body Leaf Leaf) Leaf) (Tree.Node performInvocation_Notification_'proc kernel_all_global_addresses.performInvocation_Notification_body (Tree.Node pte_pte_large_ptr_get_reserved_'proc kernel_all_global_addresses.pte_pte_large_ptr_get_reserved_body Leaf Leaf) Leaf))))) (Tree.Node endpoint_ptr_get_epQueue_tail_'proc kernel_all_global_addresses.endpoint_ptr_get_epQueue_tail_body (Tree.Node seL4_Fault_get_seL4_FaultType_'proc kernel_all_global_addresses.seL4_Fault_get_seL4_FaultType_body (Tree.Node cap_irq_handler_cap_get_capIRQ_'proc kernel_all_global_addresses.cap_irq_handler_cap_get_capIRQ_body (Tree.Node generic_frame_cap_get_capFSize_'proc kernel_all_global_addresses.generic_frame_cap_get_capFSize_body (Tree.Node invalidateTranslationASIDLocal_'proc kernel_all_global_addresses.invalidateTranslationASIDLocal_body (Tree.Node invokeIRQHandler_SetIRQHandler_'proc (kernel_all_global_addresses.invokeIRQHandler_SetIRQHandler_body symbol_table) Leaf Leaf) Leaf) (Tree.Node cap_zombie_cap_get_capZombieID_'proc kernel_all_global_addresses.cap_zombie_cap_get_capZombieID_body (Tree.Node cap_zombie_cap_set_capZombieID_'proc kernel_all_global_addresses.cap_zombie_cap_set_capZombieID_body Leaf Leaf) Leaf)) (Tree.Node cap_frame_cap_get_capFIsDevice_'proc kernel_all_global_addresses.cap_frame_cap_get_capFIsDevice_body (Tree.Node cap_frame_cap_get_capFVMRights_'proc kernel_all_global_addresses.cap_frame_cap_get_capFVMRights_body (Tree.Node cap_frame_cap_set_capFVMRights_'proc kernel_all_global_addresses.cap_frame_cap_set_capFVMRights_body Leaf Leaf) Leaf) (Tree.Node writeAuxiliaryControlRegister_'proc kernel_all_global_addresses.writeAuxiliaryControlRegister_body (Tree.Node c_handle_undefined_instruction_'proc kernel_all_global_addresses.c_handle_undefined_instruction_body Leaf Leaf) Leaf))) (Tree.Node mdb_node_ptr_set_mdbRevocable_'proc kernel_all_global_addresses.mdb_node_ptr_set_mdbRevocable_body (Tree.Node pte_pte_small_ptr_get_address_'proc kernel_all_global_addresses.pte_pte_small_ptr_get_address_body (Tree.Node replyFromKernel_success_empty_'proc kernel_all_global_addresses.replyFromKernel_success_empty_body (Tree.Node seL4_Fault_UnknownSyscall_new_'proc kernel_all_global_addresses.seL4_Fault_UnknownSyscall_new_body Leaf Leaf) Leaf) (Tree.Node performPageTableInvocationMap_'proc kernel_all_global_addresses.performPageTableInvocationMap_body (Tree.Node pte_pte_large_ptr_get_address_'proc kernel_all_global_addresses.pte_pte_large_ptr_get_address_body Leaf Leaf) Leaf)) (Tree.Node invalidateTranslationAllLocal_'proc kernel_all_global_addresses.invalidateTranslationAllLocal_body (Tree.Node invokeTCB_NotificationControl_'proc kernel_all_global_addresses.invokeTCB_NotificationControl_body (Tree.Node lookup_fault_invalid_root_new_'proc kernel_all_global_addresses.lookup_fault_invalid_root_new_body Leaf Leaf) Leaf) (Tree.Node endpoint_ptr_set_epQueue_head_'proc kernel_all_global_addresses.endpoint_ptr_set_epQueue_head_body (Tree.Node endpoint_ptr_set_epQueue_tail_'proc kernel_all_global_addresses.endpoint_ptr_set_epQueue_tail_body Leaf Leaf) Leaf)))) (Tree.Node pde_pde_section_ptr_get_size_'proc kernel_all_global_addresses.pde_pde_section_ptr_get_size_body (Tree.Node StrictC'__builtin_unreachable_'proc kernel_all_global_addresses.StrictC'__builtin_unreachable_body (Tree.Node cap_frame_cap_get_capFBasePtr_'proc kernel_all_global_addresses.cap_frame_cap_get_capFBasePtr_body (Tree.Node cleanInvalidateCacheRange_RAM_'proc kernel_all_global_addresses.cleanInvalidateCacheRange_RAM_body (Tree.Node endpoint_ptr_get_epQueue_head_'proc kernel_all_global_addresses.endpoint_ptr_get_epQueue_head_body Leaf Leaf) Leaf) (Tree.Node cap_cnode_cap_get_capCNodePtr_'proc kernel_all_global_addresses.cap_cnode_cap_get_capCNodePtr_body (Tree.Node cap_endpoint_cap_get_capEPPtr_'proc kernel_all_global_addresses.cap_endpoint_cap_get_capEPPtr_body Leaf Leaf) Leaf)) (Tree.Node readAuxiliaryControlRegister_'proc kernel_all_global_addresses.readAuxiliaryControlRegister_body (Tree.Node seL4_CNode_CapData_get_guard_'proc kernel_all_global_addresses.seL4_CNode_CapData_get_guard_body (Tree.Node seL4_Fault_UserException_new_'proc kernel_all_global_addresses.seL4_Fault_UserException_new_body Leaf Leaf) Leaf) (Tree.Node performASIDControlInvocation_'proc kernel_all_global_addresses.performASIDControlInvocation_body (Tree.Node performPageInvocationUnmapIO_'proc kernel_all_global_addresses.performPageInvocationUnmapIO_body Leaf Leaf) Leaf))) (Tree.Node cap_thread_cap_get_capTCBPtr_'proc kernel_all_global_addresses.cap_thread_cap_get_capTCBPtr_body (Tree.Node create_unmapped_it_frame_cap_'proc kernel_all_global_addresses.create_unmapped_it_frame_cap_body (Tree.Node decodeARMPageTableInvocation_'proc kernel_all_global_addresses.decodeARMPageTableInvocation_body (Tree.Node invokeCNodeCancelBadgedSends_'proc kernel_all_global_addresses.invokeCNodeCancelBadgedSends_body Leaf Leaf) Leaf) (Tree.Node createSafeMappingEntries_PDE_'proc kernel_all_global_addresses.createSafeMappingEntries_PDE_body (Tree.Node createSafeMappingEntries_PTE_'proc kernel_all_global_addresses.createSafeMappingEntries_PTE_body Leaf Leaf) Leaf)) (Tree.Node arch_clean_invalidate_caches_'proc kernel_all_global_addresses.arch_clean_invalidate_caches_body (Tree.Node c_handle_fastpath_reply_recv_'proc kernel_all_global_addresses.c_handle_fastpath_reply_recv_body (Tree.Node calculate_extra_bi_size_bits_'proc kernel_all_global_addresses.calculate_extra_bi_size_bits_body Leaf Leaf) Leaf) (Tree.Node Arch_getSanitiseRegisterInfo_'proc kernel_all_global_addresses.Arch_getSanitiseRegisterInfo_body Leaf Leaf))))))) (Tree.Node endpoint_ptr_get_state_'proc kernel_all_global_addresses.endpoint_ptr_get_state_body (Tree.Node pde_pde_section_get_size_'proc kernel_all_global_addresses.pde_pde_section_get_size_body (Tree.Node decodeIRQControlInvocation_'proc kernel_all_global_addresses.decodeIRQControlInvocation_body (Tree.Node cap_reply_cap_get_capTCBPtr_'proc kernel_all_global_addresses.cap_reply_cap_get_capTCBPtr_body (Tree.Node performPageInvocationMapPTE_'proc kernel_all_global_addresses.performPageInvocationMapPTE_body (Tree.Node seL4_MessageInfo_get_length_'proc kernel_all_global_addresses.seL4_MessageInfo_get_length_body (Tree.Node seL4_MessageInfo_set_length_'proc kernel_all_global_addresses.seL4_MessageInfo_set_length_body (Tree.Node thread_state_ptr_get_tsType_'proc kernel_all_global_addresses.thread_state_ptr_get_tsType_body Leaf Leaf) Leaf) (Tree.Node plat_cleanInvalidateL2Cache_'proc kernel_all_global_addresses.plat_cleanInvalidateL2Cache_body (Tree.Node plat_cleanInvalidateL2Range_'proc kernel_all_global_addresses.plat_cleanInvalidateL2Range_body Leaf Leaf) Leaf)) (Tree.Node mdb_node_ptr_set_mdbPrev_np_'proc kernel_all_global_addresses.mdb_node_ptr_set_mdbPrev_np_body (Tree.Node mdb_node_set_mdbFirstBadged_'proc kernel_all_global_addresses.mdb_node_set_mdbFirstBadged_body (Tree.Node performPageInvocationMapPDE_'proc kernel_all_global_addresses.performPageInvocationMapPDE_body Leaf Leaf) Leaf) (Tree.Node invalidateTranslationSingle_'proc kernel_all_global_addresses.invalidateTranslationSingle_body (Tree.Node mdb_node_get_mdbFirstBadged_'proc kernel_all_global_addresses.mdb_node_get_mdbFirstBadged_body Leaf Leaf) Leaf))) (Tree.Node performPageInvocationUnmap_'proc kernel_all_global_addresses.performPageInvocationUnmap_body (Tree.Node seL4_MessageInfo_get_label_'proc kernel_all_global_addresses.seL4_MessageInfo_get_label_body (Tree.Node thread_state_get_tcbQueued_'proc kernel_all_global_addresses.thread_state_get_tcbQueued_body (Tree.Node writeSystemControlRegister_'proc kernel_all_global_addresses.writeSystemControlRegister_body Leaf Leaf) Leaf) (Tree.Node pte_pte_large_get_reserved_'proc kernel_all_global_addresses.pte_pte_large_get_reserved_body (Tree.Node seL4_Fault_VMFault_get_FSR_'proc kernel_all_global_addresses.seL4_Fault_VMFault_get_FSR_body Leaf Leaf) Leaf)) (Tree.Node notification_ptr_set_state_'proc kernel_all_global_addresses.notification_ptr_set_state_body (Tree.Node pde_pde_coarse_get_address_'proc kernel_all_global_addresses.pde_pde_coarse_get_address_body (Tree.Node performInvocation_Endpoint_'proc kernel_all_global_addresses.performInvocation_Endpoint_body Leaf Leaf) Leaf) (Tree.Node decodeIRQHandlerInvocation_'proc kernel_all_global_addresses.decodeIRQHandlerInvocation_body (Tree.Node notification_ptr_get_state_'proc kernel_all_global_addresses.notification_ptr_get_state_body Leaf Leaf) Leaf)))) (Tree.Node mdb_node_set_mdbRevocable_'proc kernel_all_global_addresses.mdb_node_set_mdbRevocable_body (Tree.Node cap_untyped_cap_get_capPtr_'proc kernel_all_global_addresses.cap_untyped_cap_get_capPtr_body (Tree.Node create_mapped_it_frame_cap_'proc kernel_all_global_addresses.create_mapped_it_frame_cap_body (Tree.Node create_untypeds_for_region_'proc kernel_all_global_addresses.create_untypeds_for_region_body (Tree.Node decodeARMIOSpaceInvocation_'proc kernel_all_global_addresses.decodeARMIOSpaceInvocation_body Leaf Leaf) Leaf) (Tree.Node cleanInvalidate_D_by_level_'proc kernel_all_global_addresses.cleanInvalidate_D_by_level_body (Tree.Node cpu_initLocalIRQController_'proc kernel_all_global_addresses.cpu_initLocalIRQController_body Leaf Leaf) Leaf)) (Tree.Node c_handle_instruction_fault_'proc kernel_all_global_addresses.c_handle_instruction_fault_body (Tree.Node cap_frame_cap_get_capFSize_'proc kernel_all_global_addresses.cap_frame_cap_get_capFSize_body (Tree.Node cap_page_directory_cap_new_'proc kernel_all_global_addresses.cap_page_directory_cap_new_body Leaf Leaf) Leaf) (Tree.Node performASIDPoolInvocation_'proc kernel_all_global_addresses.performASIDPoolInvocation_body (Tree.Node readSystemControlRegister_'proc kernel_all_global_addresses.readSystemControlRegister_body Leaf Leaf) Leaf))) (Tree.Node cap_get_archCapIsPhysical_'proc kernel_all_global_addresses.cap_get_archCapIsPhysical_body (Tree.Node invalidateLocalTLB_VAASID_'proc kernel_all_global_addresses.invalidateLocalTLB_VAASID_body (Tree.Node invalidateTranslationASID_'proc kernel_all_global_addresses.invalidateTranslationASID_body (Tree.Node mdb_node_get_mdbRevocable_'proc kernel_all_global_addresses.mdb_node_get_mdbRevocable_body Leaf Leaf) Leaf) (Tree.Node create_rootserver_objects_'proc kernel_all_global_addresses.create_rootserver_objects_body (Tree.Node get_p_reg_kernel_img_boot_'proc (kernel_all_global_addresses.get_p_reg_kernel_img_boot_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node slotCapLongRunningDelete_'proc kernel_all_global_addresses.slotCapLongRunningDelete_body (Tree.Node armv_contextSwitch_HWASID_'proc (kernel_all_global_addresses.armv_contextSwitch_HWASID_body symbol_table) (Tree.Node calculate_rootserver_size_'proc kernel_all_global_addresses.calculate_rootserver_size_body Leaf Leaf) Leaf) (Tree.Node rootserver_max_size_bits_'proc kernel_all_global_addresses.rootserver_max_size_bits_body (Tree.Node seL4_Fault_NullFault_new_'proc kernel_all_global_addresses.seL4_Fault_NullFault_new_body Leaf Leaf) Leaf))))) (Tree.Node messageInfoFromWord_raw_'proc kernel_all_global_addresses.messageInfoFromWord_raw_body (Tree.Node cap_reply_cap_ptr_new_np_'proc kernel_all_global_addresses.cap_reply_cap_ptr_new_np_body (Tree.Node invalidateCacheRange_RAM_'proc kernel_all_global_addresses.invalidateCacheRange_RAM_body (Tree.Node lookup_fault_get_lufType_'proc kernel_all_global_addresses.lookup_fault_get_lufType_body (Tree.Node mdb_node_ptr_set_mdbNext_'proc kernel_all_global_addresses.mdb_node_ptr_set_mdbNext_body (Tree.Node mdb_node_ptr_set_mdbPrev_'proc kernel_all_global_addresses.mdb_node_ptr_set_mdbPrev_body Leaf Leaf) Leaf) (Tree.Node invalidateTranslationAll_'proc kernel_all_global_addresses.invalidateTranslationAll_body (Tree.Node invokeTCB_WriteRegisters_'proc kernel_all_global_addresses.invokeTCB_WriteRegisters_body Leaf Leaf) Leaf)) (Tree.Node decodeARMIOMapInvocation_'proc kernel_all_global_addresses.decodeARMIOMapInvocation_body (Tree.Node decodeUnbindNotification_'proc kernel_all_global_addresses.decodeUnbindNotification_body (Tree.Node fastpath_reply_cap_check_'proc kernel_all_global_addresses.fastpath_reply_cap_check_body Leaf Leaf) Leaf) (Tree.Node create_it_page_table_cap_'proc kernel_all_global_addresses.create_it_page_table_cap_body (Tree.Node decodeARMFrameInvocation_'proc kernel_all_global_addresses.decodeARMFrameInvocation_body Leaf Leaf) Leaf))) (Tree.Node unbindMaybeNotification_'proc kernel_all_global_addresses.unbindMaybeNotification_body (Tree.Node Arch_prepareThreadDelete_'proc kernel_all_global_addresses.Arch_prepareThreadDelete_body (Tree.Node cap_asid_control_cap_new_'proc kernel_all_global_addresses.cap_asid_control_cap_new_body (Tree.Node cap_notification_cap_new_'proc kernel_all_global_addresses.cap_notification_cap_new_body Leaf Leaf) Leaf) (Tree.Node Arch_configureIdleThread_'proc (kernel_all_global_addresses.Arch_configureIdleThread_body symbol_table) (Tree.Node Arch_postModifyRegisters_'proc kernel_all_global_addresses.Arch_postModifyRegisters_body Leaf Leaf) Leaf)) (Tree.Node seL4_Fault_CapFault_new_'proc kernel_all_global_addresses.seL4_Fault_CapFault_new_body (Tree.Node supportsAsyncExceptions_'proc kernel_all_global_addresses.supportsAsyncExceptions_body (Tree.Node thread_state_get_tsType_'proc kernel_all_global_addresses.thread_state_get_tsType_body Leaf Leaf) Leaf) (Tree.Node performInvocation_Reply_'proc kernel_all_global_addresses.performInvocation_Reply_body (Tree.Node scheduleChooseNewThread_'proc kernel_all_global_addresses.scheduleChooseNewThread_body Leaf Leaf) Leaf)))) (Tree.Node check_export_arch_timer_'proc kernel_all_global_addresses.check_export_arch_timer_body (Tree.Node decodeUntypedInvocation_'proc kernel_all_global_addresses.decodeUntypedInvocation_body (Tree.Node invokeTCB_CopyRegisters_'proc kernel_all_global_addresses.invokeTCB_CopyRegisters_body (Tree.Node invokeTCB_ReadRegisters_'proc kernel_all_global_addresses.invokeTCB_ReadRegisters_body (Tree.Node invokeTCB_ThreadControl_'proc kernel_all_global_addresses.invokeTCB_ThreadControl_body Leaf Leaf) Leaf) (Tree.Node invalidateLocalTLB_ASID_'proc kernel_all_global_addresses.invalidateLocalTLB_ASID_body (Tree.Node invokeIRQHandler_AckIRQ_'proc kernel_all_global_addresses.invokeIRQHandler_AckIRQ_body Leaf Leaf) Leaf)) (Tree.Node create_ipcbuf_frame_cap_'proc kernel_all_global_addresses.create_ipcbuf_frame_cap_body (Tree.Node create_it_address_space_'proc kernel_all_global_addresses.create_it_address_space_body (Tree.Node decodeARMIOPTInvocation_'proc kernel_all_global_addresses.decodeARMIOPTInvocation_body Leaf Leaf) Leaf) (Tree.Node cleanInvalidateL1Caches_'proc kernel_all_global_addresses.cleanInvalidateL1Caches_body (Tree.Node create_frames_of_region_'proc kernel_all_global_addresses.create_frames_of_region_body Leaf Leaf) Leaf))) (Tree.Node Arch_activateIdleThread_'proc kernel_all_global_addresses.Arch_activateIdleThread_body (Tree.Node cap_irq_control_cap_new_'proc kernel_all_global_addresses.cap_irq_control_cap_new_body (Tree.Node cap_irq_handler_cap_new_'proc kernel_all_global_addresses.cap_irq_handler_cap_new_body (Tree.Node cap_small_frame_cap_new_'proc kernel_all_global_addresses.cap_small_frame_cap_new_body Leaf Leaf) Leaf) (Tree.Node Arch_switchToIdleThread_'proc kernel_all_global_addresses.Arch_switchToIdleThread_body (Tree.Node cap_get_archCapSizeBits_'proc kernel_all_global_addresses.cap_get_archCapSizeBits_body Leaf Leaf) Leaf)) (Tree.Node invalidateCacheRange_I_'proc kernel_all_global_addresses.invalidateCacheRange_I_body (Tree.Node plat_invalidateL2Range_'proc kernel_all_global_addresses.plat_invalidateL2Range_body (Tree.Node seL4_Fault_VMFault_new_'proc kernel_all_global_addresses.seL4_Fault_VMFault_new_body Leaf Leaf) Leaf) (Tree.Node endpoint_ptr_set_state_'proc kernel_all_global_addresses.endpoint_ptr_set_state_body Leaf Leaf)))))) (Tree.Node Arch_performTransfer_'proc kernel_all_global_addresses.Arch_performTransfer_body (Tree.Node Arch_decodeInvocation_'proc kernel_all_global_addresses.Arch_decodeInvocation_body (Tree.Node performPageGetAddress_'proc kernel_all_global_addresses.performPageGetAddress_body (Tree.Node cap_page_table_cap_new_'proc kernel_all_global_addresses.cap_page_table_cap_new_body (Tree.Node decodeBindNotification_'proc kernel_all_global_addresses.decodeBindNotification_body (Tree.Node decodeDomainInvocation_'proc kernel_all_global_addresses.decodeDomainInvocation_body (Tree.Node doNBRecvFailedTransfer_'proc kernel_all_global_addresses.doNBRecvFailedTransfer_body Leaf Leaf) Leaf) (Tree.Node check_available_memory_'proc kernel_all_global_addresses.check_available_memory_body (Tree.Node decodeARMMMUInvocation_'proc kernel_all_global_addresses.decodeARMMMUInvocation_body Leaf Leaf) Leaf)) (Tree.Node setMRs_lookup_failure_'proc kernel_all_global_addresses.setMRs_lookup_failure_body (Tree.Node activate_kernel_vspace_'proc (kernel_all_global_addresses.activate_kernel_vspace_body symbol_table) (Tree.Node c_handle_fastpath_call_'proc kernel_all_global_addresses.c_handle_fastpath_call_body Leaf Leaf) Leaf) (Tree.Node pptr_in_kernel_window_'proc kernel_all_global_addresses.pptr_in_kernel_window_body (Tree.Node replyFromKernel_error_'proc kernel_all_global_addresses.replyFromKernel_error_body Leaf Leaf) Leaf))) (Tree.Node ceiling_kernel_window_'proc kernel_all_global_addresses.ceiling_kernel_window_body (Tree.Node create_initial_thread_'proc kernel_all_global_addresses.create_initial_thread_body (Tree.Node decodeCNodeInvocation_'proc kernel_all_global_addresses.decodeCNodeInvocation_body (Tree.Node invokeCNodeSaveCaller_'proc kernel_all_global_addresses.invokeCNodeSaveCaller_body Leaf Leaf) Leaf) (Tree.Node check_reserved_memory_'proc kernel_all_global_addresses.check_reserved_memory_body (Tree.Node cleanInvalidate_D_PoC_'proc kernel_all_global_addresses.cleanInvalidate_D_PoC_body Leaf Leaf) Leaf)) (Tree.Node armv_init_user_access_'proc kernel_all_global_addresses.armv_init_user_access_body (Tree.Node cap_asid_pool_cap_new_'proc kernel_all_global_addresses.cap_asid_pool_cap_new_body (Tree.Node cap_get_capIsPhysical_'proc kernel_all_global_addresses.cap_get_capIsPhysical_body Leaf Leaf) Leaf) (Tree.Node Arch_handleFaultReply_'proc kernel_all_global_addresses.Arch_handleFaultReply_body (Tree.Node Arch_invokeIRQControl_'proc kernel_all_global_addresses.Arch_invokeIRQControl_body Leaf Leaf) Leaf)))) (Tree.Node handleUnknownSyscall_'proc kernel_all_global_addresses.handleUnknownSyscall_body (Tree.Node mdb_node_get_mdbNext_'proc kernel_all_global_addresses.mdb_node_get_mdbNext_body (Tree.Node seL4_MessageInfo_new_'proc kernel_all_global_addresses.seL4_MessageInfo_new_body (Tree.Node setMRs_syscall_error_'proc kernel_all_global_addresses.setMRs_syscall_error_body (Tree.Node vmAttributesFromWord_'proc kernel_all_global_addresses.vmAttributesFromWord_body Leaf Leaf) Leaf) (Tree.Node mdb_node_get_mdbPrev_'proc kernel_all_global_addresses.mdb_node_get_mdbPrev_body (Tree.Node mdb_node_set_mdbPrev_'proc kernel_all_global_addresses.mdb_node_set_mdbPrev_body Leaf Leaf) Leaf)) (Tree.Node isValidVTableRoot_fp_'proc kernel_all_global_addresses.isValidVTableRoot_fp_body (Tree.Node lookupSlotForCNodeOp_'proc kernel_all_global_addresses.lookupSlotForCNodeOp_body (Tree.Node maybe_alloc_extra_bi_'proc kernel_all_global_addresses.maybe_alloc_extra_bi_body Leaf Leaf) Leaf) (Tree.Node handleUserLevelFault_'proc kernel_all_global_addresses.handleUserLevelFault_body (Tree.Node invokeUntyped_Retype_'proc kernel_all_global_addresses.invokeUntyped_Retype_body Leaf Leaf) Leaf))) (Tree.Node clearIOPageDirectory_'proc kernel_all_global_addresses.clearIOPageDirectory_body (Tree.Node doUnbindNotification_'proc kernel_all_global_addresses.doUnbindNotification_body (Tree.Node get_p_reg_kernel_img_'proc (kernel_all_global_addresses.get_p_reg_kernel_img_body symbol_table) (Tree.Node handleInterruptEntry_'proc kernel_all_global_addresses.handleInterruptEntry_body Leaf Leaf) Leaf) (Tree.Node decodeSetSchedParams_'proc kernel_all_global_addresses.decodeSetSchedParams_body (Tree.Node decodeWriteRegisters_'proc kernel_all_global_addresses.decodeWriteRegisters_body Leaf Leaf) Leaf)) (Tree.Node capTransferFromWords_'proc kernel_all_global_addresses.capTransferFromWords_body (Tree.Node cap_endpoint_cap_new_'proc kernel_all_global_addresses.cap_endpoint_cap_new_body (Tree.Node cleanInvalidateByWSL_'proc kernel_all_global_addresses.cleanInvalidateByWSL_body Leaf Leaf) Leaf) (Tree.Node Arch_postCapDeletion_'proc kernel_all_global_addresses.Arch_postCapDeletion_body (Tree.Node alloc_rootserver_obj_'proc kernel_all_global_addresses.alloc_rootserver_obj_body Leaf Leaf) Leaf))))) (Tree.Node create_bi_frame_cap_'proc kernel_all_global_addresses.create_bi_frame_cap_body (Tree.Node lookupPTSlot_nofail_'proc kernel_all_global_addresses.lookupPTSlot_nofail_body (Tree.Node pte_pte_invalid_new_'proc kernel_all_global_addresses.pte_pte_invalid_new_body (Tree.Node setUntypedCapAsFull_'proc kernel_all_global_addresses.setUntypedCapAsFull_body (Tree.Node wordFromMessageInfo_'proc kernel_all_global_addresses.wordFromMessageInfo_body (Tree.Node writeContextIDAndPD_'proc kernel_all_global_addresses.writeContextIDAndPD_body Leaf Leaf) Leaf) (Tree.Node pte_ptr_get_pteSize_'proc kernel_all_global_addresses.pte_ptr_get_pteSize_body (Tree.Node pte_ptr_get_pteType_'proc kernel_all_global_addresses.pte_ptr_get_pteType_body Leaf Leaf) Leaf)) (Tree.Node pde_pde_section_new_'proc kernel_all_global_addresses.pde_pde_section_new_body (Tree.Node pde_ptr_get_pdeType_'proc kernel_all_global_addresses.pde_ptr_get_pdeType_body (Tree.Node provide_untyped_cap_'proc kernel_all_global_addresses.provide_untyped_cap_body Leaf Leaf) Leaf) (Tree.Node messageInfoFromWord_'proc kernel_all_global_addresses.messageInfoFromWord_body (Tree.Node pde_pde_invalid_new_'proc kernel_all_global_addresses.pde_pde_invalid_new_body Leaf Leaf) Leaf))) (Tree.Node decodeSetMCPriority_'proc kernel_all_global_addresses.decodeSetMCPriority_body (Tree.Node hasCancelSendRights_'proc kernel_all_global_addresses.hasCancelSendRights_body (Tree.Node invalidateASIDEntry_'proc kernel_all_global_addresses.invalidateASIDEntry_body (Tree.Node invalidateTLBByASID_'proc kernel_all_global_addresses.invalidateTLBByASID_body Leaf Leaf) Leaf) (Tree.Node decodeTCBInvocation_'proc kernel_all_global_addresses.decodeTCBInvocation_body (Tree.Node fastpath_reply_recv_'proc kernel_all_global_addresses.fastpath_reply_recv_body Leaf Leaf) Leaf)) (Tree.Node create_it_frame_cap_'proc kernel_all_global_addresses.create_it_frame_cap_body (Tree.Node decodeCopyRegisters_'proc kernel_all_global_addresses.decodeCopyRegisters_body (Tree.Node decodeReadRegisters_'proc kernel_all_global_addresses.decodeReadRegisters_body Leaf Leaf) Leaf) (Tree.Node create_iospace_caps_'proc kernel_all_global_addresses.create_iospace_caps_body (Tree.Node create_it_asid_pool_'proc kernel_all_global_addresses.create_it_asid_pool_body Leaf Leaf) Leaf)))) (Tree.Node Arch_isCapRevocable_'proc kernel_all_global_addresses.Arch_isCapRevocable_body (Tree.Node checkValidIPCBuffer_'proc kernel_all_global_addresses.checkValidIPCBuffer_body (Tree.Node cleanCacheRange_RAM_'proc kernel_all_global_addresses.cleanCacheRange_RAM_body (Tree.Node cleanInvalidate_L1D_'proc kernel_all_global_addresses.cleanInvalidate_L1D_body (Tree.Node configureIdleThread_'proc kernel_all_global_addresses.configureIdleThread_body Leaf Leaf) Leaf) (Tree.Node cleanCacheRange_PoC_'proc kernel_all_global_addresses.cleanCacheRange_PoC_body (Tree.Node cleanCacheRange_PoU_'proc kernel_all_global_addresses.cleanCacheRange_PoU_body Leaf Leaf) Leaf)) (Tree.Node c_handle_data_fault_'proc kernel_all_global_addresses.c_handle_data_fault_body (Tree.Node cap_get_capSizeBits_'proc kernel_all_global_addresses.cap_get_capSizeBits_body (Tree.Node cap_untyped_cap_new_'proc kernel_all_global_addresses.cap_untyped_cap_new_body Leaf Leaf) Leaf) (Tree.Node Arch_setTLSRegister_'proc kernel_all_global_addresses.Arch_setTLSRegister_body (Tree.Node Arch_switchToThread_'proc kernel_all_global_addresses.Arch_switchToThread_body Leaf Leaf) Leaf))) (Tree.Node rescheduleRequired_'proc kernel_all_global_addresses.rescheduleRequired_body (Tree.Node unbindNotification_'proc kernel_all_global_addresses.unbindNotification_body (Tree.Node write_it_asid_pool_'proc kernel_all_global_addresses.write_it_asid_pool_body (Tree.Node Arch_decodeTransfer_'proc kernel_all_global_addresses.Arch_decodeTransfer_body Leaf Leaf) Leaf) (Tree.Node resolveAddressBits_'proc kernel_all_global_addresses.resolveAddressBits_body (Tree.Node switchToIdleThread_'proc kernel_all_global_addresses.switchToIdleThread_body Leaf Leaf) Leaf)) (Tree.Node ntfn_ptr_set_queue_'proc kernel_all_global_addresses.ntfn_ptr_set_queue_body (Tree.Node pde_pde_coarse_new_'proc kernel_all_global_addresses.pde_pde_coarse_new_body (Tree.Node ready_queues_index_'proc kernel_all_global_addresses.ready_queues_index_body Leaf Leaf) Leaf) (Tree.Node ntfn_ptr_get_queue_'proc kernel_all_global_addresses.ntfn_ptr_get_queue_body Leaf Leaf)))))))) (Tree.Node maskCapRights_'proc kernel_all_global_addresses.maskCapRights_body (Tree.Node decodeSetTLSBase_'proc kernel_all_global_addresses.decodeSetTLSBase_body (Tree.Node deleteIOPageTable_'proc kernel_all_global_addresses.deleteIOPageTable_body (Tree.Node switchToThread_fp_'proc kernel_all_global_addresses.switchToThread_fp_body (Tree.Node cap_domain_cap_new_'proc kernel_all_global_addresses.cap_domain_cap_new_body (Tree.Node decodeSetIPCBuffer_'proc kernel_all_global_addresses.decodeSetIPCBuffer_body (Tree.Node enableFpuInstInHyp_'proc kernel_all_global_addresses.enableFpuInstInHyp_body (Tree.Node handleVMFaultEvent_'proc kernel_all_global_addresses.handleVMFaultEvent_body (Tree.Node invalidateLocalTLB_'proc kernel_all_global_addresses.invalidateLocalTLB_body Leaf Leaf) Leaf) (Tree.Node decodeTCBConfigure_'proc kernel_all_global_addresses.decodeTCBConfigure_body (Tree.Node deletingIRQHandler_'proc (kernel_all_global_addresses.deletingIRQHandler_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node cap_zombie_cap_new_'proc kernel_all_global_addresses.cap_zombie_cap_new_body (Tree.Node copyGlobalMappings_'proc (kernel_all_global_addresses.copyGlobalMappings_body symbol_table) (Tree.Node create_idle_thread_'proc (kernel_all_global_addresses.create_idle_thread_body symbol_table) Leaf Leaf) Leaf) (Tree.Node cap_get_archCapPtr_'proc kernel_all_global_addresses.cap_get_archCapPtr_body (Tree.Node cap_thread_cap_new_'proc kernel_all_global_addresses.cap_thread_cap_new_body Leaf Leaf) Leaf))) (Tree.Node addressTranslateS1_'proc kernel_all_global_addresses.addressTranslateS1_body (Tree.Node armv_contextSwitch_'proc kernel_all_global_addresses.armv_contextSwitch_body (Tree.Node c_handle_interrupt_'proc kernel_all_global_addresses.c_handle_interrupt_body (Tree.Node cap_capType_equals_'proc kernel_all_global_addresses.cap_capType_equals_body Leaf Leaf) Leaf) (Tree.Node arm_load_thread_id_'proc kernel_all_global_addresses.arm_load_thread_id_body (Tree.Node arm_save_thread_id_'proc kernel_all_global_addresses.arm_save_thread_id_body Leaf Leaf) Leaf)) (Tree.Node Arch_getObjectSize_'proc kernel_all_global_addresses.Arch_getObjectSize_body (Tree.Node Arch_maskCapRights_'proc kernel_all_global_addresses.Arch_maskCapRights_body (Tree.Node Arch_updateCapData_'proc kernel_all_global_addresses.Arch_updateCapData_body Leaf Leaf) Leaf) (Tree.Node vm_attributes_new_'proc kernel_all_global_addresses.vm_attributes_new_body (Tree.Node writeContextIDPL2_'proc kernel_all_global_addresses.writeContextIDPL2_body Leaf Leaf) Leaf)))) (Tree.Node invokeTCB_Suspend_'proc kernel_all_global_addresses.invokeTCB_Suspend_body (Tree.Node plat_cleanL2Range_'proc kernel_all_global_addresses.plat_cleanL2Range_body (Tree.Node pte_pte_large_new_'proc kernel_all_global_addresses.pte_pte_large_new_body (Tree.Node pte_pte_small_new_'proc kernel_all_global_addresses.pte_pte_small_new_body (Tree.Node setVMRootForFlush_'proc kernel_all_global_addresses.setVMRootForFlush_body Leaf Leaf) Leaf) (Tree.Node populate_bi_frame_'proc kernel_all_global_addresses.populate_bi_frame_body (Tree.Node pptr_to_paddr_reg_'proc kernel_all_global_addresses.pptr_to_paddr_reg_body Leaf Leaf) Leaf)) (Tree.Node isValidVTableRoot_'proc kernel_all_global_addresses.isValidVTableRoot_body (Tree.Node map_kernel_window_'proc (kernel_all_global_addresses.map_kernel_window_body symbol_table) (Tree.Node paddr_to_pptr_reg_'proc kernel_all_global_addresses.paddr_to_pptr_reg_body Leaf Leaf) Leaf) (Tree.Node isFinalCapability_'proc kernel_all_global_addresses.isFinalCapability_body (Tree.Node isIOSpaceFrameCap_'proc kernel_all_global_addresses.isIOSpaceFrameCap_body Leaf Leaf) Leaf))) (Tree.Node handleSpuriousIRQ_'proc kernel_all_global_addresses.handleSpuriousIRQ_body (Tree.Node invokeCNodeInsert_'proc kernel_all_global_addresses.invokeCNodeInsert_body (Tree.Node invokeCNodeRevoke_'proc kernel_all_global_addresses.invokeCNodeRevoke_body (Tree.Node invokeCNodeRotate_'proc kernel_all_global_addresses.invokeCNodeRotate_body Leaf Leaf) Leaf) (Tree.Node initIRQController_'proc kernel_all_global_addresses.initIRQController_body (Tree.Node invokeCNodeDelete_'proc kernel_all_global_addresses.invokeCNodeDelete_body Leaf Leaf) Leaf)) (Tree.Node fastpath_mi_check_'proc kernel_all_global_addresses.fastpath_mi_check_body (Tree.Node handleDoubleFault_'proc kernel_all_global_addresses.handleDoubleFault_body (Tree.Node handleReservedIRQ_'proc kernel_all_global_addresses.handleReservedIRQ_body Leaf Leaf) Leaf) (Tree.Node deletedIRQHandler_'proc kernel_all_global_addresses.deletedIRQHandler_body (Tree.Node fastpath_copy_mrs_'proc kernel_all_global_addresses.fastpath_copy_mrs_body Leaf Leaf) Leaf))))) (Tree.Node pteCheckIfMapped_'proc kernel_all_global_addresses.pteCheckIfMapped_body (Tree.Node arch_get_n_paging_'proc kernel_all_global_addresses.arch_get_n_paging_body (Tree.Node cap_reply_cap_new_'proc kernel_all_global_addresses.cap_reply_cap_new_body (Tree.Node create_domain_cap_'proc kernel_all_global_addresses.create_domain_cap_body (Tree.Node create_root_cnode_'proc kernel_all_global_addresses.create_root_cnode_body (Tree.Node decodeSetPriority_'proc kernel_all_global_addresses.decodeSetPriority_body Leaf Leaf) Leaf) (Tree.Node clearExMonitor_fp_'proc kernel_all_global_addresses.clearExMonitor_fp_body (Tree.Node copyMRsFaultReply_'proc kernel_all_global_addresses.copyMRsFaultReply_body Leaf Leaf) Leaf)) (Tree.Node cancelBadgedSends_'proc kernel_all_global_addresses.cancelBadgedSends_body (Tree.Node cap_cnode_cap_new_'proc kernel_all_global_addresses.cap_cnode_cap_new_body (Tree.Node cap_frame_cap_new_'proc kernel_all_global_addresses.cap_frame_cap_new_body Leaf Leaf) Leaf) (Tree.Node arch_init_freemem_'proc (kernel_all_global_addresses.arch_init_freemem_body symbol_table) (Tree.Node c_handle_vm_fault_'proc kernel_all_global_addresses.c_handle_vm_fault_body Leaf Leaf) Leaf))) (Tree.Node wordFromVMRights_'proc kernel_all_global_addresses.wordFromVMRights_body (Tree.Node Arch_sameRegionAs_'proc kernel_all_global_addresses.Arch_sameRegionAs_body (Tree.Node Arch_setMRs_fault_'proc kernel_all_global_addresses.Arch_setMRs_fault_body (Tree.Node arch_c_entry_hook_'proc kernel_all_global_addresses.arch_c_entry_hook_body Leaf Leaf) Leaf) (Tree.Node Arch_createObject_'proc kernel_all_global_addresses.Arch_createObject_body (Tree.Node Arch_sameObjectAs_'proc kernel_all_global_addresses.Arch_sameObjectAs_body Leaf Leaf) Leaf)) (Tree.Node setupReplyMaster_'proc kernel_all_global_addresses.setupReplyMaster_body (Tree.Node trapFpuInstToHyp_'proc kernel_all_global_addresses.trapFpuInstToHyp_body (Tree.Node vmRightsFromWord_'proc kernel_all_global_addresses.vmRightsFromWord_body Leaf Leaf) Leaf) (Tree.Node removeFromBitmap_'proc kernel_all_global_addresses.removeFromBitmap_body (Tree.Node sanitiseRegister_'proc kernel_all_global_addresses.sanitiseRegister_body Leaf Leaf) Leaf)))) (Tree.Node invalidate_I_PoU_'proc kernel_all_global_addresses.invalidate_I_PoU_body (Tree.Node lookupTargetSlot_'proc kernel_all_global_addresses.lookupTargetSlot_body (Tree.Node pdeCheckIfMapped_'proc kernel_all_global_addresses.pdeCheckIfMapped_body (Tree.Node performPageFlush_'proc kernel_all_global_addresses.performPageFlush_body (Tree.Node possibleSwitchTo_'proc kernel_all_global_addresses.possibleSwitchTo_body Leaf Leaf) Leaf) (Tree.Node map_it_frame_cap_'proc kernel_all_global_addresses.map_it_frame_cap_body (Tree.Node map_kernel_frame_'proc (kernel_all_global_addresses.map_kernel_frame_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node invokeTCB_Resume_'proc kernel_all_global_addresses.invokeTCB_Resume_body (Tree.Node lookupCapAndSlot_'proc kernel_all_global_addresses.lookupCapAndSlot_body (Tree.Node lookupSourceSlot_'proc kernel_all_global_addresses.lookupSourceSlot_body Leaf Leaf) Leaf) (Tree.Node invokeIRQControl_'proc kernel_all_global_addresses.invokeIRQControl_body (Tree.Node invokeSetTLSBase_'proc kernel_all_global_addresses.invokeSetTLSBase_body Leaf Leaf) Leaf))) (Tree.Node fpsimd_HWCapTest_'proc kernel_all_global_addresses.fpsimd_HWCapTest_body (Tree.Node infer_cpu_gic_id_'proc kernel_all_global_addresses.infer_cpu_gic_id_body (Tree.Node invalidateByVA_I_'proc kernel_all_global_addresses.invalidateByVA_I_body (Tree.Node invalidateHypTLB_'proc kernel_all_global_addresses.invalidateHypTLB_body Leaf Leaf) Leaf) (Tree.Node handleFaultReply_'proc kernel_all_global_addresses.handleFaultReply_body (Tree.Node handleInvocation_'proc kernel_all_global_addresses.handleInvocation_body Leaf Leaf) Leaf)) (Tree.Node ensureNoChildren_'proc kernel_all_global_addresses.ensureNoChildren_body (Tree.Node ep_ptr_get_queue_'proc kernel_all_global_addresses.ep_ptr_get_queue_body (Tree.Node ep_ptr_set_queue_'proc kernel_all_global_addresses.ep_ptr_set_queue_body Leaf Leaf) Leaf) (Tree.Node doNormalTransfer_'proc kernel_all_global_addresses.doNormalTransfer_body Leaf Leaf)))))) (Tree.Node create_untypeds_'proc kernel_all_global_addresses.create_untypeds_body (Tree.Node prio_to_l1index_'proc kernel_all_global_addresses.prio_to_l1index_body (Tree.Node Arch_isFrameType_'proc kernel_all_global_addresses.Arch_isFrameType_body (Tree.Node capSwapForDelete_'proc kernel_all_global_addresses.capSwapForDelete_body (Tree.Node check_export_pmu_'proc kernel_all_global_addresses.check_export_pmu_body (Tree.Node createNewObjects_'proc kernel_all_global_addresses.createNewObjects_body (Tree.Node decodeInvocation_'proc kernel_all_global_addresses.decodeInvocation_body Leaf Leaf) Leaf) (Tree.Node cap_null_cap_new_'proc kernel_all_global_addresses.cap_null_cap_new_body (Tree.Node checkVPAlignment_'proc kernel_all_global_addresses.checkVPAlignment_body Leaf Leaf) Leaf)) (Tree.Node branchFlushRange_'proc kernel_all_global_addresses.branchFlushRange_body (Tree.Node c_handle_syscall_'proc kernel_all_global_addresses.c_handle_syscall_body (Tree.Node cancelAllSignals_'proc kernel_all_global_addresses.cancelAllSignals_body Leaf Leaf) Leaf) (Tree.Node arch_c_exit_hook_'proc kernel_all_global_addresses.arch_c_exit_hook_body (Tree.Node bindNotification_'proc kernel_all_global_addresses.bindNotification_body Leaf Leaf) Leaf))) (Tree.Node tcbSchedDequeue_'proc kernel_all_global_addresses.tcbSchedDequeue_body (Tree.Node updateRestartPC_'proc kernel_all_global_addresses.updateRestartPC_body (Tree.Node Arch_finaliseCap_'proc kernel_all_global_addresses.Arch_finaliseCap_body (Tree.Node Arch_initContext_'proc kernel_all_global_addresses.Arch_initContext_body Leaf Leaf) Leaf) (Tree.Node tcbSchedEnqueue_'proc kernel_all_global_addresses.tcbSchedEnqueue_body (Tree.Node try_init_kernel_'proc kernel_all_global_addresses.try_init_kernel_body Leaf Leaf) Leaf)) (Tree.Node resetUntypedCap_'proc kernel_all_global_addresses.resetUntypedCap_body (Tree.Node setCurrentPDPL2_'proc kernel_all_global_addresses.setCurrentPDPL2_body (Tree.Node setHardwareASID_'proc kernel_all_global_addresses.setHardwareASID_body Leaf Leaf) Leaf) (Tree.Node pte_get_pteSize_'proc kernel_all_global_addresses.pte_get_pteSize_body (Tree.Node pte_get_pteType_'proc kernel_all_global_addresses.pte_get_pteType_body Leaf Leaf) Leaf)))) (Tree.Node l1index_to_prio_'proc kernel_all_global_addresses.l1index_to_prio_body (Tree.Node pageBitsForSize_'proc kernel_all_global_addresses.pageBitsForSize_body (Tree.Node plat_cleanCache_'proc kernel_all_global_addresses.plat_cleanCache_body (Tree.Node postCapDeletion_'proc kernel_all_global_addresses.postCapDeletion_body (Tree.Node preemptionPoint_'proc kernel_all_global_addresses.preemptionPoint_body Leaf Leaf) Leaf) (Tree.Node pageTableMapped_'proc kernel_all_global_addresses.pageTableMapped_body (Tree.Node pde_get_pdeType_'proc kernel_all_global_addresses.pde_get_pdeType_body Leaf Leaf) Leaf)) (Tree.Node lookupIPCBuffer_'proc kernel_all_global_addresses.lookupIPCBuffer_body (Tree.Node lookupPivotSlot_'proc kernel_all_global_addresses.lookupPivotSlot_body (Tree.Node ntfn_set_active_'proc kernel_all_global_addresses.ntfn_set_active_body Leaf Leaf) Leaf) (Tree.Node loadCapTransfer_'proc kernel_all_global_addresses.loadCapTransfer_body (Tree.Node lookupExtraCaps_'proc kernel_all_global_addresses.lookupExtraCaps_body Leaf Leaf) Leaf))) (Tree.Node ensureEmptySlot_'proc kernel_all_global_addresses.ensureEmptySlot_body (Tree.Node init_core_state_'proc kernel_all_global_addresses.init_core_state_body (Tree.Node invokeCNodeMove_'proc kernel_all_global_addresses.invokeCNodeMove_body (Tree.Node it_alloc_paging_'proc kernel_all_global_addresses.it_alloc_paging_body Leaf Leaf) Leaf) (Tree.Node getReceiveSlots_'proc kernel_all_global_addresses.getReceiveSlots_body (Tree.Node handleInterrupt_'proc (kernel_all_global_addresses.handleInterrupt_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node dist_enable_set_'proc kernel_all_global_addresses.dist_enable_set_body (Tree.Node doFaultTransfer_'proc kernel_all_global_addresses.doFaultTransfer_body (Tree.Node doReplyTransfer_'proc kernel_all_global_addresses.doReplyTransfer_body Leaf Leaf) Leaf) (Tree.Node deleteCallerCap_'proc kernel_all_global_addresses.deleteCallerCap_body (Tree.Node dist_enable_clr_'proc kernel_all_global_addresses.dist_enable_clr_body Leaf Leaf) Leaf))))) (Tree.Node deleteASIDPool_'proc kernel_all_global_addresses.deleteASIDPool_body (Tree.Node setKernelStack_'proc kernel_all_global_addresses.setKernelStack_body (Tree.Node wordFromRights_'proc kernel_all_global_addresses.wordFromRights_body (Tree.Node capCyclicZombie_'proc kernel_all_global_addresses.capCyclicZombie_body (Tree.Node cap_get_capType_'proc kernel_all_global_addresses.cap_get_capType_body (Tree.Node cleanCaches_PoU_'proc kernel_all_global_addresses.cleanCaches_PoU_body Leaf Leaf) Leaf) (Tree.Node writeContextID_'proc kernel_all_global_addresses.writeContextID_body (Tree.Node VGICMaintenance_'proc kernel_all_global_addresses.VGICMaintenance_body Leaf Leaf) Leaf)) (Tree.Node switchToThread_'proc kernel_all_global_addresses.switchToThread_body (Tree.Node tcbSchedAppend_'proc kernel_all_global_addresses.tcbSchedAppend_body (Tree.Node unmapPageTable_'proc kernel_all_global_addresses.unmapPageTable_body Leaf Leaf) Leaf) (Tree.Node setThreadState_'proc kernel_all_global_addresses.setThreadState_body (Tree.Node setupCallerCap_'proc kernel_all_global_addresses.setupCallerCap_body Leaf Leaf) Leaf))) (Tree.Node invalidateByVA_'proc kernel_all_global_addresses.invalidateByVA_body (Tree.Node performPDFlush_'proc kernel_all_global_addresses.performPDFlush_body (Tree.Node reserve_region_'proc kernel_all_global_addresses.reserve_region_body (Tree.Node rightsFromWord_'proc kernel_all_global_addresses.rightsFromWord_body Leaf Leaf) Leaf) (Tree.Node invert_l1index_'proc kernel_all_global_addresses.invert_l1index_body (Tree.Node isCapRevocable_'proc kernel_all_global_addresses.isCapRevocable_body Leaf Leaf) Leaf)) (Tree.Node getKernelStack_'proc kernel_all_global_addresses.getKernelStack_body (Tree.Node getProcessorID_'proc kernel_all_global_addresses.getProcessorID_body (Tree.Node invalidateASID_'proc kernel_all_global_addresses.invalidateASID_body Leaf Leaf) Leaf) (Tree.Node findFreeHWASID_'proc kernel_all_global_addresses.findFreeHWASID_body (Tree.Node getHighestPrio_'proc kernel_all_global_addresses.getHighestPrio_body Leaf Leaf) Leaf)))) (Tree.Node writeTPIDRURW_'proc kernel_all_global_addresses.writeTPIDRURW_body (Tree.Node cleanInvalByVA_'proc kernel_all_global_addresses.cleanInvalByVA_body (Tree.Node completeSignal_'proc kernel_all_global_addresses.completeSignal_body (Tree.Node cpu_iface_init_'proc kernel_all_global_addresses.cpu_iface_init_body (Tree.Node decodeSetSpace_'proc kernel_all_global_addresses.decodeSetSpace_body Leaf Leaf) Leaf) (Tree.Node clearExMonitor_'proc kernel_all_global_addresses.clearExMonitor_body (Tree.Node clearMemory_PT_'proc kernel_all_global_addresses.clearMemory_PT_body Leaf Leaf) Leaf)) (Tree.Node Arch_deriveCap_'proc kernel_all_global_addresses.Arch_deriveCap_body (Tree.Node activateThread_'proc kernel_all_global_addresses.activateThread_body (Tree.Node cap_get_capPtr_'proc kernel_all_global_addresses.cap_get_capPtr_body Leaf Leaf) Leaf) (Tree.Node writeTTBR0Ptr_'proc kernel_all_global_addresses.writeTTBR0Ptr_body (Tree.Node APFromVMRights_'proc kernel_all_global_addresses.APFromVMRights_body Leaf Leaf) Leaf))) (Tree.Node setExtraBadge_'proc kernel_all_global_addresses.setExtraBadge_body (Tree.Node updateCapData_'proc kernel_all_global_addresses.updateCapData_body (Tree.Node writeTPIDRPRW_'proc kernel_all_global_addresses.writeTPIDRPRW_body (Tree.Node writeTPIDRURO_'proc kernel_all_global_addresses.writeTPIDRURO_body Leaf Leaf) Leaf) (Tree.Node setIRQTrigger_'proc kernel_all_global_addresses.setIRQTrigger_body (Tree.Node setMCPriority_'proc kernel_all_global_addresses.setMCPriority_body Leaf Leaf) Leaf)) (Tree.Node merge_regions_'proc kernel_all_global_addresses.merge_regions_body (Tree.Node readCacheSize_'proc kernel_all_global_addresses.readCacheSize_body (Tree.Node receiveSignal_'proc kernel_all_global_addresses.receiveSignal_body Leaf Leaf) Leaf) (Tree.Node maskInterrupt_'proc kernel_all_global_addresses.maskInterrupt_body Leaf Leaf))))))) (Tree.Node flushTable_'proc kernel_all_global_addresses.flushTable_body (Tree.Node capRemovable_'proc kernel_all_global_addresses.capRemovable_body (Tree.Node readTPIDRURW_'proc kernel_all_global_addresses.readTPIDRURW_body (Tree.Node cleanByVA_PoU_'proc kernel_all_global_addresses.cleanByVA_PoU_body (Tree.Node handleSyscall_'proc kernel_all_global_addresses.handleSyscall_body (Tree.Node isHighestPrio_'proc kernel_all_global_addresses.isHighestPrio_body (Tree.Node isMDBParentOf_'proc kernel_all_global_addresses.isMDBParentOf_body (Tree.Node map_it_pt_cap_'proc kernel_all_global_addresses.map_it_pt_cap_body Leaf Leaf) Leaf) (Tree.Node handleVMFault_'proc kernel_all_global_addresses.handleVMFault_body (Tree.Node insert_region_'proc kernel_all_global_addresses.insert_region_body Leaf Leaf) Leaf)) (Tree.Node findPDForASID_'proc kernel_all_global_addresses.findPDForASID_body (Tree.Node getObjectSize_'proc kernel_all_global_addresses.getObjectSize_body (Tree.Node getSyscallArg_'proc kernel_all_global_addresses.getSyscallArg_body Leaf Leaf) Leaf) (Tree.Node doIPCTransfer_'proc kernel_all_global_addresses.doIPCTransfer_body (Tree.Node fastpath_call_'proc kernel_all_global_addresses.fastpath_call_body Leaf Leaf) Leaf))) (Tree.Node setCurrentPD_'proc kernel_all_global_addresses.setCurrentPD_body (Tree.Node transferCaps_'proc kernel_all_global_addresses.transferCaps_body (Tree.Node Arch_checkIRQ_'proc kernel_all_global_addresses.Arch_checkIRQ_body (Tree.Node addrFromKPPtr_'proc kernel_all_global_addresses.addrFromKPPtr_body Leaf Leaf) Leaf) (Tree.Node setMRs_fault_'proc kernel_all_global_addresses.setMRs_fault_body (Tree.Node tcbEPDequeue_'proc kernel_all_global_addresses.tcbEPDequeue_body Leaf Leaf) Leaf)) (Tree.Node sameObjectAs_'proc kernel_all_global_addresses.sameObjectAs_body (Tree.Node sameRegionAs_'proc kernel_all_global_addresses.sameRegionAs_body (Tree.Node sendFaultIPC_'proc kernel_all_global_addresses.sendFaultIPC_body Leaf Leaf) Leaf) (Tree.Node reduceZombie_'proc kernel_all_global_addresses.reduceZombie_body (Tree.Node resolveVAddr_'proc kernel_all_global_addresses.resolveVAddr_body Leaf Leaf) Leaf)))) (Tree.Node init_freemem_'proc kernel_all_global_addresses.init_freemem_body (Tree.Node lookupPTSlot_'proc kernel_all_global_addresses.lookupPTSlot_body (Tree.Node ptrFromPAddr_'proc kernel_all_global_addresses.ptrFromPAddr_body (Tree.Node readTPIDRPRW_'proc kernel_all_global_addresses.readTPIDRPRW_body (Tree.Node readTPIDRURO_'proc kernel_all_global_addresses.readTPIDRURO_body Leaf Leaf) Leaf) (Tree.Node maskVMRights_'proc kernel_all_global_addresses.maskVMRights_body (Tree.Node mdb_node_new_'proc kernel_all_global_addresses.mdb_node_new_body Leaf Leaf) Leaf)) (Tree.Node is_reg_empty_'proc kernel_all_global_addresses.is_reg_empty_body (Tree.Node lockTLBEntry_'proc kernel_all_global_addresses.lockTLBEntry_body (Tree.Node lookupPDSlot_'proc kernel_all_global_addresses.lookupPDSlot_body Leaf Leaf) Leaf) (Tree.Node insertNewCap_'proc kernel_all_global_addresses.insertNewCap_body (Tree.Node isIRQPending_'proc kernel_all_global_addresses.isIRQPending_body Leaf Leaf) Leaf))) (Tree.Node cteDeleteOne_'proc kernel_all_global_addresses.cteDeleteOne_body (Tree.Node getExtraCPtr_'proc kernel_all_global_addresses.getExtraCPtr_body (Tree.Node getRestartPC_'proc kernel_all_global_addresses.getRestartPC_body (Tree.Node get_n_paging_'proc kernel_all_global_addresses.get_n_paging_body Leaf Leaf) Leaf) (Tree.Node finaliseSlot_'proc kernel_all_global_addresses.finaliseSlot_body (Tree.Node getActiveIRQ_'proc kernel_all_global_addresses.getActiveIRQ_body Leaf Leaf) Leaf)) (Tree.Node clearEnFPEXC_'proc kernel_all_global_addresses.clearEnFPEXC_body (Tree.Node copyMRsFault_'proc kernel_all_global_addresses.copyMRsFault_body (Tree.Node createObject_'proc kernel_all_global_addresses.createObject_body Leaf Leaf) Leaf) (Tree.Node char_to_long_'proc kernel_all_global_addresses.char_to_long_body (Tree.Node chooseThread_'proc kernel_all_global_addresses.chooseThread_body Leaf Leaf) Leaf))))) (Tree.Node handleReply_'proc kernel_all_global_addresses.handleReply_body (Tree.Node setRegister_'proc kernel_all_global_addresses.setRegister_body (Tree.Node L2_cacheSync_'proc kernel_all_global_addresses.L2_cacheSync_body (Tree.Node c_entry_hook_'proc kernel_all_global_addresses.c_entry_hook_body (Tree.Node cancelAllIPC_'proc kernel_all_global_addresses.cancelAllIPC_body (Tree.Node cancelSignal_'proc kernel_all_global_addresses.cancelSignal_body Leaf Leaf) Leaf) (Tree.Node ackInterrupt_'proc kernel_all_global_addresses.ackInterrupt_body (Tree.Node addrFromPPtr_'proc kernel_all_global_addresses.addrFromPPtr_body Leaf Leaf) Leaf)) (Tree.Node tcbEPAppend_'proc kernel_all_global_addresses.tcbEPAppend_body (Tree.Node unmapIOPage_'proc kernel_all_global_addresses.unmapIOPage_body (Tree.Node writeHTPIDR_'proc kernel_all_global_addresses.writeHTPIDR_body Leaf Leaf) Leaf) (Tree.Node storeHWASID_'proc kernel_all_global_addresses.storeHWASID_body (Tree.Node str_to_long_'proc kernel_all_global_addresses.str_to_long_body Leaf Leaf) Leaf))) (Tree.Node makeUserPDE_'proc kernel_all_global_addresses.makeUserPDE_body (Tree.Node scheduleTCB_'proc kernel_all_global_addresses.scheduleTCB_body (Tree.Node setIRQState_'proc kernel_all_global_addresses.setIRQState_body (Tree.Node setPriority_'proc kernel_all_global_addresses.setPriority_body Leaf Leaf) Leaf) (Tree.Node makeUserPTE_'proc kernel_all_global_addresses.makeUserPTE_body (Tree.Node provide_cap_'proc kernel_all_global_addresses.provide_cap_body Leaf Leaf) Leaf)) (Tree.Node initL2Cache_'proc kernel_all_global_addresses.initL2Cache_body (Tree.Node init_kernel_'proc kernel_all_global_addresses.init_kernel_body (Tree.Node isIRQActive_'proc kernel_all_global_addresses.isIRQActive_body Leaf Leaf) Leaf) (Tree.Node handleYield_'proc kernel_all_global_addresses.handleYield_body (Tree.Node idle_thread_'proc kernel_all_global_addresses.idle_thread_body Leaf Leaf) Leaf)))) (Tree.Node writeTTBR0_'proc kernel_all_global_addresses.writeTTBR0_body (Tree.Node c_exit_hook_'proc kernel_all_global_addresses.c_exit_hook_body (Tree.Node finaliseCap_'proc kernel_all_global_addresses.finaliseCap_body (Tree.Node getRegister_'proc kernel_all_global_addresses.getRegister_body (Tree.Node handleFault_'proc kernel_all_global_addresses.handleFault_body Leaf Leaf) Leaf) (Tree.Node clean_D_PoU_'proc kernel_all_global_addresses.clean_D_PoU_body (Tree.Node clearMemory_'proc kernel_all_global_addresses.clearMemory_body Leaf Leaf) Leaf)) (Tree.Node addToBitmap_'proc kernel_all_global_addresses.addToBitmap_body (Tree.Node bi_finalise_'proc kernel_all_global_addresses.bi_finalise_body (Tree.Node branchFlush_'proc kernel_all_global_addresses.branchFlush_body Leaf Leaf) Leaf) (Tree.Node writeTTBR1_'proc kernel_all_global_addresses.writeTTBR1_body (Tree.Node write_slot_'proc kernel_all_global_addresses.write_slot_body Leaf Leaf) Leaf))) (Tree.Node nextDomain_'proc kernel_all_global_addresses.nextDomain_body (Tree.Node resetTimer_'proc kernel_all_global_addresses.resetTimer_body (Tree.Node sendSignal_'proc kernel_all_global_addresses.sendSignal_body (Tree.Node writeTTBCR_'proc kernel_all_global_addresses.writeTTBCR_body Leaf Leaf) Leaf) (Tree.Node readHTPIDR_'proc kernel_all_global_addresses.readHTPIDR_body (Tree.Node receiveIPC_'proc kernel_all_global_addresses.receiveIPC_body Leaf Leaf) Leaf)) (Tree.Node isRunnable_'proc kernel_all_global_addresses.isRunnable_body (Tree.Node loadHWASID_'proc kernel_all_global_addresses.loadHWASID_body (Tree.Node lookupSlot_'proc kernel_all_global_addresses.lookupSlot_body Leaf Leaf) Leaf) (Tree.Node handleRecv_'proc kernel_all_global_addresses.handleRecv_body Leaf Leaf)))))) (Tree.Node getAIFSR_'proc kernel_all_global_addresses.getAIFSR_body (Tree.Node initTimer_'proc kernel_all_global_addresses.initTimer_body (Tree.Node setDomain_'proc kernel_all_global_addresses.setDomain_body (Tree.Node Zombie_new_'proc kernel_all_global_addresses.Zombie_new_body (Tree.Node deleteASID_'proc kernel_all_global_addresses.deleteASID_body (Tree.Node disableFpu_'proc kernel_all_global_addresses.disableFpu_body (Tree.Node flushSpace_'proc kernel_all_global_addresses.flushSpace_body Leaf Leaf) Leaf) (Tree.Node arm_errata_'proc kernel_all_global_addresses.arm_errata_body (Tree.Node cleanByWSL_'proc kernel_all_global_addresses.cleanByWSL_body Leaf Leaf) Leaf)) (Tree.Node timerTick_'proc kernel_all_global_addresses.timerTick_body (Tree.Node unmapPage_'proc kernel_all_global_addresses.unmapPage_body (Tree.Node writeDACR_'proc kernel_all_global_addresses.writeDACR_body Leaf Leaf) Leaf) (Tree.Node setNextPC_'proc kernel_all_global_addresses.setNextPC_body (Tree.Node setVMRoot_'proc (kernel_all_global_addresses.setVMRoot_body symbol_table) Leaf Leaf) Leaf))) (Tree.Node lookupCap_'proc kernel_all_global_addresses.lookupCap_body (Tree.Node readTTBCR_'proc kernel_all_global_addresses.readTTBCR_body (Tree.Node readTTBR0_'proc kernel_all_global_addresses.readTTBR0_body (Tree.Node readTTBR1_'proc kernel_all_global_addresses.readTTBR1_body Leaf Leaf) Leaf) (Tree.Node lookup_fp_'proc kernel_all_global_addresses.lookup_fp_body (Tree.Node readMPIDR_'proc kernel_all_global_addresses.readMPIDR_body Leaf Leaf) Leaf)) (Tree.Node isArchCap_'proc kernel_all_global_addresses.isArchCap_body (Tree.Node isBlocked_'proc kernel_all_global_addresses.isBlocked_body (Tree.Node isStopped_'proc kernel_all_global_addresses.isStopped_body Leaf Leaf) Leaf) (Tree.Node init_irqs_'proc kernel_all_global_addresses.init_irqs_body (Tree.Node init_plat_'proc kernel_all_global_addresses.init_plat_body Leaf Leaf) Leaf)))) (Tree.Node checkPrio_'proc kernel_all_global_addresses.checkPrio_body (Tree.Node dist_init_'proc kernel_all_global_addresses.dist_init_body (Tree.Node flushBTAC_'proc kernel_all_global_addresses.flushBTAC_body (Tree.Node flushPage_'proc kernel_all_global_addresses.flushPage_body (Tree.Node getHWASID_'proc kernel_all_global_addresses.getHWASID_body Leaf Leaf) Leaf) (Tree.Node dsb_ishst_'proc kernel_all_global_addresses.dsb_ishst_body (Tree.Node emptySlot_'proc kernel_all_global_addresses.emptySlot_body Leaf Leaf) Leaf)) (Tree.Node cteInsert_'proc kernel_all_global_addresses.cteInsert_body (Tree.Node cteRevoke_'proc kernel_all_global_addresses.cteRevoke_body (Tree.Node deriveCap_'proc kernel_all_global_addresses.deriveCap_body Leaf Leaf) Leaf) (Tree.Node cleanByVA_'proc kernel_all_global_addresses.cleanByVA_body (Tree.Node cteDelete_'proc kernel_all_global_addresses.cteDelete_body Leaf Leaf) Leaf))) (Tree.Node schedule_'proc kernel_all_global_addresses.schedule_body (Tree.Node setAIFSR_'proc kernel_all_global_addresses.setAIFSR_body (Tree.Node slowpath_'proc kernel_all_global_addresses.slowpath_body (Tree.Node cancelIPC_'proc kernel_all_global_addresses.cancelIPC_body Leaf Leaf) Leaf) (Tree.Node setACTLR_'proc kernel_all_global_addresses.setACTLR_body (Tree.Node setADFSR_'proc kernel_all_global_addresses.setADFSR_body Leaf Leaf) Leaf)) (Tree.Node physBase_'proc kernel_all_global_addresses.physBase_body (Tree.Node readCLID_'proc kernel_all_global_addresses.readCLID_body (Tree.Node readDACR_'proc kernel_all_global_addresses.readDACR_body Leaf Leaf) Leaf) (Tree.Node init_cpu_'proc (kernel_all_global_addresses.init_cpu_body symbol_table) (Tree.Node pageBase_'proc kernel_all_global_addresses.pageBase_body Leaf Leaf) Leaf))))) (Tree.Node getCIDR_'proc kernel_all_global_addresses.getCIDR_body (Tree.Node setDFSR_'proc kernel_all_global_addresses.setDFSR_body (Tree.Node strlcpy_'proc kernel_all_global_addresses.strlcpy_body (Tree.Node suspend_'proc kernel_all_global_addresses.suspend_body (Tree.Node getACTLR_'proc kernel_all_global_addresses.getACTLR_body (Tree.Node getADFSR_'proc kernel_all_global_addresses.getADFSR_body Leaf Leaf) Leaf) (Tree.Node strncmp_'proc kernel_all_global_addresses.strncmp_body (Tree.Node strnlen_'proc kernel_all_global_addresses.strnlen_body Leaf Leaf) Leaf)) (Tree.Node setNMRR_'proc kernel_all_global_addresses.setNMRR_body (Tree.Node setPRRR_'proc kernel_all_global_addresses.setPRRR_body (Tree.Node strlcat_'proc kernel_all_global_addresses.strlcat_body Leaf Leaf) Leaf) (Tree.Node setIFAR_'proc kernel_all_global_addresses.setIFAR_body (Tree.Node setIFSR_'proc kernel_all_global_addresses.setIFSR_body Leaf Leaf) Leaf))) (Tree.Node getPRRR_'proc kernel_all_global_addresses.getPRRR_body (Tree.Node sendIPC_'proc kernel_all_global_addresses.sendIPC_body (Tree.Node setCIDR_'proc kernel_all_global_addresses.setCIDR_body (Tree.Node setDFAR_'proc kernel_all_global_addresses.setDFAR_body Leaf Leaf) Leaf) (Tree.Node memzero_'proc kernel_all_global_addresses.memzero_body (Tree.Node restart_'proc kernel_all_global_addresses.restart_body Leaf Leaf) Leaf)) (Tree.Node getIFAR_'proc kernel_all_global_addresses.getIFAR_body (Tree.Node getIFSR_'proc kernel_all_global_addresses.getIFSR_body (Tree.Node getNMRR_'proc kernel_all_global_addresses.getNMRR_body Leaf Leaf) Leaf) (Tree.Node getDFAR_'proc kernel_all_global_addresses.getDFAR_body (Tree.Node getDFSR_'proc kernel_all_global_addresses.getDFSR_body Leaf Leaf) Leaf)))) (Tree.Node ctz32_'proc kernel_all_global_addresses.ctz32_body (Tree.Node memset_'proc kernel_all_global_addresses.memset_body (Tree.Node cteMove_'proc kernel_all_global_addresses.cteMove_body (Tree.Node cteSwap_'proc kernel_all_global_addresses.cteSwap_body (Tree.Node doFlush_'proc kernel_all_global_addresses.doFlush_body Leaf Leaf) Leaf) (Tree.Node alignUp_'proc kernel_all_global_addresses.alignUp_body (Tree.Node copyMRs_'proc kernel_all_global_addresses.copyMRs_body Leaf Leaf) Leaf)) (Tree.Node setMR_'proc kernel_all_global_addresses.setMR_body (Tree.Node getFAR_'proc kernel_all_global_addresses.getFAR_body (Tree.Node memcpy_'proc kernel_all_global_addresses.memcpy_body Leaf Leaf) Leaf) (Tree.Node ctz64_'proc kernel_all_global_addresses.ctz64_body (Tree.Node ctzll_'proc kernel_all_global_addresses.ctzll_body Leaf Leaf) Leaf))) (Tree.Node clzl_'proc kernel_all_global_addresses.clzl_body (Tree.Node clz32_'proc kernel_all_global_addresses.clz32_body (Tree.Node clz64_'proc kernel_all_global_addresses.clz64_body (Tree.Node clzll_'proc kernel_all_global_addresses.clzll_body Leaf Leaf) Leaf) (Tree.Node ctzl_'proc kernel_all_global_addresses.ctzl_body (Tree.Node halt_'proc kernel_all_global_addresses.halt_body Leaf Leaf) Leaf)) (Tree.Node dsb_'proc kernel_all_global_addresses.dsb_body (Tree.Node isb_'proc kernel_all_global_addresses.isb_body (Tree.Node wfi_'proc kernel_all_global_addresses.wfi_body Leaf Leaf) Leaf) (Tree.Node dmb_'proc kernel_all_global_addresses.dmb_body Leaf Leaf))))))))) id) (lookup_tree (Tree.Node map_kernel_devices_'proc (kernel_all_substitute.map_kernel_devices_body symbol_table) (Tree.Node thread_state_ptr_set_tsType_'proc kernel_all_substitute.thread_state_ptr_set_tsType_body (Tree.Node seL4_Fault_UserException_get_code_'proc kernel_all_substitute.seL4_Fault_UserException_get_code_body (Tree.Node pde_pde_invalid_get_stored_asid_valid_'proc kernel_all_substitute.pde_pde_invalid_get_stored_asid_valid_body (Tree.Node thread_state_ptr_set_blockingIPCCanGrant_'proc kernel_all_substitute.thread_state_ptr_set_blockingIPCCanGrant_body (Tree.Node cap_small_frame_cap_get_capFMappedASIDHigh_'proc kernel_all_substitute.cap_small_frame_cap_get_capFMappedASIDHigh_body (Tree.Node cap_page_directory_cap_ptr_set_capPDIsMapped_'proc kernel_all_substitute.cap_page_directory_cap_ptr_set_capPDIsMapped_body (Tree.Node thread_state_ptr_set_blockingIPCCanGrantReply_'proc kernel_all_substitute.thread_state_ptr_set_blockingIPCCanGrantReply_body (Tree.Node cap_page_directory_cap_ptr_set_capPDMappedASID_'proc kernel_all_substitute.cap_page_directory_cap_ptr_set_capPDMappedASID_body (Tree.Node mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_'proc kernel_all_substitute.mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_body Leaf Leaf) Leaf) (Tree.Node lookup_fault_missing_capability_get_bitsLeft_'proc kernel_all_substitute.lookup_fault_missing_capability_get_bitsLeft_body (Tree.Node thread_state_ptr_get_blockingIPCCanGrantReply_'proc kernel_all_substitute.thread_state_ptr_get_blockingIPCCanGrantReply_body Leaf Leaf) Leaf)) (Tree.Node generic_frame_cap_ptr_set_capFMappedAddress_'proc kernel_all_substitute.generic_frame_cap_ptr_set_capFMappedAddress_body (Tree.Node seL4_Fault_UnknownSyscall_get_syscallNumber_'proc kernel_all_substitute.seL4_Fault_UnknownSyscall_get_syscallNumber_body (Tree.Node thread_state_ptr_mset_blockingObject_tsType_'proc kernel_all_substitute.thread_state_ptr_mset_blockingObject_tsType_body Leaf Leaf) Leaf) (Tree.Node cap_small_frame_cap_set_capFMappedASIDHigh_'proc kernel_all_substitute.cap_small_frame_cap_set_capFMappedASIDHigh_body (Tree.Node lookup_fault_guard_mismatch_get_guardFound_'proc kernel_all_substitute.lookup_fault_guard_mismatch_get_guardFound_body Leaf Leaf) Leaf))) (Tree.Node cap_small_frame_cap_set_capFMappedAddress_'proc kernel_all_substitute.cap_small_frame_cap_set_capFMappedAddress_body (Tree.Node cap_notification_cap_get_capNtfnCanReceive_'proc kernel_all_substitute.cap_notification_cap_get_capNtfnCanReceive_body (Tree.Node cap_notification_cap_set_capNtfnCanReceive_'proc kernel_all_substitute.cap_notification_cap_set_capNtfnCanReceive_body (Tree.Node cap_page_directory_cap_get_capPDMappedASID_'proc kernel_all_substitute.cap_page_directory_cap_get_capPDMappedASID_body Leaf Leaf) Leaf) (Tree.Node lookup_fault_depth_mismatch_get_bitsFound_'proc kernel_all_substitute.lookup_fault_depth_mismatch_get_bitsFound_body (Tree.Node lookup_fault_guard_mismatch_get_bitsFound_'proc kernel_all_substitute.lookup_fault_guard_mismatch_get_bitsFound_body Leaf Leaf) Leaf)) (Tree.Node cap_small_frame_cap_get_capFMappedASIDLow_'proc kernel_all_substitute.cap_small_frame_cap_get_capFMappedASIDLow_body (Tree.Node cap_small_frame_cap_get_capFMappedAddress_'proc kernel_all_substitute.cap_small_frame_cap_get_capFMappedAddress_body (Tree.Node cap_small_frame_cap_set_capFMappedASIDLow_'proc kernel_all_substitute.cap_small_frame_cap_set_capFMappedASIDLow_body Leaf Leaf) Leaf) (Tree.Node cap_page_table_cap_get_capPTMappedAddress_'proc kernel_all_substitute.cap_page_table_cap_get_capPTMappedAddress_body (Tree.Node cap_page_table_cap_set_capPTMappedAddress_'proc kernel_all_substitute.cap_page_table_cap_set_capPTMappedAddress_body Leaf Leaf) Leaf)))) (Tree.Node thread_state_ptr_set_blockingIPCIsCall_'proc kernel_all_substitute.thread_state_ptr_set_blockingIPCIsCall_body (Tree.Node seL4_Fault_VMFault_get_instructionFault_'proc kernel_all_substitute.seL4_Fault_VMFault_get_instructionFault_body (Tree.Node lookup_fault_depth_mismatch_get_bitsLeft_'proc kernel_all_substitute.lookup_fault_depth_mismatch_get_bitsLeft_body (Tree.Node lookup_fault_guard_mismatch_get_bitsLeft_'proc kernel_all_substitute.lookup_fault_guard_mismatch_get_bitsLeft_body (Tree.Node thread_state_ptr_get_blockingIPCCanGrant_'proc kernel_all_substitute.thread_state_ptr_get_blockingIPCCanGrant_body Leaf Leaf) Leaf) (Tree.Node cap_page_directory_cap_get_capPDIsMapped_'proc kernel_all_substitute.cap_page_directory_cap_get_capPDIsMapped_body (Tree.Node cap_page_table_cap_ptr_set_capPTIsMapped_'proc kernel_all_substitute.cap_page_table_cap_ptr_set_capPTIsMapped_body Leaf Leaf) Leaf)) (Tree.Node cap_page_directory_cap_get_capPDBasePtr_'proc kernel_all_substitute.cap_page_directory_cap_get_capPDBasePtr_body (Tree.Node generic_frame_cap_get_capFMappedAddress_'proc kernel_all_substitute.generic_frame_cap_get_capFMappedAddress_body (Tree.Node generic_frame_cap_set_capFMappedAddress_'proc kernel_all_substitute.generic_frame_cap_set_capFMappedAddress_body Leaf Leaf) Leaf) (Tree.Node cap_notification_cap_get_capNtfnCanSend_'proc kernel_all_substitute.cap_notification_cap_get_capNtfnCanSend_body (Tree.Node cap_notification_cap_set_capNtfnCanSend_'proc kernel_all_substitute.cap_notification_cap_set_capNtfnCanSend_body Leaf Leaf) Leaf))) (Tree.Node cap_small_frame_cap_get_capFMappedASID_'proc kernel_all_substitute.cap_small_frame_cap_get_capFMappedASID_body (Tree.Node notification_ptr_set_ntfnMsgIdentifier_'proc kernel_all_substitute.notification_ptr_set_ntfnMsgIdentifier_body (Tree.Node seL4_Fault_CapFault_get_inReceivePhase_'proc kernel_all_substitute.seL4_Fault_CapFault_get_inReceivePhase_body (Tree.Node thread_state_ptr_get_blockingIPCIsCall_'proc kernel_all_substitute.thread_state_ptr_get_blockingIPCIsCall_body Leaf Leaf) Leaf) (Tree.Node cap_small_frame_cap_set_capFMappedASID_'proc kernel_all_substitute.cap_small_frame_cap_set_capFMappedASID_body (Tree.Node notification_ptr_get_ntfnMsgIdentifier_'proc kernel_all_substitute.notification_ptr_get_ntfnMsgIdentifier_body Leaf Leaf) Leaf)) (Tree.Node thread_state_ptr_set_blockingIPCBadge_'proc kernel_all_substitute.thread_state_ptr_set_blockingIPCBadge_body (Tree.Node cap_page_table_cap_get_capPTMappedASID_'proc kernel_all_substitute.cap_page_table_cap_get_capPTMappedASID_body (Tree.Node cap_page_table_cap_set_capPTMappedASID_'proc kernel_all_substitute.cap_page_table_cap_set_capPTMappedASID_body Leaf Leaf) Leaf) (Tree.Node seL4_CapRights_get_capAllowGrantReply_'proc kernel_all_substitute.seL4_CapRights_get_capAllowGrantReply_body (Tree.Node thread_state_ptr_get_blockingIPCBadge_'proc kernel_all_substitute.thread_state_ptr_get_blockingIPCBadge_body Leaf Leaf) Leaf))))) (Tree.Node cap_page_table_cap_get_capPTBasePtr_'proc kernel_all_substitute.cap_page_table_cap_get_capPTBasePtr_body (Tree.Node cap_page_table_cap_get_capPTIsMapped_'proc kernel_all_substitute.cap_page_table_cap_get_capPTIsMapped_body (Tree.Node endpoint_ptr_mset_epQueue_tail_state_'proc kernel_all_substitute.endpoint_ptr_mset_epQueue_tail_state_body (Tree.Node cap_endpoint_cap_set_capCanGrantReply_'proc kernel_all_substitute.cap_endpoint_cap_set_capCanGrantReply_body (Tree.Node cap_notification_cap_get_capNtfnBadge_'proc kernel_all_substitute.cap_notification_cap_get_capNtfnBadge_body (Tree.Node cap_notification_cap_set_capNtfnBadge_'proc kernel_all_substitute.cap_notification_cap_set_capNtfnBadge_body Leaf Leaf) Leaf) (Tree.Node generic_frame_cap_get_capFMappedASID_'proc kernel_all_substitute.generic_frame_cap_get_capFMappedASID_body (Tree.Node cap_endpoint_cap_get_capCanGrantReply_'proc kernel_all_substitute.cap_endpoint_cap_get_capCanGrantReply_body Leaf Leaf) Leaf)) (Tree.Node cap_small_frame_cap_get_capFVMRights_'proc kernel_all_substitute.cap_small_frame_cap_get_capFVMRights_body (Tree.Node cap_small_frame_cap_set_capFVMRights_'proc kernel_all_substitute.cap_small_frame_cap_set_capFVMRights_body (Tree.Node cap_untyped_cap_ptr_set_capFreeIndex_'proc kernel_all_substitute.cap_untyped_cap_ptr_set_capFreeIndex_body Leaf Leaf) Leaf) (Tree.Node cap_page_table_cap_set_capPTIsMapped_'proc kernel_all_substitute.cap_page_table_cap_set_capPTIsMapped_body (Tree.Node cap_small_frame_cap_get_capFIsDevice_'proc kernel_all_substitute.cap_small_frame_cap_get_capFIsDevice_body Leaf Leaf) Leaf))) (Tree.Node notification_ptr_set_ntfnQueue_tail_'proc kernel_all_substitute.notification_ptr_set_ntfnQueue_tail_body (Tree.Node thread_state_ptr_set_blockingObject_'proc kernel_all_substitute.thread_state_ptr_set_blockingObject_body (Tree.Node cap_frame_cap_get_capFMappedASIDHigh_'proc kernel_all_substitute.cap_frame_cap_get_capFMappedASIDHigh_body (Tree.Node cap_frame_cap_set_capFMappedASIDHigh_'proc kernel_all_substitute.cap_frame_cap_set_capFMappedASIDHigh_body Leaf Leaf) Leaf) (Tree.Node seL4_Fault_UserException_get_number_'proc kernel_all_substitute.seL4_Fault_UserException_get_number_body (Tree.Node thread_state_ptr_get_blockingObject_'proc kernel_all_substitute.thread_state_ptr_get_blockingObject_body Leaf Leaf) Leaf)) (Tree.Node notification_ptr_get_ntfnQueue_head_'proc kernel_all_substitute.notification_ptr_get_ntfnQueue_head_body (Tree.Node notification_ptr_get_ntfnQueue_tail_'proc kernel_all_substitute.notification_ptr_get_ntfnQueue_tail_body (Tree.Node notification_ptr_set_ntfnQueue_head_'proc kernel_all_substitute.notification_ptr_set_ntfnQueue_head_body Leaf Leaf) Leaf) (Tree.Node cap_small_frame_cap_get_capFBasePtr_'proc kernel_all_substitute.cap_small_frame_cap_get_capFBasePtr_body (Tree.Node lookup_fault_missing_capability_new_'proc kernel_all_substitute.lookup_fault_missing_capability_new_body Leaf Leaf) Leaf)))) (Tree.Node pde_pde_invalid_get_stored_hw_asid_'proc kernel_all_substitute.pde_pde_invalid_get_stored_hw_asid_body (Tree.Node cap_cnode_cap_set_capCNodeGuardSize_'proc kernel_all_substitute.cap_cnode_cap_set_capCNodeGuardSize_body (Tree.Node cap_frame_cap_set_capFMappedASIDLow_'proc kernel_all_substitute.cap_frame_cap_set_capFMappedASIDLow_body (Tree.Node cap_frame_cap_set_capFMappedAddress_'proc kernel_all_substitute.cap_frame_cap_set_capFMappedAddress_body (Tree.Node cap_notification_cap_get_capNtfnPtr_'proc kernel_all_substitute.cap_notification_cap_get_capNtfnPtr_body Leaf Leaf) Leaf) (Tree.Node cap_frame_cap_get_capFMappedASIDLow_'proc kernel_all_substitute.cap_frame_cap_get_capFMappedASIDLow_body (Tree.Node cap_frame_cap_get_capFMappedAddress_'proc kernel_all_substitute.cap_frame_cap_get_capFMappedAddress_body Leaf Leaf) Leaf)) (Tree.Node vm_attributes_get_armPageCacheable_'proc kernel_all_substitute.vm_attributes_get_armPageCacheable_body (Tree.Node vm_attributes_get_armParityEnabled_'proc kernel_all_substitute.vm_attributes_get_armParityEnabled_body (Tree.Node cap_cnode_cap_get_capCNodeGuardSize_'proc kernel_all_substitute.cap_cnode_cap_get_capCNodeGuardSize_body Leaf Leaf) Leaf) (Tree.Node seL4_MessageInfo_get_capsUnwrapped_'proc kernel_all_substitute.seL4_MessageInfo_get_capsUnwrapped_body (Tree.Node seL4_MessageInfo_set_capsUnwrapped_'proc kernel_all_substitute.seL4_MessageInfo_set_capsUnwrapped_body Leaf Leaf) Leaf))) (Tree.Node cap_reply_cap_set_capReplyCanGrant_'proc kernel_all_substitute.cap_reply_cap_set_capReplyCanGrant_body (Tree.Node generic_frame_cap_get_capFIsDevice_'proc kernel_all_substitute.generic_frame_cap_get_capFIsDevice_body (Tree.Node generic_frame_cap_get_capFIsMapped_'proc kernel_all_substitute.generic_frame_cap_get_capFIsMapped_body (Tree.Node generic_frame_cap_get_capFVMRights_'proc kernel_all_substitute.generic_frame_cap_get_capFVMRights_body Leaf Leaf) Leaf) (Tree.Node cap_zombie_cap_get_capZombieNumber_'proc kernel_all_substitute.cap_zombie_cap_get_capZombieNumber_body (Tree.Node cap_zombie_cap_set_capZombieNumber_'proc kernel_all_substitute.cap_zombie_cap_set_capZombieNumber_body Leaf Leaf) Leaf)) (Tree.Node cap_endpoint_cap_get_capCanReceive_'proc kernel_all_substitute.cap_endpoint_cap_get_capCanReceive_body (Tree.Node cap_endpoint_cap_set_capCanReceive_'proc kernel_all_substitute.cap_endpoint_cap_set_capCanReceive_body (Tree.Node cap_reply_cap_get_capReplyCanGrant_'proc kernel_all_substitute.cap_reply_cap_get_capReplyCanGrant_body Leaf Leaf) Leaf) (Tree.Node vm_attributes_get_armExecuteNever_'proc kernel_all_substitute.vm_attributes_get_armExecuteNever_body Leaf Leaf)))))) (Tree.Node pde_pde_coarse_ptr_get_address_'proc kernel_all_substitute.pde_pde_coarse_ptr_get_address_body (Tree.Node seL4_CapRights_get_capAllowRead_'proc kernel_all_substitute.seL4_CapRights_get_capAllowRead_body (Tree.Node decodeARMPageDirectoryInvocation_'proc kernel_all_substitute.decodeARMPageDirectoryInvocation_body (Tree.Node seL4_CapRights_get_capAllowWrite_'proc kernel_all_substitute.seL4_CapRights_get_capAllowWrite_body (Tree.Node generic_frame_cap_get_capFBasePtr_'proc kernel_all_substitute.generic_frame_cap_get_capFBasePtr_body (Tree.Node notification_ptr_get_ntfnBoundTCB_'proc kernel_all_substitute.notification_ptr_get_ntfnBoundTCB_body (Tree.Node notification_ptr_set_ntfnBoundTCB_'proc kernel_all_substitute.notification_ptr_set_ntfnBoundTCB_body Leaf Leaf) Leaf) (Tree.Node cap_asid_pool_cap_get_capASIDBase_'proc kernel_all_substitute.cap_asid_pool_cap_get_capASIDBase_body (Tree.Node cap_asid_pool_cap_get_capASIDPool_'proc kernel_all_substitute.cap_asid_pool_cap_get_capASIDPool_body Leaf Leaf) Leaf)) (Tree.Node invokeIRQHandler_ClearIRQHandler_'proc (kernel_all_substitute.invokeIRQHandler_ClearIRQHandler_body symbol_table) (Tree.Node seL4_CNode_CapData_get_guardSize_'proc kernel_all_substitute.seL4_CNode_CapData_get_guardSize_body (Tree.Node seL4_CapRights_get_capAllowGrant_'proc kernel_all_substitute.seL4_CapRights_get_capAllowGrant_body Leaf Leaf) Leaf) (Tree.Node endpoint_ptr_set_epQueue_head_np_'proc kernel_all_substitute.endpoint_ptr_set_epQueue_head_np_body (Tree.Node invalidateTranslationSingleLocal_'proc kernel_all_global_addresses.invalidateTranslationSingleLocal_body Leaf Leaf) Leaf))) (Tree.Node cap_reply_cap_get_capReplyMaster_'proc kernel_all_substitute.cap_reply_cap_get_capReplyMaster_body (Tree.Node cap_untyped_cap_set_capFreeIndex_'proc kernel_all_substitute.cap_untyped_cap_set_capFreeIndex_body (Tree.Node cap_zombie_cap_get_capZombieBits_'proc kernel_all_substitute.cap_zombie_cap_get_capZombieBits_body (Tree.Node cap_zombie_cap_get_capZombieType_'proc kernel_all_substitute.cap_zombie_cap_get_capZombieType_body Leaf Leaf) Leaf) (Tree.Node cap_untyped_cap_get_capBlockSize_'proc kernel_all_substitute.cap_untyped_cap_get_capBlockSize_body (Tree.Node cap_untyped_cap_get_capFreeIndex_'proc kernel_all_substitute.cap_untyped_cap_get_capFreeIndex_body Leaf Leaf) Leaf)) (Tree.Node cap_endpoint_cap_set_capCanGrant_'proc kernel_all_substitute.cap_endpoint_cap_set_capCanGrant_body (Tree.Node cap_frame_cap_get_capFMappedASID_'proc kernel_all_substitute.cap_frame_cap_get_capFMappedASID_body (Tree.Node cap_frame_cap_set_capFMappedASID_'proc kernel_all_substitute.cap_frame_cap_set_capFMappedASID_body Leaf Leaf) Leaf) (Tree.Node seL4_Fault_CapFault_get_address_'proc kernel_all_substitute.seL4_Fault_CapFault_get_address_body (Tree.Node cap_endpoint_cap_get_capCanGrant_'proc kernel_all_substitute.cap_endpoint_cap_get_capCanGrant_body Leaf Leaf) Leaf)))) (Tree.Node cap_cnode_cap_set_capCNodeGuard_'proc kernel_all_substitute.cap_cnode_cap_set_capCNodeGuard_body (Tree.Node cap_zombie_cap_get_capZombiePtr_'proc kernel_all_substitute.cap_zombie_cap_get_capZombiePtr_body (Tree.Node mdb_node_ptr_set_mdbFirstBadged_'proc kernel_all_substitute.mdb_node_ptr_set_mdbFirstBadged_body (Tree.Node pde_pde_section_ptr_get_address_'proc kernel_all_substitute.pde_pde_section_ptr_get_address_body (Tree.Node performPageTableInvocationUnmap_'proc kernel_all_substitute.performPageTableInvocationUnmap_body Leaf Leaf) Leaf) (Tree.Node lookup_fault_depth_mismatch_new_'proc kernel_all_substitute.lookup_fault_depth_mismatch_new_body (Tree.Node lookup_fault_guard_mismatch_new_'proc kernel_all_substitute.lookup_fault_guard_mismatch_new_body Leaf Leaf) Leaf)) (Tree.Node cap_endpoint_cap_set_capCanSend_'proc kernel_all_substitute.cap_endpoint_cap_set_capCanSend_body (Tree.Node cap_endpoint_cap_set_capEPBadge_'proc kernel_all_substitute.cap_endpoint_cap_set_capEPBadge_body (Tree.Node cap_untyped_cap_get_capIsDevice_'proc kernel_all_substitute.cap_untyped_cap_get_capIsDevice_body Leaf Leaf) Leaf) (Tree.Node cap_endpoint_cap_get_capCanSend_'proc kernel_all_substitute.cap_endpoint_cap_get_capCanSend_body (Tree.Node cap_endpoint_cap_get_capEPBadge_'proc kernel_all_substitute.cap_endpoint_cap_get_capEPBadge_body Leaf Leaf) Leaf))) (Tree.Node thread_state_ptr_set_tcbQueued_'proc kernel_all_substitute.thread_state_ptr_set_tcbQueued_body (Tree.Node arch_clean_invalidate_L1_caches_'proc kernel_all_global_addresses.arch_clean_invalidate_L1_caches_body (Tree.Node cap_cnode_cap_get_capCNodeGuard_'proc kernel_all_substitute.cap_cnode_cap_get_capCNodeGuard_body (Tree.Node cap_cnode_cap_get_capCNodeRadix_'proc kernel_all_substitute.cap_cnode_cap_get_capCNodeRadix_body Leaf Leaf) Leaf) (Tree.Node thread_state_ptr_set_tsType_np_'proc kernel_all_substitute.thread_state_ptr_set_tsType_np_body (Tree.Node Arch_decodeIRQControlInvocation_'proc kernel_all_substitute.Arch_decodeIRQControlInvocation_body Leaf Leaf) Leaf)) (Tree.Node seL4_Fault_VMFault_get_address_'proc kernel_all_substitute.seL4_Fault_VMFault_get_address_body (Tree.Node seL4_MessageInfo_get_extraCaps_'proc kernel_all_substitute.seL4_MessageInfo_get_extraCaps_body (Tree.Node seL4_MessageInfo_set_extraCaps_'proc kernel_all_substitute.seL4_MessageInfo_set_extraCaps_body Leaf Leaf) Leaf) (Tree.Node performInvocation_Notification_'proc kernel_all_global_addresses.performInvocation_Notification_body (Tree.Node pte_pte_large_ptr_get_reserved_'proc kernel_all_substitute.pte_pte_large_ptr_get_reserved_body Leaf Leaf) Leaf))))) (Tree.Node endpoint_ptr_get_epQueue_tail_'proc kernel_all_substitute.endpoint_ptr_get_epQueue_tail_body (Tree.Node seL4_Fault_get_seL4_FaultType_'proc kernel_all_global_addresses.seL4_Fault_get_seL4_FaultType_body (Tree.Node cap_irq_handler_cap_get_capIRQ_'proc kernel_all_substitute.cap_irq_handler_cap_get_capIRQ_body (Tree.Node generic_frame_cap_get_capFSize_'proc kernel_all_substitute.generic_frame_cap_get_capFSize_body (Tree.Node invalidateTranslationASIDLocal_'proc kernel_all_global_addresses.invalidateTranslationASIDLocal_body (Tree.Node invokeIRQHandler_SetIRQHandler_'proc (kernel_all_substitute.invokeIRQHandler_SetIRQHandler_body symbol_table) Leaf Leaf) Leaf) (Tree.Node cap_zombie_cap_get_capZombieID_'proc kernel_all_substitute.cap_zombie_cap_get_capZombieID_body (Tree.Node cap_zombie_cap_set_capZombieID_'proc kernel_all_substitute.cap_zombie_cap_set_capZombieID_body Leaf Leaf) Leaf)) (Tree.Node cap_frame_cap_get_capFIsDevice_'proc kernel_all_substitute.cap_frame_cap_get_capFIsDevice_body (Tree.Node cap_frame_cap_get_capFVMRights_'proc kernel_all_substitute.cap_frame_cap_get_capFVMRights_body (Tree.Node cap_frame_cap_set_capFVMRights_'proc kernel_all_substitute.cap_frame_cap_set_capFVMRights_body Leaf Leaf) Leaf) (Tree.Node writeAuxiliaryControlRegister_'proc kernel_all_global_addresses.writeAuxiliaryControlRegister_body (Tree.Node c_handle_undefined_instruction_'proc kernel_all_global_addresses.c_handle_undefined_instruction_body Leaf Leaf) Leaf))) (Tree.Node mdb_node_ptr_set_mdbRevocable_'proc kernel_all_substitute.mdb_node_ptr_set_mdbRevocable_body (Tree.Node pte_pte_small_ptr_get_address_'proc kernel_all_substitute.pte_pte_small_ptr_get_address_body (Tree.Node replyFromKernel_success_empty_'proc kernel_all_substitute.replyFromKernel_success_empty_body (Tree.Node seL4_Fault_UnknownSyscall_new_'proc kernel_all_substitute.seL4_Fault_UnknownSyscall_new_body Leaf Leaf) Leaf) (Tree.Node performPageTableInvocationMap_'proc kernel_all_substitute.performPageTableInvocationMap_body (Tree.Node pte_pte_large_ptr_get_address_'proc kernel_all_substitute.pte_pte_large_ptr_get_address_body Leaf Leaf) Leaf)) (Tree.Node invalidateTranslationAllLocal_'proc kernel_all_global_addresses.invalidateTranslationAllLocal_body (Tree.Node invokeTCB_NotificationControl_'proc kernel_all_global_addresses.invokeTCB_NotificationControl_body (Tree.Node lookup_fault_invalid_root_new_'proc kernel_all_substitute.lookup_fault_invalid_root_new_body Leaf Leaf) Leaf) (Tree.Node endpoint_ptr_set_epQueue_head_'proc kernel_all_substitute.endpoint_ptr_set_epQueue_head_body (Tree.Node endpoint_ptr_set_epQueue_tail_'proc kernel_all_substitute.endpoint_ptr_set_epQueue_tail_body Leaf Leaf) Leaf)))) (Tree.Node pde_pde_section_ptr_get_size_'proc kernel_all_substitute.pde_pde_section_ptr_get_size_body (Tree.Node StrictC'__builtin_unreachable_'proc kernel_all_global_addresses.StrictC'__builtin_unreachable_body (Tree.Node cap_frame_cap_get_capFBasePtr_'proc kernel_all_substitute.cap_frame_cap_get_capFBasePtr_body (Tree.Node cleanInvalidateCacheRange_RAM_'proc kernel_all_global_addresses.cleanInvalidateCacheRange_RAM_body (Tree.Node endpoint_ptr_get_epQueue_head_'proc kernel_all_substitute.endpoint_ptr_get_epQueue_head_body Leaf Leaf) Leaf) (Tree.Node cap_cnode_cap_get_capCNodePtr_'proc kernel_all_substitute.cap_cnode_cap_get_capCNodePtr_body (Tree.Node cap_endpoint_cap_get_capEPPtr_'proc kernel_all_substitute.cap_endpoint_cap_get_capEPPtr_body Leaf Leaf) Leaf)) (Tree.Node readAuxiliaryControlRegister_'proc kernel_all_substitute.readAuxiliaryControlRegister_body (Tree.Node seL4_CNode_CapData_get_guard_'proc kernel_all_substitute.seL4_CNode_CapData_get_guard_body (Tree.Node seL4_Fault_UserException_new_'proc kernel_all_substitute.seL4_Fault_UserException_new_body Leaf Leaf) Leaf) (Tree.Node performASIDControlInvocation_'proc (kernel_all_substitute.performASIDControlInvocation_body domain) (Tree.Node performPageInvocationUnmapIO_'proc kernel_all_global_addresses.performPageInvocationUnmapIO_body Leaf Leaf) Leaf))) (Tree.Node cap_thread_cap_get_capTCBPtr_'proc kernel_all_substitute.cap_thread_cap_get_capTCBPtr_body (Tree.Node create_unmapped_it_frame_cap_'proc kernel_all_substitute.create_unmapped_it_frame_cap_body (Tree.Node decodeARMPageTableInvocation_'proc kernel_all_substitute.decodeARMPageTableInvocation_body (Tree.Node invokeCNodeCancelBadgedSends_'proc kernel_all_substitute.invokeCNodeCancelBadgedSends_body Leaf Leaf) Leaf) (Tree.Node createSafeMappingEntries_PDE_'proc kernel_all_substitute.createSafeMappingEntries_PDE_body (Tree.Node createSafeMappingEntries_PTE_'proc kernel_all_substitute.createSafeMappingEntries_PTE_body Leaf Leaf) Leaf)) (Tree.Node arch_clean_invalidate_caches_'proc kernel_all_global_addresses.arch_clean_invalidate_caches_body (Tree.Node c_handle_fastpath_reply_recv_'proc kernel_all_global_addresses.c_handle_fastpath_reply_recv_body (Tree.Node calculate_extra_bi_size_bits_'proc kernel_all_substitute.calculate_extra_bi_size_bits_body Leaf Leaf) Leaf) (Tree.Node Arch_getSanitiseRegisterInfo_'proc kernel_all_global_addresses.Arch_getSanitiseRegisterInfo_body Leaf Leaf))))))) (Tree.Node endpoint_ptr_get_state_'proc kernel_all_substitute.endpoint_ptr_get_state_body (Tree.Node pde_pde_section_get_size_'proc kernel_all_substitute.pde_pde_section_get_size_body (Tree.Node decodeIRQControlInvocation_'proc kernel_all_substitute.decodeIRQControlInvocation_body (Tree.Node cap_reply_cap_get_capTCBPtr_'proc kernel_all_substitute.cap_reply_cap_get_capTCBPtr_body (Tree.Node performPageInvocationMapPTE_'proc kernel_all_substitute.performPageInvocationMapPTE_body (Tree.Node seL4_MessageInfo_get_length_'proc kernel_all_substitute.seL4_MessageInfo_get_length_body (Tree.Node seL4_MessageInfo_set_length_'proc kernel_all_substitute.seL4_MessageInfo_set_length_body (Tree.Node thread_state_ptr_get_tsType_'proc kernel_all_substitute.thread_state_ptr_get_tsType_body Leaf Leaf) Leaf) (Tree.Node plat_cleanInvalidateL2Cache_'proc kernel_all_substitute.plat_cleanInvalidateL2Cache_body (Tree.Node plat_cleanInvalidateL2Range_'proc kernel_all_substitute.plat_cleanInvalidateL2Range_body Leaf Leaf) Leaf)) (Tree.Node mdb_node_ptr_set_mdbPrev_np_'proc kernel_all_substitute.mdb_node_ptr_set_mdbPrev_np_body (Tree.Node mdb_node_set_mdbFirstBadged_'proc kernel_all_substitute.mdb_node_set_mdbFirstBadged_body (Tree.Node performPageInvocationMapPDE_'proc kernel_all_substitute.performPageInvocationMapPDE_body Leaf Leaf) Leaf) (Tree.Node invalidateTranslationSingle_'proc kernel_all_global_addresses.invalidateTranslationSingle_body (Tree.Node mdb_node_get_mdbFirstBadged_'proc kernel_all_substitute.mdb_node_get_mdbFirstBadged_body Leaf Leaf) Leaf))) (Tree.Node performPageInvocationUnmap_'proc kernel_all_substitute.performPageInvocationUnmap_body (Tree.Node seL4_MessageInfo_get_label_'proc kernel_all_substitute.seL4_MessageInfo_get_label_body (Tree.Node thread_state_get_tcbQueued_'proc kernel_all_substitute.thread_state_get_tcbQueued_body (Tree.Node writeSystemControlRegister_'proc kernel_all_global_addresses.writeSystemControlRegister_body Leaf Leaf) Leaf) (Tree.Node pte_pte_large_get_reserved_'proc kernel_all_substitute.pte_pte_large_get_reserved_body (Tree.Node seL4_Fault_VMFault_get_FSR_'proc kernel_all_substitute.seL4_Fault_VMFault_get_FSR_body Leaf Leaf) Leaf)) (Tree.Node notification_ptr_set_state_'proc kernel_all_substitute.notification_ptr_set_state_body (Tree.Node pde_pde_coarse_get_address_'proc kernel_all_substitute.pde_pde_coarse_get_address_body (Tree.Node performInvocation_Endpoint_'proc kernel_all_global_addresses.performInvocation_Endpoint_body Leaf Leaf) Leaf) (Tree.Node decodeIRQHandlerInvocation_'proc kernel_all_substitute.decodeIRQHandlerInvocation_body (Tree.Node notification_ptr_get_state_'proc kernel_all_substitute.notification_ptr_get_state_body Leaf Leaf) Leaf)))) (Tree.Node mdb_node_set_mdbRevocable_'proc kernel_all_substitute.mdb_node_set_mdbRevocable_body (Tree.Node cap_untyped_cap_get_capPtr_'proc kernel_all_substitute.cap_untyped_cap_get_capPtr_body (Tree.Node create_mapped_it_frame_cap_'proc kernel_all_substitute.create_mapped_it_frame_cap_body (Tree.Node create_untypeds_for_region_'proc kernel_all_substitute.create_untypeds_for_region_body (Tree.Node decodeARMIOSpaceInvocation_'proc kernel_all_global_addresses.decodeARMIOSpaceInvocation_body Leaf Leaf) Leaf) (Tree.Node cleanInvalidate_D_by_level_'proc kernel_all_substitute.cleanInvalidate_D_by_level_body (Tree.Node cpu_initLocalIRQController_'proc kernel_all_global_addresses.cpu_initLocalIRQController_body Leaf Leaf) Leaf)) (Tree.Node c_handle_instruction_fault_'proc kernel_all_substitute.c_handle_instruction_fault_body (Tree.Node cap_frame_cap_get_capFSize_'proc kernel_all_substitute.cap_frame_cap_get_capFSize_body (Tree.Node cap_page_directory_cap_new_'proc kernel_all_substitute.cap_page_directory_cap_new_body Leaf Leaf) Leaf) (Tree.Node performASIDPoolInvocation_'proc kernel_all_substitute.performASIDPoolInvocation_body (Tree.Node readSystemControlRegister_'proc kernel_all_substitute.readSystemControlRegister_body Leaf Leaf) Leaf))) (Tree.Node cap_get_archCapIsPhysical_'proc kernel_all_substitute.cap_get_archCapIsPhysical_body (Tree.Node invalidateLocalTLB_VAASID_'proc kernel_all_global_addresses.invalidateLocalTLB_VAASID_body (Tree.Node invalidateTranslationASID_'proc kernel_all_global_addresses.invalidateTranslationASID_body (Tree.Node mdb_node_get_mdbRevocable_'proc kernel_all_substitute.mdb_node_get_mdbRevocable_body Leaf Leaf) Leaf) (Tree.Node create_rootserver_objects_'proc kernel_all_substitute.create_rootserver_objects_body (Tree.Node get_p_reg_kernel_img_boot_'proc (kernel_all_substitute.get_p_reg_kernel_img_boot_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node slotCapLongRunningDelete_'proc kernel_all_substitute.slotCapLongRunningDelete_body (Tree.Node armv_contextSwitch_HWASID_'proc (kernel_all_substitute.armv_contextSwitch_HWASID_body symbol_table) (Tree.Node calculate_rootserver_size_'proc kernel_all_substitute.calculate_rootserver_size_body Leaf Leaf) Leaf) (Tree.Node rootserver_max_size_bits_'proc kernel_all_substitute.rootserver_max_size_bits_body (Tree.Node seL4_Fault_NullFault_new_'proc kernel_all_substitute.seL4_Fault_NullFault_new_body Leaf Leaf) Leaf))))) (Tree.Node messageInfoFromWord_raw_'proc kernel_all_substitute.messageInfoFromWord_raw_body (Tree.Node cap_reply_cap_ptr_new_np_'proc kernel_all_substitute.cap_reply_cap_ptr_new_np_body (Tree.Node invalidateCacheRange_RAM_'proc kernel_all_global_addresses.invalidateCacheRange_RAM_body (Tree.Node lookup_fault_get_lufType_'proc kernel_all_global_addresses.lookup_fault_get_lufType_body (Tree.Node mdb_node_ptr_set_mdbNext_'proc kernel_all_substitute.mdb_node_ptr_set_mdbNext_body (Tree.Node mdb_node_ptr_set_mdbPrev_'proc kernel_all_substitute.mdb_node_ptr_set_mdbPrev_body Leaf Leaf) Leaf) (Tree.Node invalidateTranslationAll_'proc kernel_all_global_addresses.invalidateTranslationAll_body (Tree.Node invokeTCB_WriteRegisters_'proc kernel_all_substitute.invokeTCB_WriteRegisters_body Leaf Leaf) Leaf)) (Tree.Node decodeARMIOMapInvocation_'proc kernel_all_global_addresses.decodeARMIOMapInvocation_body (Tree.Node decodeUnbindNotification_'proc kernel_all_substitute.decodeUnbindNotification_body (Tree.Node fastpath_reply_cap_check_'proc kernel_all_global_addresses.fastpath_reply_cap_check_body Leaf Leaf) Leaf) (Tree.Node create_it_page_table_cap_'proc kernel_all_substitute.create_it_page_table_cap_body (Tree.Node decodeARMFrameInvocation_'proc kernel_all_substitute.decodeARMFrameInvocation_body Leaf Leaf) Leaf))) (Tree.Node unbindMaybeNotification_'proc kernel_all_substitute.unbindMaybeNotification_body (Tree.Node Arch_prepareThreadDelete_'proc kernel_all_global_addresses.Arch_prepareThreadDelete_body (Tree.Node cap_asid_control_cap_new_'proc kernel_all_substitute.cap_asid_control_cap_new_body (Tree.Node cap_notification_cap_new_'proc kernel_all_substitute.cap_notification_cap_new_body Leaf Leaf) Leaf) (Tree.Node Arch_configureIdleThread_'proc (kernel_all_global_addresses.Arch_configureIdleThread_body symbol_table) (Tree.Node Arch_postModifyRegisters_'proc kernel_all_global_addresses.Arch_postModifyRegisters_body Leaf Leaf) Leaf)) (Tree.Node seL4_Fault_CapFault_new_'proc kernel_all_substitute.seL4_Fault_CapFault_new_body (Tree.Node supportsAsyncExceptions_'proc kernel_all_substitute.supportsAsyncExceptions_body (Tree.Node thread_state_get_tsType_'proc kernel_all_substitute.thread_state_get_tsType_body Leaf Leaf) Leaf) (Tree.Node performInvocation_Reply_'proc kernel_all_global_addresses.performInvocation_Reply_body (Tree.Node scheduleChooseNewThread_'proc kernel_all_global_addresses.scheduleChooseNewThread_body Leaf Leaf) Leaf)))) (Tree.Node check_export_arch_timer_'proc kernel_all_substitute.check_export_arch_timer_body (Tree.Node decodeUntypedInvocation_'proc kernel_all_substitute.decodeUntypedInvocation_body (Tree.Node invokeTCB_CopyRegisters_'proc kernel_all_substitute.invokeTCB_CopyRegisters_body (Tree.Node invokeTCB_ReadRegisters_'proc kernel_all_substitute.invokeTCB_ReadRegisters_body (Tree.Node invokeTCB_ThreadControl_'proc kernel_all_substitute.invokeTCB_ThreadControl_body Leaf Leaf) Leaf) (Tree.Node invalidateLocalTLB_ASID_'proc kernel_all_global_addresses.invalidateLocalTLB_ASID_body (Tree.Node invokeIRQHandler_AckIRQ_'proc kernel_all_global_addresses.invokeIRQHandler_AckIRQ_body Leaf Leaf) Leaf)) (Tree.Node create_ipcbuf_frame_cap_'proc kernel_all_substitute.create_ipcbuf_frame_cap_body (Tree.Node create_it_address_space_'proc kernel_all_substitute.create_it_address_space_body (Tree.Node decodeARMIOPTInvocation_'proc kernel_all_global_addresses.decodeARMIOPTInvocation_body Leaf Leaf) Leaf) (Tree.Node cleanInvalidateL1Caches_'proc kernel_all_global_addresses.cleanInvalidateL1Caches_body (Tree.Node create_frames_of_region_'proc kernel_all_substitute.create_frames_of_region_body Leaf Leaf) Leaf))) (Tree.Node Arch_activateIdleThread_'proc kernel_all_global_addresses.Arch_activateIdleThread_body (Tree.Node cap_irq_control_cap_new_'proc kernel_all_substitute.cap_irq_control_cap_new_body (Tree.Node cap_irq_handler_cap_new_'proc kernel_all_substitute.cap_irq_handler_cap_new_body (Tree.Node cap_small_frame_cap_new_'proc kernel_all_substitute.cap_small_frame_cap_new_body Leaf Leaf) Leaf) (Tree.Node Arch_switchToIdleThread_'proc kernel_all_global_addresses.Arch_switchToIdleThread_body (Tree.Node cap_get_archCapSizeBits_'proc kernel_all_substitute.cap_get_archCapSizeBits_body Leaf Leaf) Leaf)) (Tree.Node invalidateCacheRange_I_'proc kernel_all_global_addresses.invalidateCacheRange_I_body (Tree.Node plat_invalidateL2Range_'proc kernel_all_substitute.plat_invalidateL2Range_body (Tree.Node seL4_Fault_VMFault_new_'proc kernel_all_substitute.seL4_Fault_VMFault_new_body Leaf Leaf) Leaf) (Tree.Node endpoint_ptr_set_state_'proc kernel_all_substitute.endpoint_ptr_set_state_body Leaf Leaf)))))) (Tree.Node Arch_performTransfer_'proc kernel_all_global_addresses.Arch_performTransfer_body (Tree.Node Arch_decodeInvocation_'proc kernel_all_substitute.Arch_decodeInvocation_body (Tree.Node performPageGetAddress_'proc kernel_all_substitute.performPageGetAddress_body (Tree.Node cap_page_table_cap_new_'proc kernel_all_substitute.cap_page_table_cap_new_body (Tree.Node decodeBindNotification_'proc kernel_all_substitute.decodeBindNotification_body (Tree.Node decodeDomainInvocation_'proc kernel_all_substitute.decodeDomainInvocation_body (Tree.Node doNBRecvFailedTransfer_'proc kernel_all_global_addresses.doNBRecvFailedTransfer_body Leaf Leaf) Leaf) (Tree.Node check_available_memory_'proc kernel_all_substitute.check_available_memory_body (Tree.Node decodeARMMMUInvocation_'proc kernel_all_substitute.decodeARMMMUInvocation_body Leaf Leaf) Leaf)) (Tree.Node setMRs_lookup_failure_'proc kernel_all_substitute.setMRs_lookup_failure_body (Tree.Node activate_kernel_vspace_'proc (kernel_all_substitute.activate_kernel_vspace_body symbol_table) (Tree.Node c_handle_fastpath_call_'proc kernel_all_global_addresses.c_handle_fastpath_call_body Leaf Leaf) Leaf) (Tree.Node pptr_in_kernel_window_'proc kernel_all_global_addresses.pptr_in_kernel_window_body (Tree.Node replyFromKernel_error_'proc kernel_all_substitute.replyFromKernel_error_body Leaf Leaf) Leaf))) (Tree.Node ceiling_kernel_window_'proc kernel_all_substitute.ceiling_kernel_window_body (Tree.Node create_initial_thread_'proc kernel_all_substitute.create_initial_thread_body (Tree.Node decodeCNodeInvocation_'proc kernel_all_substitute.decodeCNodeInvocation_body (Tree.Node invokeCNodeSaveCaller_'proc kernel_all_substitute.invokeCNodeSaveCaller_body Leaf Leaf) Leaf) (Tree.Node check_reserved_memory_'proc kernel_all_substitute.check_reserved_memory_body (Tree.Node cleanInvalidate_D_PoC_'proc kernel_all_substitute.cleanInvalidate_D_PoC_body Leaf Leaf) Leaf)) (Tree.Node armv_init_user_access_'proc kernel_all_substitute.armv_init_user_access_body (Tree.Node cap_asid_pool_cap_new_'proc kernel_all_substitute.cap_asid_pool_cap_new_body (Tree.Node cap_get_capIsPhysical_'proc kernel_all_substitute.cap_get_capIsPhysical_body Leaf Leaf) Leaf) (Tree.Node Arch_handleFaultReply_'proc kernel_all_substitute.Arch_handleFaultReply_body (Tree.Node Arch_invokeIRQControl_'proc kernel_all_substitute.Arch_invokeIRQControl_body Leaf Leaf) Leaf)))) (Tree.Node handleUnknownSyscall_'proc kernel_all_substitute.handleUnknownSyscall_body (Tree.Node mdb_node_get_mdbNext_'proc kernel_all_substitute.mdb_node_get_mdbNext_body (Tree.Node seL4_MessageInfo_new_'proc kernel_all_substitute.seL4_MessageInfo_new_body (Tree.Node setMRs_syscall_error_'proc kernel_all_substitute.setMRs_syscall_error_body (Tree.Node vmAttributesFromWord_'proc kernel_all_substitute.vmAttributesFromWord_body Leaf Leaf) Leaf) (Tree.Node mdb_node_get_mdbPrev_'proc kernel_all_substitute.mdb_node_get_mdbPrev_body (Tree.Node mdb_node_set_mdbPrev_'proc kernel_all_substitute.mdb_node_set_mdbPrev_body Leaf Leaf) Leaf)) (Tree.Node isValidVTableRoot_fp_'proc kernel_all_global_addresses.isValidVTableRoot_fp_body (Tree.Node lookupSlotForCNodeOp_'proc kernel_all_substitute.lookupSlotForCNodeOp_body (Tree.Node maybe_alloc_extra_bi_'proc kernel_all_substitute.maybe_alloc_extra_bi_body Leaf Leaf) Leaf) (Tree.Node handleUserLevelFault_'proc kernel_all_substitute.handleUserLevelFault_body (Tree.Node invokeUntyped_Retype_'proc kernel_all_substitute.invokeUntyped_Retype_body Leaf Leaf) Leaf))) (Tree.Node clearIOPageDirectory_'proc kernel_all_global_addresses.clearIOPageDirectory_body (Tree.Node doUnbindNotification_'proc kernel_all_substitute.doUnbindNotification_body (Tree.Node get_p_reg_kernel_img_'proc (kernel_all_substitute.get_p_reg_kernel_img_body symbol_table) (Tree.Node handleInterruptEntry_'proc kernel_all_substitute.handleInterruptEntry_body Leaf Leaf) Leaf) (Tree.Node decodeSetSchedParams_'proc kernel_all_substitute.decodeSetSchedParams_body (Tree.Node decodeWriteRegisters_'proc kernel_all_substitute.decodeWriteRegisters_body Leaf Leaf) Leaf)) (Tree.Node capTransferFromWords_'proc kernel_all_substitute.capTransferFromWords_body (Tree.Node cap_endpoint_cap_new_'proc kernel_all_substitute.cap_endpoint_cap_new_body (Tree.Node cleanInvalidateByWSL_'proc kernel_all_global_addresses.cleanInvalidateByWSL_body Leaf Leaf) Leaf) (Tree.Node Arch_postCapDeletion_'proc kernel_all_global_addresses.Arch_postCapDeletion_body (Tree.Node alloc_rootserver_obj_'proc kernel_all_substitute.alloc_rootserver_obj_body Leaf Leaf) Leaf))))) (Tree.Node create_bi_frame_cap_'proc kernel_all_substitute.create_bi_frame_cap_body (Tree.Node lookupPTSlot_nofail_'proc kernel_all_substitute.lookupPTSlot_nofail_body (Tree.Node pte_pte_invalid_new_'proc kernel_all_global_addresses.pte_pte_invalid_new_body (Tree.Node setUntypedCapAsFull_'proc kernel_all_substitute.setUntypedCapAsFull_body (Tree.Node wordFromMessageInfo_'proc kernel_all_global_addresses.wordFromMessageInfo_body (Tree.Node writeContextIDAndPD_'proc kernel_all_global_addresses.writeContextIDAndPD_body Leaf Leaf) Leaf) (Tree.Node pte_ptr_get_pteSize_'proc kernel_all_substitute.pte_ptr_get_pteSize_body (Tree.Node pte_ptr_get_pteType_'proc kernel_all_substitute.pte_ptr_get_pteType_body Leaf Leaf) Leaf)) (Tree.Node pde_pde_section_new_'proc kernel_all_substitute.pde_pde_section_new_body (Tree.Node pde_ptr_get_pdeType_'proc kernel_all_substitute.pde_ptr_get_pdeType_body (Tree.Node provide_untyped_cap_'proc kernel_all_substitute.provide_untyped_cap_body Leaf Leaf) Leaf) (Tree.Node messageInfoFromWord_'proc kernel_all_substitute.messageInfoFromWord_body (Tree.Node pde_pde_invalid_new_'proc kernel_all_substitute.pde_pde_invalid_new_body Leaf Leaf) Leaf))) (Tree.Node decodeSetMCPriority_'proc kernel_all_substitute.decodeSetMCPriority_body (Tree.Node hasCancelSendRights_'proc kernel_all_substitute.hasCancelSendRights_body (Tree.Node invalidateASIDEntry_'proc kernel_all_substitute.invalidateASIDEntry_body (Tree.Node invalidateTLBByASID_'proc kernel_all_substitute.invalidateTLBByASID_body Leaf Leaf) Leaf) (Tree.Node decodeTCBInvocation_'proc kernel_all_substitute.decodeTCBInvocation_body (Tree.Node fastpath_reply_recv_'proc kernel_all_substitute.fastpath_reply_recv_body Leaf Leaf) Leaf)) (Tree.Node create_it_frame_cap_'proc kernel_all_substitute.create_it_frame_cap_body (Tree.Node decodeCopyRegisters_'proc kernel_all_substitute.decodeCopyRegisters_body (Tree.Node decodeReadRegisters_'proc kernel_all_substitute.decodeReadRegisters_body Leaf Leaf) Leaf) (Tree.Node create_iospace_caps_'proc kernel_all_global_addresses.create_iospace_caps_body (Tree.Node create_it_asid_pool_'proc kernel_all_substitute.create_it_asid_pool_body Leaf Leaf) Leaf)))) (Tree.Node Arch_isCapRevocable_'proc kernel_all_global_addresses.Arch_isCapRevocable_body (Tree.Node checkValidIPCBuffer_'proc kernel_all_substitute.checkValidIPCBuffer_body (Tree.Node cleanCacheRange_RAM_'proc kernel_all_global_addresses.cleanCacheRange_RAM_body (Tree.Node cleanInvalidate_L1D_'proc kernel_all_substitute.cleanInvalidate_L1D_body (Tree.Node configureIdleThread_'proc kernel_all_global_addresses.configureIdleThread_body Leaf Leaf) Leaf) (Tree.Node cleanCacheRange_PoC_'proc kernel_all_global_addresses.cleanCacheRange_PoC_body (Tree.Node cleanCacheRange_PoU_'proc kernel_all_global_addresses.cleanCacheRange_PoU_body Leaf Leaf) Leaf)) (Tree.Node c_handle_data_fault_'proc kernel_all_substitute.c_handle_data_fault_body (Tree.Node cap_get_capSizeBits_'proc kernel_all_substitute.cap_get_capSizeBits_body (Tree.Node cap_untyped_cap_new_'proc kernel_all_substitute.cap_untyped_cap_new_body Leaf Leaf) Leaf) (Tree.Node Arch_setTLSRegister_'proc kernel_all_global_addresses.Arch_setTLSRegister_body (Tree.Node Arch_switchToThread_'proc kernel_all_global_addresses.Arch_switchToThread_body Leaf Leaf) Leaf))) (Tree.Node rescheduleRequired_'proc kernel_all_substitute.rescheduleRequired_body (Tree.Node unbindNotification_'proc kernel_all_substitute.unbindNotification_body (Tree.Node write_it_asid_pool_'proc kernel_all_substitute.write_it_asid_pool_body (Tree.Node Arch_decodeTransfer_'proc kernel_all_global_addresses.Arch_decodeTransfer_body Leaf Leaf) Leaf) (Tree.Node resolveAddressBits_'proc kernel_all_substitute.resolveAddressBits_body (Tree.Node switchToIdleThread_'proc kernel_all_global_addresses.switchToIdleThread_body Leaf Leaf) Leaf)) (Tree.Node ntfn_ptr_set_queue_'proc kernel_all_global_addresses.ntfn_ptr_set_queue_body (Tree.Node pde_pde_coarse_new_'proc kernel_all_substitute.pde_pde_coarse_new_body (Tree.Node ready_queues_index_'proc kernel_all_substitute.ready_queues_index_body Leaf Leaf) Leaf) (Tree.Node ntfn_ptr_get_queue_'proc kernel_all_substitute.ntfn_ptr_get_queue_body Leaf Leaf)))))))) (Tree.Node maskCapRights_'proc kernel_all_substitute.maskCapRights_body (Tree.Node decodeSetTLSBase_'proc kernel_all_substitute.decodeSetTLSBase_body (Tree.Node deleteIOPageTable_'proc kernel_all_global_addresses.deleteIOPageTable_body (Tree.Node switchToThread_fp_'proc kernel_all_substitute.switchToThread_fp_body (Tree.Node cap_domain_cap_new_'proc kernel_all_substitute.cap_domain_cap_new_body (Tree.Node decodeSetIPCBuffer_'proc kernel_all_substitute.decodeSetIPCBuffer_body (Tree.Node enableFpuInstInHyp_'proc kernel_all_global_addresses.enableFpuInstInHyp_body (Tree.Node handleVMFaultEvent_'proc kernel_all_substitute.handleVMFaultEvent_body (Tree.Node invalidateLocalTLB_'proc kernel_all_global_addresses.invalidateLocalTLB_body Leaf Leaf) Leaf) (Tree.Node decodeTCBConfigure_'proc kernel_all_substitute.decodeTCBConfigure_body (Tree.Node deletingIRQHandler_'proc (kernel_all_substitute.deletingIRQHandler_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node cap_zombie_cap_new_'proc kernel_all_substitute.cap_zombie_cap_new_body (Tree.Node copyGlobalMappings_'proc (kernel_all_substitute.copyGlobalMappings_body symbol_table) (Tree.Node create_idle_thread_'proc (kernel_all_substitute.create_idle_thread_body symbol_table) Leaf Leaf) Leaf) (Tree.Node cap_get_archCapPtr_'proc kernel_all_substitute.cap_get_archCapPtr_body (Tree.Node cap_thread_cap_new_'proc kernel_all_substitute.cap_thread_cap_new_body Leaf Leaf) Leaf))) (Tree.Node addressTranslateS1_'proc kernel_all_substitute.addressTranslateS1_body (Tree.Node armv_contextSwitch_'proc kernel_all_substitute.armv_contextSwitch_body (Tree.Node c_handle_interrupt_'proc kernel_all_global_addresses.c_handle_interrupt_body (Tree.Node cap_capType_equals_'proc kernel_all_global_addresses.cap_capType_equals_body Leaf Leaf) Leaf) (Tree.Node arm_load_thread_id_'proc kernel_all_substitute.arm_load_thread_id_body (Tree.Node arm_save_thread_id_'proc kernel_all_substitute.arm_save_thread_id_body Leaf Leaf) Leaf)) (Tree.Node Arch_getObjectSize_'proc kernel_all_substitute.Arch_getObjectSize_body (Tree.Node Arch_maskCapRights_'proc kernel_all_substitute.Arch_maskCapRights_body (Tree.Node Arch_updateCapData_'proc kernel_all_substitute.Arch_updateCapData_body Leaf Leaf) Leaf) (Tree.Node vm_attributes_new_'proc kernel_all_substitute.vm_attributes_new_body (Tree.Node writeContextIDPL2_'proc kernel_all_global_addresses.writeContextIDPL2_body Leaf Leaf) Leaf)))) (Tree.Node invokeTCB_Suspend_'proc kernel_all_global_addresses.invokeTCB_Suspend_body (Tree.Node plat_cleanL2Range_'proc kernel_all_substitute.plat_cleanL2Range_body (Tree.Node pte_pte_large_new_'proc kernel_all_substitute.pte_pte_large_new_body (Tree.Node pte_pte_small_new_'proc kernel_all_substitute.pte_pte_small_new_body (Tree.Node setVMRootForFlush_'proc kernel_all_substitute.setVMRootForFlush_body Leaf Leaf) Leaf) (Tree.Node populate_bi_frame_'proc kernel_all_substitute.populate_bi_frame_body (Tree.Node pptr_to_paddr_reg_'proc kernel_all_substitute.pptr_to_paddr_reg_body Leaf Leaf) Leaf)) (Tree.Node isValidVTableRoot_'proc kernel_all_substitute.isValidVTableRoot_body (Tree.Node map_kernel_window_'proc (kernel_all_substitute.map_kernel_window_body symbol_table) (Tree.Node paddr_to_pptr_reg_'proc kernel_all_substitute.paddr_to_pptr_reg_body Leaf Leaf) Leaf) (Tree.Node isFinalCapability_'proc kernel_all_substitute.isFinalCapability_body (Tree.Node isIOSpaceFrameCap_'proc kernel_all_global_addresses.isIOSpaceFrameCap_body Leaf Leaf) Leaf))) (Tree.Node handleSpuriousIRQ_'proc kernel_all_global_addresses.handleSpuriousIRQ_body (Tree.Node invokeCNodeInsert_'proc kernel_all_global_addresses.invokeCNodeInsert_body (Tree.Node invokeCNodeRevoke_'proc kernel_all_substitute.invokeCNodeRevoke_body (Tree.Node invokeCNodeRotate_'proc kernel_all_global_addresses.invokeCNodeRotate_body Leaf Leaf) Leaf) (Tree.Node initIRQController_'proc kernel_all_global_addresses.initIRQController_body (Tree.Node invokeCNodeDelete_'proc kernel_all_substitute.invokeCNodeDelete_body Leaf Leaf) Leaf)) (Tree.Node fastpath_mi_check_'proc kernel_all_global_addresses.fastpath_mi_check_body (Tree.Node handleDoubleFault_'proc kernel_all_global_addresses.handleDoubleFault_body (Tree.Node handleReservedIRQ_'proc kernel_all_global_addresses.handleReservedIRQ_body Leaf Leaf) Leaf) (Tree.Node deletedIRQHandler_'proc kernel_all_global_addresses.deletedIRQHandler_body (Tree.Node fastpath_copy_mrs_'proc kernel_all_substitute.fastpath_copy_mrs_body Leaf Leaf) Leaf))))) (Tree.Node pteCheckIfMapped_'proc kernel_all_substitute.pteCheckIfMapped_body (Tree.Node arch_get_n_paging_'proc kernel_all_substitute.arch_get_n_paging_body (Tree.Node cap_reply_cap_new_'proc kernel_all_substitute.cap_reply_cap_new_body (Tree.Node create_domain_cap_'proc kernel_all_substitute.create_domain_cap_body (Tree.Node create_root_cnode_'proc kernel_all_substitute.create_root_cnode_body (Tree.Node decodeSetPriority_'proc kernel_all_substitute.decodeSetPriority_body Leaf Leaf) Leaf) (Tree.Node clearExMonitor_fp_'proc kernel_all_global_addresses.clearExMonitor_fp_body (Tree.Node copyMRsFaultReply_'proc kernel_all_substitute.copyMRsFaultReply_body Leaf Leaf) Leaf)) (Tree.Node cancelBadgedSends_'proc kernel_all_substitute.cancelBadgedSends_body (Tree.Node cap_cnode_cap_new_'proc kernel_all_substitute.cap_cnode_cap_new_body (Tree.Node cap_frame_cap_new_'proc kernel_all_substitute.cap_frame_cap_new_body Leaf Leaf) Leaf) (Tree.Node arch_init_freemem_'proc (kernel_all_substitute.arch_init_freemem_body symbol_table) (Tree.Node c_handle_vm_fault_'proc kernel_all_global_addresses.c_handle_vm_fault_body Leaf Leaf) Leaf))) (Tree.Node wordFromVMRights_'proc kernel_all_substitute.wordFromVMRights_body (Tree.Node Arch_sameRegionAs_'proc kernel_all_substitute.Arch_sameRegionAs_body (Tree.Node Arch_setMRs_fault_'proc kernel_all_substitute.Arch_setMRs_fault_body (Tree.Node arch_c_entry_hook_'proc kernel_all_global_addresses.arch_c_entry_hook_body Leaf Leaf) Leaf) (Tree.Node Arch_createObject_'proc (kernel_all_substitute.Arch_createObject_body domain) (Tree.Node Arch_sameObjectAs_'proc kernel_all_substitute.Arch_sameObjectAs_body Leaf Leaf) Leaf)) (Tree.Node setupReplyMaster_'proc kernel_all_substitute.setupReplyMaster_body (Tree.Node trapFpuInstToHyp_'proc kernel_all_global_addresses.trapFpuInstToHyp_body (Tree.Node vmRightsFromWord_'proc kernel_all_substitute.vmRightsFromWord_body Leaf Leaf) Leaf) (Tree.Node removeFromBitmap_'proc kernel_all_substitute.removeFromBitmap_body (Tree.Node sanitiseRegister_'proc kernel_all_substitute.sanitiseRegister_body Leaf Leaf) Leaf)))) (Tree.Node invalidate_I_PoU_'proc kernel_all_global_addresses.invalidate_I_PoU_body (Tree.Node lookupTargetSlot_'proc kernel_all_substitute.lookupTargetSlot_body (Tree.Node pdeCheckIfMapped_'proc kernel_all_substitute.pdeCheckIfMapped_body (Tree.Node performPageFlush_'proc kernel_all_substitute.performPageFlush_body (Tree.Node possibleSwitchTo_'proc kernel_all_substitute.possibleSwitchTo_body Leaf Leaf) Leaf) (Tree.Node map_it_frame_cap_'proc kernel_all_substitute.map_it_frame_cap_body (Tree.Node map_kernel_frame_'proc (kernel_all_substitute.map_kernel_frame_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node invokeTCB_Resume_'proc kernel_all_global_addresses.invokeTCB_Resume_body (Tree.Node lookupCapAndSlot_'proc kernel_all_substitute.lookupCapAndSlot_body (Tree.Node lookupSourceSlot_'proc kernel_all_substitute.lookupSourceSlot_body Leaf Leaf) Leaf) (Tree.Node invokeIRQControl_'proc kernel_all_substitute.invokeIRQControl_body (Tree.Node invokeSetTLSBase_'proc kernel_all_global_addresses.invokeSetTLSBase_body Leaf Leaf) Leaf))) (Tree.Node fpsimd_HWCapTest_'proc kernel_all_substitute.fpsimd_HWCapTest_body (Tree.Node infer_cpu_gic_id_'proc kernel_all_substitute.infer_cpu_gic_id_body (Tree.Node invalidateByVA_I_'proc kernel_all_global_addresses.invalidateByVA_I_body (Tree.Node invalidateHypTLB_'proc kernel_all_global_addresses.invalidateHypTLB_body Leaf Leaf) Leaf) (Tree.Node handleFaultReply_'proc kernel_all_substitute.handleFaultReply_body (Tree.Node handleInvocation_'proc kernel_all_substitute.handleInvocation_body Leaf Leaf) Leaf)) (Tree.Node ensureNoChildren_'proc kernel_all_substitute.ensureNoChildren_body (Tree.Node ep_ptr_get_queue_'proc kernel_all_substitute.ep_ptr_get_queue_body (Tree.Node ep_ptr_set_queue_'proc kernel_all_global_addresses.ep_ptr_set_queue_body Leaf Leaf) Leaf) (Tree.Node doNormalTransfer_'proc kernel_all_substitute.doNormalTransfer_body Leaf Leaf)))))) (Tree.Node create_untypeds_'proc kernel_all_substitute.create_untypeds_body (Tree.Node prio_to_l1index_'proc kernel_all_global_addresses.prio_to_l1index_body (Tree.Node Arch_isFrameType_'proc kernel_all_substitute.Arch_isFrameType_body (Tree.Node capSwapForDelete_'proc kernel_all_substitute.capSwapForDelete_body (Tree.Node check_export_pmu_'proc kernel_all_global_addresses.check_export_pmu_body (Tree.Node createNewObjects_'proc (kernel_all_substitute.createNewObjects_body domain) (Tree.Node decodeInvocation_'proc kernel_all_substitute.decodeInvocation_body Leaf Leaf) Leaf) (Tree.Node cap_null_cap_new_'proc kernel_all_substitute.cap_null_cap_new_body (Tree.Node checkVPAlignment_'proc kernel_all_substitute.checkVPAlignment_body Leaf Leaf) Leaf)) (Tree.Node branchFlushRange_'proc kernel_all_global_addresses.branchFlushRange_body (Tree.Node c_handle_syscall_'proc kernel_all_global_addresses.c_handle_syscall_body (Tree.Node cancelAllSignals_'proc kernel_all_substitute.cancelAllSignals_body Leaf Leaf) Leaf) (Tree.Node arch_c_exit_hook_'proc kernel_all_global_addresses.arch_c_exit_hook_body (Tree.Node bindNotification_'proc kernel_all_substitute.bindNotification_body Leaf Leaf) Leaf))) (Tree.Node tcbSchedDequeue_'proc kernel_all_substitute.tcbSchedDequeue_body (Tree.Node updateRestartPC_'proc kernel_all_substitute.updateRestartPC_body (Tree.Node Arch_finaliseCap_'proc kernel_all_substitute.Arch_finaliseCap_body (Tree.Node Arch_initContext_'proc kernel_all_substitute.Arch_initContext_body Leaf Leaf) Leaf) (Tree.Node tcbSchedEnqueue_'proc kernel_all_substitute.tcbSchedEnqueue_body (Tree.Node try_init_kernel_'proc kernel_all_substitute.try_init_kernel_body Leaf Leaf) Leaf)) (Tree.Node resetUntypedCap_'proc (kernel_all_substitute.resetUntypedCap_body domain) (Tree.Node setCurrentPDPL2_'proc kernel_all_global_addresses.setCurrentPDPL2_body (Tree.Node setHardwareASID_'proc kernel_all_global_addresses.setHardwareASID_body Leaf Leaf) Leaf) (Tree.Node pte_get_pteSize_'proc kernel_all_global_addresses.pte_get_pteSize_body (Tree.Node pte_get_pteType_'proc kernel_all_substitute.pte_get_pteType_body Leaf Leaf) Leaf)))) (Tree.Node l1index_to_prio_'proc kernel_all_global_addresses.l1index_to_prio_body (Tree.Node pageBitsForSize_'proc kernel_all_substitute.pageBitsForSize_body (Tree.Node plat_cleanCache_'proc kernel_all_substitute.plat_cleanCache_body (Tree.Node postCapDeletion_'proc kernel_all_substitute.postCapDeletion_body (Tree.Node preemptionPoint_'proc kernel_all_substitute.preemptionPoint_body Leaf Leaf) Leaf) (Tree.Node pageTableMapped_'proc kernel_all_substitute.pageTableMapped_body (Tree.Node pde_get_pdeType_'proc kernel_all_global_addresses.pde_get_pdeType_body Leaf Leaf) Leaf)) (Tree.Node lookupIPCBuffer_'proc kernel_all_substitute.lookupIPCBuffer_body (Tree.Node lookupPivotSlot_'proc kernel_all_substitute.lookupPivotSlot_body (Tree.Node ntfn_set_active_'proc kernel_all_global_addresses.ntfn_set_active_body Leaf Leaf) Leaf) (Tree.Node loadCapTransfer_'proc kernel_all_substitute.loadCapTransfer_body (Tree.Node lookupExtraCaps_'proc kernel_all_substitute.lookupExtraCaps_body Leaf Leaf) Leaf))) (Tree.Node ensureEmptySlot_'proc kernel_all_substitute.ensureEmptySlot_body (Tree.Node init_core_state_'proc kernel_all_global_addresses.init_core_state_body (Tree.Node invokeCNodeMove_'proc kernel_all_global_addresses.invokeCNodeMove_body (Tree.Node it_alloc_paging_'proc kernel_all_substitute.it_alloc_paging_body Leaf Leaf) Leaf) (Tree.Node getReceiveSlots_'proc kernel_all_substitute.getReceiveSlots_body (Tree.Node handleInterrupt_'proc (kernel_all_substitute.handleInterrupt_body symbol_table) Leaf Leaf) Leaf)) (Tree.Node dist_enable_set_'proc kernel_all_substitute.dist_enable_set_body (Tree.Node doFaultTransfer_'proc kernel_all_substitute.doFaultTransfer_body (Tree.Node doReplyTransfer_'proc kernel_all_substitute.doReplyTransfer_body Leaf Leaf) Leaf) (Tree.Node deleteCallerCap_'proc kernel_all_substitute.deleteCallerCap_body (Tree.Node dist_enable_clr_'proc kernel_all_substitute.dist_enable_clr_body Leaf Leaf) Leaf))))) (Tree.Node deleteASIDPool_'proc kernel_all_substitute.deleteASIDPool_body (Tree.Node setKernelStack_'proc kernel_all_global_addresses.setKernelStack_body (Tree.Node wordFromRights_'proc kernel_all_global_addresses.wordFromRights_body (Tree.Node capCyclicZombie_'proc kernel_all_substitute.capCyclicZombie_body (Tree.Node cap_get_capType_'proc kernel_all_global_addresses.cap_get_capType_body (Tree.Node cleanCaches_PoU_'proc kernel_all_global_addresses.cleanCaches_PoU_body Leaf Leaf) Leaf) (Tree.Node writeContextID_'proc kernel_all_global_addresses.writeContextID_body (Tree.Node VGICMaintenance_'proc kernel_all_global_addresses.VGICMaintenance_body Leaf Leaf) Leaf)) (Tree.Node switchToThread_'proc kernel_all_global_addresses.switchToThread_body (Tree.Node tcbSchedAppend_'proc kernel_all_substitute.tcbSchedAppend_body (Tree.Node unmapPageTable_'proc kernel_all_substitute.unmapPageTable_body Leaf Leaf) Leaf) (Tree.Node setThreadState_'proc kernel_all_substitute.setThreadState_body (Tree.Node setupCallerCap_'proc kernel_all_substitute.setupCallerCap_body Leaf Leaf) Leaf))) (Tree.Node invalidateByVA_'proc kernel_all_global_addresses.invalidateByVA_body (Tree.Node performPDFlush_'proc kernel_all_substitute.performPDFlush_body (Tree.Node reserve_region_'proc kernel_all_substitute.reserve_region_body (Tree.Node rightsFromWord_'proc kernel_all_substitute.rightsFromWord_body Leaf Leaf) Leaf) (Tree.Node invert_l1index_'proc kernel_all_substitute.invert_l1index_body (Tree.Node isCapRevocable_'proc kernel_all_substitute.isCapRevocable_body Leaf Leaf) Leaf)) (Tree.Node getKernelStack_'proc kernel_all_substitute.getKernelStack_body (Tree.Node getProcessorID_'proc kernel_all_substitute.getProcessorID_body (Tree.Node invalidateASID_'proc kernel_all_substitute.invalidateASID_body Leaf Leaf) Leaf) (Tree.Node findFreeHWASID_'proc kernel_all_substitute.findFreeHWASID_body (Tree.Node getHighestPrio_'proc kernel_all_substitute.getHighestPrio_body Leaf Leaf) Leaf)))) (Tree.Node writeTPIDRURW_'proc kernel_all_global_addresses.writeTPIDRURW_body (Tree.Node cleanInvalByVA_'proc kernel_all_global_addresses.cleanInvalByVA_body (Tree.Node completeSignal_'proc kernel_all_substitute.completeSignal_body (Tree.Node cpu_iface_init_'proc kernel_all_substitute.cpu_iface_init_body (Tree.Node decodeSetSpace_'proc kernel_all_substitute.decodeSetSpace_body Leaf Leaf) Leaf) (Tree.Node clearExMonitor_'proc kernel_all_global_addresses.clearExMonitor_body (Tree.Node clearMemory_PT_'proc kernel_all_substitute.clearMemory_PT_body Leaf Leaf) Leaf)) (Tree.Node Arch_deriveCap_'proc kernel_all_substitute.Arch_deriveCap_body (Tree.Node activateThread_'proc kernel_all_substitute.activateThread_body (Tree.Node cap_get_capPtr_'proc kernel_all_substitute.cap_get_capPtr_body Leaf Leaf) Leaf) (Tree.Node writeTTBR0Ptr_'proc kernel_all_global_addresses.writeTTBR0Ptr_body (Tree.Node APFromVMRights_'proc kernel_all_substitute.APFromVMRights_body Leaf Leaf) Leaf))) (Tree.Node setExtraBadge_'proc kernel_all_substitute.setExtraBadge_body (Tree.Node updateCapData_'proc kernel_all_substitute.updateCapData_body (Tree.Node writeTPIDRPRW_'proc kernel_all_global_addresses.writeTPIDRPRW_body (Tree.Node writeTPIDRURO_'proc kernel_all_global_addresses.writeTPIDRURO_body Leaf Leaf) Leaf) (Tree.Node setIRQTrigger_'proc kernel_all_substitute.setIRQTrigger_body (Tree.Node setMCPriority_'proc kernel_all_substitute.setMCPriority_body Leaf Leaf) Leaf)) (Tree.Node merge_regions_'proc kernel_all_substitute.merge_regions_body (Tree.Node readCacheSize_'proc kernel_all_substitute.readCacheSize_body (Tree.Node receiveSignal_'proc kernel_all_substitute.receiveSignal_body Leaf Leaf) Leaf) (Tree.Node maskInterrupt_'proc kernel_all_global_addresses.maskInterrupt_body Leaf Leaf))))))) (Tree.Node flushTable_'proc kernel_all_substitute.flushTable_body (Tree.Node capRemovable_'proc kernel_all_substitute.capRemovable_body (Tree.Node readTPIDRURW_'proc kernel_all_substitute.readTPIDRURW_body (Tree.Node cleanByVA_PoU_'proc kernel_all_global_addresses.cleanByVA_PoU_body (Tree.Node handleSyscall_'proc kernel_all_substitute.handleSyscall_body (Tree.Node isHighestPrio_'proc kernel_all_substitute.isHighestPrio_body (Tree.Node isMDBParentOf_'proc kernel_all_substitute.isMDBParentOf_body (Tree.Node map_it_pt_cap_'proc kernel_all_substitute.map_it_pt_cap_body Leaf Leaf) Leaf) (Tree.Node handleVMFault_'proc kernel_all_substitute.handleVMFault_body (Tree.Node insert_region_'proc kernel_all_substitute.insert_region_body Leaf Leaf) Leaf)) (Tree.Node findPDForASID_'proc kernel_all_substitute.findPDForASID_body (Tree.Node getObjectSize_'proc kernel_all_substitute.getObjectSize_body (Tree.Node getSyscallArg_'proc kernel_all_substitute.getSyscallArg_body Leaf Leaf) Leaf) (Tree.Node doIPCTransfer_'proc kernel_all_substitute.doIPCTransfer_body (Tree.Node fastpath_call_'proc kernel_all_substitute.fastpath_call_body Leaf Leaf) Leaf))) (Tree.Node setCurrentPD_'proc kernel_all_global_addresses.setCurrentPD_body (Tree.Node transferCaps_'proc kernel_all_substitute.transferCaps_body (Tree.Node Arch_checkIRQ_'proc kernel_all_global_addresses.Arch_checkIRQ_body (Tree.Node addrFromKPPtr_'proc kernel_all_substitute.addrFromKPPtr_body Leaf Leaf) Leaf) (Tree.Node setMRs_fault_'proc kernel_all_substitute.setMRs_fault_body (Tree.Node tcbEPDequeue_'proc kernel_all_substitute.tcbEPDequeue_body Leaf Leaf) Leaf)) (Tree.Node sameObjectAs_'proc kernel_all_substitute.sameObjectAs_body (Tree.Node sameRegionAs_'proc kernel_all_substitute.sameRegionAs_body (Tree.Node sendFaultIPC_'proc kernel_all_substitute.sendFaultIPC_body Leaf Leaf) Leaf) (Tree.Node reduceZombie_'proc kernel_all_substitute.reduceZombie_body (Tree.Node resolveVAddr_'proc kernel_all_substitute.resolveVAddr_body Leaf Leaf) Leaf)))) (Tree.Node init_freemem_'proc kernel_all_substitute.init_freemem_body (Tree.Node lookupPTSlot_'proc kernel_all_substitute.lookupPTSlot_body (Tree.Node ptrFromPAddr_'proc kernel_all_substitute.ptrFromPAddr_body (Tree.Node readTPIDRPRW_'proc kernel_all_substitute.readTPIDRPRW_body (Tree.Node readTPIDRURO_'proc kernel_all_substitute.readTPIDRURO_body Leaf Leaf) Leaf) (Tree.Node maskVMRights_'proc kernel_all_substitute.maskVMRights_body (Tree.Node mdb_node_new_'proc kernel_all_substitute.mdb_node_new_body Leaf Leaf) Leaf)) (Tree.Node is_reg_empty_'proc kernel_all_global_addresses.is_reg_empty_body (Tree.Node lockTLBEntry_'proc kernel_all_global_addresses.lockTLBEntry_body (Tree.Node lookupPDSlot_'proc kernel_all_substitute.lookupPDSlot_body Leaf Leaf) Leaf) (Tree.Node insertNewCap_'proc kernel_all_substitute.insertNewCap_body (Tree.Node isIRQPending_'proc kernel_all_substitute.isIRQPending_body Leaf Leaf) Leaf))) (Tree.Node cteDeleteOne_'proc kernel_all_substitute.cteDeleteOne_body (Tree.Node getExtraCPtr_'proc kernel_all_substitute.getExtraCPtr_body (Tree.Node getRestartPC_'proc kernel_all_substitute.getRestartPC_body (Tree.Node get_n_paging_'proc kernel_all_global_addresses.get_n_paging_body Leaf Leaf) Leaf) (Tree.Node finaliseSlot_'proc kernel_all_substitute.finaliseSlot_body (Tree.Node getActiveIRQ_'proc kernel_all_substitute.getActiveIRQ_body Leaf Leaf) Leaf)) (Tree.Node clearEnFPEXC_'proc kernel_all_substitute.clearEnFPEXC_body (Tree.Node copyMRsFault_'proc kernel_all_substitute.copyMRsFault_body (Tree.Node createObject_'proc (kernel_all_substitute.createObject_body domain) Leaf Leaf) Leaf) (Tree.Node char_to_long_'proc kernel_all_global_addresses.char_to_long_body (Tree.Node chooseThread_'proc kernel_all_substitute.chooseThread_body Leaf Leaf) Leaf))))) (Tree.Node handleReply_'proc kernel_all_substitute.handleReply_body (Tree.Node setRegister_'proc kernel_all_substitute.setRegister_body (Tree.Node L2_cacheSync_'proc kernel_all_substitute.L2_cacheSync_body (Tree.Node c_entry_hook_'proc kernel_all_global_addresses.c_entry_hook_body (Tree.Node cancelAllIPC_'proc kernel_all_substitute.cancelAllIPC_body (Tree.Node cancelSignal_'proc kernel_all_substitute.cancelSignal_body Leaf Leaf) Leaf) (Tree.Node ackInterrupt_'proc kernel_all_substitute.ackInterrupt_body (Tree.Node addrFromPPtr_'proc kernel_all_substitute.addrFromPPtr_body Leaf Leaf) Leaf)) (Tree.Node tcbEPAppend_'proc kernel_all_substitute.tcbEPAppend_body (Tree.Node unmapIOPage_'proc kernel_all_global_addresses.unmapIOPage_body (Tree.Node writeHTPIDR_'proc kernel_all_global_addresses.writeHTPIDR_body Leaf Leaf) Leaf) (Tree.Node storeHWASID_'proc kernel_all_substitute.storeHWASID_body (Tree.Node str_to_long_'proc kernel_all_substitute.str_to_long_body Leaf Leaf) Leaf))) (Tree.Node makeUserPDE_'proc kernel_all_substitute.makeUserPDE_body (Tree.Node scheduleTCB_'proc kernel_all_substitute.scheduleTCB_body (Tree.Node setIRQState_'proc kernel_all_global_addresses.setIRQState_body (Tree.Node setPriority_'proc kernel_all_substitute.setPriority_body Leaf Leaf) Leaf) (Tree.Node makeUserPTE_'proc kernel_all_substitute.makeUserPTE_body (Tree.Node provide_cap_'proc kernel_all_substitute.provide_cap_body Leaf Leaf) Leaf)) (Tree.Node initL2Cache_'proc kernel_all_substitute.initL2Cache_body (Tree.Node init_kernel_'proc kernel_all_substitute.init_kernel_body (Tree.Node isIRQActive_'proc kernel_all_global_addresses.isIRQActive_body Leaf Leaf) Leaf) (Tree.Node handleYield_'proc kernel_all_global_addresses.handleYield_body (Tree.Node idle_thread_'proc kernel_all_global_addresses.idle_thread_body Leaf Leaf) Leaf)))) (Tree.Node writeTTBR0_'proc kernel_all_global_addresses.writeTTBR0_body (Tree.Node c_exit_hook_'proc kernel_all_global_addresses.c_exit_hook_body (Tree.Node finaliseCap_'proc kernel_all_substitute.finaliseCap_body (Tree.Node getRegister_'proc kernel_all_substitute.getRegister_body (Tree.Node handleFault_'proc kernel_all_substitute.handleFault_body Leaf Leaf) Leaf) (Tree.Node clean_D_PoU_'proc kernel_all_substitute.clean_D_PoU_body (Tree.Node clearMemory_'proc kernel_all_substitute.clearMemory_body Leaf Leaf) Leaf)) (Tree.Node addToBitmap_'proc kernel_all_substitute.addToBitmap_body (Tree.Node bi_finalise_'proc kernel_all_substitute.bi_finalise_body (Tree.Node branchFlush_'proc kernel_all_global_addresses.branchFlush_body Leaf Leaf) Leaf) (Tree.Node writeTTBR1_'proc kernel_all_global_addresses.writeTTBR1_body (Tree.Node write_slot_'proc kernel_all_substitute.write_slot_body Leaf Leaf) Leaf))) (Tree.Node nextDomain_'proc kernel_all_substitute.nextDomain_body (Tree.Node resetTimer_'proc kernel_all_substitute.resetTimer_body (Tree.Node sendSignal_'proc kernel_all_substitute.sendSignal_body (Tree.Node writeTTBCR_'proc kernel_all_global_addresses.writeTTBCR_body Leaf Leaf) Leaf) (Tree.Node readHTPIDR_'proc kernel_all_global_addresses.readHTPIDR_body (Tree.Node receiveIPC_'proc kernel_all_substitute.receiveIPC_body Leaf Leaf) Leaf)) (Tree.Node isRunnable_'proc kernel_all_substitute.isRunnable_body (Tree.Node loadHWASID_'proc kernel_all_substitute.loadHWASID_body (Tree.Node lookupSlot_'proc kernel_all_substitute.lookupSlot_body Leaf Leaf) Leaf) (Tree.Node handleRecv_'proc kernel_all_substitute.handleRecv_body Leaf Leaf)))))) (Tree.Node getAIFSR_'proc kernel_all_substitute.getAIFSR_body (Tree.Node initTimer_'proc kernel_all_substitute.initTimer_body (Tree.Node setDomain_'proc kernel_all_substitute.setDomain_body (Tree.Node Zombie_new_'proc kernel_all_substitute.Zombie_new_body (Tree.Node deleteASID_'proc kernel_all_substitute.deleteASID_body (Tree.Node disableFpu_'proc kernel_all_global_addresses.disableFpu_body (Tree.Node flushSpace_'proc kernel_all_substitute.flushSpace_body Leaf Leaf) Leaf) (Tree.Node arm_errata_'proc kernel_all_global_addresses.arm_errata_body (Tree.Node cleanByWSL_'proc kernel_all_global_addresses.cleanByWSL_body Leaf Leaf) Leaf)) (Tree.Node timerTick_'proc kernel_all_substitute.timerTick_body (Tree.Node unmapPage_'proc kernel_all_substitute.unmapPage_body (Tree.Node writeDACR_'proc kernel_all_global_addresses.writeDACR_body Leaf Leaf) Leaf) (Tree.Node setNextPC_'proc kernel_all_global_addresses.setNextPC_body (Tree.Node setVMRoot_'proc (kernel_all_substitute.setVMRoot_body symbol_table) Leaf Leaf) Leaf))) (Tree.Node lookupCap_'proc kernel_all_substitute.lookupCap_body (Tree.Node readTTBCR_'proc kernel_all_substitute.readTTBCR_body (Tree.Node readTTBR0_'proc kernel_all_substitute.readTTBR0_body (Tree.Node readTTBR1_'proc kernel_all_substitute.readTTBR1_body Leaf Leaf) Leaf) (Tree.Node lookup_fp_'proc kernel_all_substitute.lookup_fp_body (Tree.Node readMPIDR_'proc kernel_all_substitute.readMPIDR_body Leaf Leaf) Leaf)) (Tree.Node isArchCap_'proc kernel_all_substitute.isArchCap_body (Tree.Node isBlocked_'proc kernel_all_substitute.isBlocked_body (Tree.Node isStopped_'proc kernel_all_substitute.isStopped_body Leaf Leaf) Leaf) (Tree.Node init_irqs_'proc kernel_all_substitute.init_irqs_body (Tree.Node init_plat_'proc kernel_all_global_addresses.init_plat_body Leaf Leaf) Leaf)))) (Tree.Node checkPrio_'proc kernel_all_substitute.checkPrio_body (Tree.Node dist_init_'proc kernel_all_substitute.dist_init_body (Tree.Node flushBTAC_'proc kernel_all_global_addresses.flushBTAC_body (Tree.Node flushPage_'proc kernel_all_substitute.flushPage_body (Tree.Node getHWASID_'proc kernel_all_substitute.getHWASID_body Leaf Leaf) Leaf) (Tree.Node dsb_ishst_'proc kernel_all_global_addresses.dsb_ishst_body (Tree.Node emptySlot_'proc kernel_all_substitute.emptySlot_body Leaf Leaf) Leaf)) (Tree.Node cteInsert_'proc kernel_all_substitute.cteInsert_body (Tree.Node cteRevoke_'proc kernel_all_substitute.cteRevoke_body (Tree.Node deriveCap_'proc kernel_all_substitute.deriveCap_body Leaf Leaf) Leaf) (Tree.Node cleanByVA_'proc kernel_all_global_addresses.cleanByVA_body (Tree.Node cteDelete_'proc kernel_all_substitute.cteDelete_body Leaf Leaf) Leaf))) (Tree.Node schedule_'proc kernel_all_substitute.schedule_body (Tree.Node setAIFSR_'proc kernel_all_global_addresses.setAIFSR_body (Tree.Node slowpath_'proc kernel_all_global_addresses.slowpath_body (Tree.Node cancelIPC_'proc kernel_all_substitute.cancelIPC_body Leaf Leaf) Leaf) (Tree.Node setACTLR_'proc kernel_all_global_addresses.setACTLR_body (Tree.Node setADFSR_'proc kernel_all_global_addresses.setADFSR_body Leaf Leaf) Leaf)) (Tree.Node physBase_'proc kernel_all_global_addresses.physBase_body (Tree.Node readCLID_'proc kernel_all_substitute.readCLID_body (Tree.Node readDACR_'proc kernel_all_substitute.readDACR_body Leaf Leaf) Leaf) (Tree.Node init_cpu_'proc (kernel_all_substitute.init_cpu_body symbol_table) (Tree.Node pageBase_'proc kernel_all_substitute.pageBase_body Leaf Leaf) Leaf))))) (Tree.Node getCIDR_'proc kernel_all_substitute.getCIDR_body (Tree.Node setDFSR_'proc kernel_all_global_addresses.setDFSR_body (Tree.Node strlcpy_'proc kernel_all_substitute.strlcpy_body (Tree.Node suspend_'proc kernel_all_substitute.suspend_body (Tree.Node getACTLR_'proc kernel_all_substitute.getACTLR_body (Tree.Node getADFSR_'proc kernel_all_substitute.getADFSR_body Leaf Leaf) Leaf) (Tree.Node strncmp_'proc kernel_all_substitute.strncmp_body (Tree.Node strnlen_'proc kernel_all_substitute.strnlen_body Leaf Leaf) Leaf)) (Tree.Node setNMRR_'proc kernel_all_global_addresses.setNMRR_body (Tree.Node setPRRR_'proc kernel_all_global_addresses.setPRRR_body (Tree.Node strlcat_'proc kernel_all_substitute.strlcat_body Leaf Leaf) Leaf) (Tree.Node setIFAR_'proc kernel_all_global_addresses.setIFAR_body (Tree.Node setIFSR_'proc kernel_all_global_addresses.setIFSR_body Leaf Leaf) Leaf))) (Tree.Node getPRRR_'proc kernel_all_substitute.getPRRR_body (Tree.Node sendIPC_'proc kernel_all_substitute.sendIPC_body (Tree.Node setCIDR_'proc kernel_all_global_addresses.setCIDR_body (Tree.Node setDFAR_'proc kernel_all_global_addresses.setDFAR_body Leaf Leaf) Leaf) (Tree.Node memzero_'proc kernel_all_substitute.memzero_body (Tree.Node restart_'proc kernel_all_substitute.restart_body Leaf Leaf) Leaf)) (Tree.Node getIFAR_'proc kernel_all_substitute.getIFAR_body (Tree.Node getIFSR_'proc kernel_all_substitute.getIFSR_body (Tree.Node getNMRR_'proc kernel_all_substitute.getNMRR_body Leaf Leaf) Leaf) (Tree.Node getDFAR_'proc kernel_all_substitute.getDFAR_body (Tree.Node getDFSR_'proc kernel_all_substitute.getDFSR_body Leaf Leaf) Leaf)))) (Tree.Node ctz32_'proc kernel_all_substitute.ctz32_body (Tree.Node memset_'proc kernel_all_substitute.memset_body (Tree.Node cteMove_'proc kernel_all_substitute.cteMove_body (Tree.Node cteSwap_'proc kernel_all_substitute.cteSwap_body (Tree.Node doFlush_'proc kernel_all_substitute.doFlush_body Leaf Leaf) Leaf) (Tree.Node alignUp_'proc kernel_all_global_addresses.alignUp_body (Tree.Node copyMRs_'proc kernel_all_substitute.copyMRs_body Leaf Leaf) Leaf)) (Tree.Node setMR_'proc kernel_all_substitute.setMR_body (Tree.Node getFAR_'proc kernel_all_substitute.getFAR_body (Tree.Node memcpy_'proc kernel_all_substitute.memcpy_body Leaf Leaf) Leaf) (Tree.Node ctz64_'proc kernel_all_substitute.ctz64_body (Tree.Node ctzll_'proc kernel_all_global_addresses.ctzll_body Leaf Leaf) Leaf))) (Tree.Node clzl_'proc kernel_all_global_addresses.clzl_body (Tree.Node clz32_'proc kernel_all_substitute.clz32_body (Tree.Node clz64_'proc kernel_all_substitute.clz64_body (Tree.Node clzll_'proc kernel_all_global_addresses.clzll_body Leaf Leaf) Leaf) (Tree.Node ctzl_'proc kernel_all_global_addresses.ctzl_body (Tree.Node halt_'proc kernel_all_global_addresses.halt_body Leaf Leaf) Leaf)) (Tree.Node dsb_'proc kernel_all_global_addresses.dsb_body (Tree.Node isb_'proc kernel_all_global_addresses.isb_body (Tree.Node wfi_'proc kernel_all_global_addresses.wfi_body Leaf Leaf) Leaf) (Tree.Node dmb_'proc kernel_all_global_addresses.dmb_body Leaf Leaf))))))))) id) proof (prove)
goal (759 subgoals):
 1. exec_statefn_simulates id UNIV UNIV (kernel_all_global_addresses.map_kernel_devices_body symbol_table) (kernel_all_substitute.map_kernel_devices_body symbol_table)
 2. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.thread_state_ptr_set_tsType_body kernel_all_substitute.thread_state_ptr_set_tsType_body
 3. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.seL4_Fault_UserException_get_code_body kernel_all_substitute.seL4_Fault_UserException_get_code_body
 4. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.pde_pde_invalid_get_stored_asid_valid_body kernel_all_substitute.pde_pde_invalid_get_stored_asid_valid_body
 5. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.thread_state_ptr_set_blockingIPCCanGrant_body kernel_all_substitute.thread_state_ptr_set_blockingIPCCanGrant_body
 6. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.cap_small_frame_cap_get_capFMappedASIDHigh_body kernel_all_substitute.cap_small_frame_cap_get_capFMappedASIDHigh_body
 7. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.cap_page_directory_cap_ptr_set_capPDIsMapped_body kernel_all_substitute.cap_page_directory_cap_ptr_set_capPDIsMapped_body
 8. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.thread_state_ptr_set_blockingIPCCanGrantReply_body kernel_all_substitute.thread_state_ptr_set_blockingIPCCanGrantReply_body
 9. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.cap_page_directory_cap_ptr_set_capPDMappedASID_body kernel_all_substitute.cap_page_directory_cap_ptr_set_capPDMappedASID_body
 10. exec_statefn_simulates id UNIV UNIV kernel_all_global_addresses.mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_body kernel_all_substitute.mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_body
A total of 759 subgoals... proof (prove)
goal (263 subgoals):
 1. exec_statefn_simulates id UNIV UNIV (TRY
  \<acute>i___int :== 0;;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> (WHILE SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C))) DO
  Guard ArrayBounds \<lbrace>\<acute>i___int <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s \<acute>i___int\<rbrace> (Guard C_Guard \<lbrace>c_guard (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))\<rbrace> (\<acute>frame___ptr_to_struct_kernel_frame_C :== PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')) +\<^sub>p sint \<acute>i___int)));;
SKIP;;
Guard C_Guard \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (\<acute>ret__struct_vm_attributes_C :== CALL vm_attributes_new_'proc(SCAST(32 signed \<rightarrow> 32) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''armExecuteNever_C'']))),SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false));;
Guard C_Guard \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL map_kernel_frame_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])),h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''pptr_C''])),SCAST(32 signed \<rightarrow> 32) VMKernelOnly,\<acute>ret__struct_vm_attributes_C)));;
Guard C_Guard \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (IF h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0xC\<rbrace> (Guard ShiftError \<lbrace>0xC <s 0x20\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL reserve_region_'proc(p_region_C.end_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])) + (1 << unat 0xC)) (p_region_C.start_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C'']))) (p_region_C 0 0)))))))
FI);;
Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint \<acute>i___int + sint 1 \<and> sint \<acute>i___int + sint 1 \<le> 2147483647\<rbrace> (\<acute>i___int :== \<acute>i___int + 1);;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> SKIP
OD)
CATCH SKIP
END) (TRY
  \<acute>i___int :== 0;;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> (WHILE SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C))) DO
  Guard ArrayBounds \<lbrace>\<acute>i___int <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s \<acute>i___int\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace> (Guard MemorySafety \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>frame___ptr_to_struct_kernel_frame_C :== PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')) +\<^sub>p sint \<acute>i___int))));;
SKIP;;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (\<acute>ret__struct_vm_attributes_C :== CALL vm_attributes_new_'proc(SCAST(32 signed \<rightarrow> 32) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''armExecuteNever_C'']))),SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL map_kernel_frame_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])),h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''pptr_C''])),SCAST(32 signed \<rightarrow> 32) VMKernelOnly,\<acute>ret__struct_vm_attributes_C)));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (IF h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0xC\<rbrace> (Guard ShiftError \<lbrace>0xC <s 0x20\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL reserve_region_'proc(p_region_C.end_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])) + (1 << unat 0xC)) (p_region_C.start_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C'']))) (p_region_C 0 0)))))))
FI);;
Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint \<acute>i___int + sint 1 \<and> sint \<acute>i___int + sint 1 \<le> 2147483647\<rbrace> (\<acute>i___int :== \<acute>i___int + 1);;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> SKIP
OD)
CATCH SKIP
END)
 2. exec_statefn_simulates id UNIV UNIV (TRY
  SKIP;;
Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xF))))))))));;
Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 0] || (\<acute>v32 << unat 0) && SCAST(32 signed \<rightarrow> 32) 0xF))))))))))))
CATCH SKIP
END) (TRY
  SKIP;;
Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xF))))))))));;
Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 0] || (\<acute>v32 << unat 0) && SCAST(32 signed \<rightarrow> 32) 0xF))))))))))))
CATCH SKIP
END)
 3. exec_statefn_simulates id UNIV UNIV (TRY
  SKIP;;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] && ~~ 8))))))))));;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 3\<rbrace> (Guard ShiftError \<lbrace>3 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] || (\<acute>v32 << unat 3) && SCAST(32 signed \<rightarrow> 32) 8))))))))))))
CATCH SKIP
END) (TRY
  SKIP;;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] && ~~ 8))))))))));;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 3\<rbrace> (Guard ShiftError \<lbrace>3 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] || (\<acute>v32 << unat 3) && SCAST(32 signed \<rightarrow> 32) 8))))))))))))
CATCH SKIP
END)
 4. exec_statefn_simulates id UNIV UNIV (TRY
  SKIP;;
SKIP;;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 0] && ~~ 0x10))))))))));;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 4\<rbrace> (Guard ShiftError \<lbrace>4 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 0] || (\<acute>v32 << unat 4) && 0x10))))))))))))
CATCH SKIP
END) (TRY
  SKIP;;
SKIP;;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 0] && ~~ 0x10))))))))));;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 4\<rbrace> (Guard ShiftError \<lbrace>4 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 0] || (\<acute>v32 << unat 4) && 0x10))))))))))))
CATCH SKIP
END)
 5. exec_statefn_simulates id UNIV UNIV (TRY
  SKIP;;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] && ~~ 4))))))))));;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 2\<rbrace> (Guard ShiftError \<lbrace>2 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] || (\<acute>v32 << unat 2) && SCAST(32 signed \<rightarrow> 32) 4))))))))))))
CATCH SKIP
END) (TRY
  SKIP;;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] && ~~ 4))))))))));;
Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 2\<rbrace> (Guard ShiftError \<lbrace>2 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C'']))) (unat 2) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] || (\<acute>v32 << unat 2) && SCAST(32 signed \<rightarrow> 32) 4))))))))))))
CATCH SKIP
END)
 6. exec_statefn_simulates id UNIV UNIV (TRY
  SKIP;;
SKIP;;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 1] && ~~ 0x1FFFF))))))))));;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 1] || (\<acute>v32 << unat 0) && 0x1FFFF))))))))))))
CATCH SKIP
END) (TRY
  SKIP;;
SKIP;;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 1] && ~~ 0x1FFFF))))))))));;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>cap_ptr\<rightarrow>[''words_C''])).[unat 1] || (\<acute>v32 << unat 0) && 0x1FFFF))))))))))))
CATCH SKIP
END)
 7. exec_statefn_simulates id UNIV UNIV (TRY
  Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>node_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 1\<rbrace> (Guard ShiftError \<lbrace>1 <s 0x20\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>node_ptr\<rightarrow>[''words_C'']))) (unat 1) (UCAST(32 \<rightarrow> 32) ((\<acute>mdbNext___unsigned_long || (\<acute>mdbRevocable___unsigned_long << unat 1)) || \<acute>mdbFirstBadged___unsigned_long))))))))))
CATCH SKIP
END) (TRY
  Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>node_ptr\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 1\<rbrace> (Guard ShiftError \<lbrace>1 <s 0x20\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>node_ptr\<rightarrow>[''words_C'']))) (unat 1) (UCAST(32 \<rightarrow> 32) ((\<acute>mdbNext___unsigned_long || (\<acute>mdbRevocable___unsigned_long << unat 1)) || \<acute>mdbFirstBadged___unsigned_long))))))))))
CATCH SKIP
END)
 8. exec_statefn_simulates id UNIV UNIV (TRY
  lvar_nondet_init ret_' ret_'_update;;
Guard ShiftError \<lbrace>0 \<le>s 2\<rbrace> (Guard ShiftError \<lbrace>2 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>thread_state_ptr\<rbrace> (\<acute>ret :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] && 4 >> unat 2)))));;
\<acute>ret__int :== 0;;
IF \<acute>ret__int \<noteq> 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0x1F\<rbrace> (Guard ShiftError \<lbrace>0x1F <s 0x20\<rbrace> (\<acute>ret__int :== (if \<acute>ret && (1 << unat 0x1F) \<noteq> 0 then 1 else 0)))
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret :== \<acute>ret || SCAST(32 signed \<rightarrow> 32) 0
FI;;
creturn global_exn_var_'_update ret__unsigned_'_update ret_';;
Guard DontReach {} SKIP
CATCH SKIP
END) (TRY
  lvar_nondet_init ret_' ret_'_update;;
Guard ShiftError \<lbrace>0 \<le>s 2\<rbrace> (Guard ShiftError \<lbrace>2 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>2 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 2\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread_state_ptr\<rbrace> (\<acute>ret :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>thread_state_ptr\<rightarrow>[''words_C''])).[unat 2] && 4 >> unat 2)))));;
\<acute>ret__int :== 0;;
IF \<acute>ret__int \<noteq> 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0x1F\<rbrace> (Guard ShiftError \<lbrace>0x1F <s 0x20\<rbrace> (\<acute>ret__int :== (if \<acute>ret && (1 << unat 0x1F) \<noteq> 0 then 1 else 0)))
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret :== \<acute>ret || SCAST(32 signed \<rightarrow> 32) 0
FI;;
creturn global_exn_var_'_update ret__unsigned_'_update ret_';;
Guard DontReach {} SKIP
CATCH SKIP
END)
 9. exec_statefn_simulates id UNIV UNIV (TRY
  Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (\<acute>ret__struct_cap_C :== CALL generic_frame_cap_set_capFMappedAddress_'proc(h_val (hrs_mem \<acute>t_hrs) \<acute>cap_ptr,\<acute>asid,\<acute>addr));;
Guard C_Guard \<lbrace>c_guard \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>cap_ptr \<acute>ret__struct_cap_C)))
CATCH SKIP
END) (TRY
  Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (\<acute>ret__struct_cap_C :== CALL generic_frame_cap_set_capFMappedAddress_'proc(h_val (hrs_mem \<acute>t_hrs) \<acute>cap_ptr,\<acute>asid,\<acute>addr));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>cap_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>cap_ptr \<acute>ret__struct_cap_C)))
CATCH SKIP
END)
 10. exec_statefn_simulates id UNIV UNIV (TRY
  Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>c_guard \<acute>ts_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>ts_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>ts_ptr\<rightarrow>[''words_C'']))) (unat 0) (UCAST(32 \<rightarrow> 32) (\<acute>ep_ref || \<acute>tsType))))))))
CATCH SKIP
END) (TRY
  Guard ArrayBounds \<lbrace>0 <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>ts_ptr\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[3]) &(\<acute>ts_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[3]) &(\<acute>ts_ptr\<rightarrow>[''words_C'']))) (unat 0) (UCAST(32 \<rightarrow> 32) (\<acute>ep_ref || \<acute>tsType))))))))
CATCH SKIP
END)
A total of 263 subgoals... proof (prove)
goal (1888 subgoals):
 1. UNIV \<inter> {s. id s \<in> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>} \<subseteq> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>
 2. bij id
 3. \<And>s. \<lbrakk>s \<in> UNIV \<inter> {s. id s \<in> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>} \<or> id s \<in> com_final_guards UNIV (Guard ArrayBounds \<lbrace>\<acute>i___int <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s \<acute>i___int\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace> (Guard MemorySafety \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>frame___ptr_to_struct_kernel_frame_C :== PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')) +\<^sub>p sint \<acute>i___int))));;
SKIP;;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (\<acute>ret__struct_vm_attributes_C :== CALL vm_attributes_new_'proc(SCAST(32 signed \<rightarrow> 32) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''armExecuteNever_C'']))),SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL map_kernel_frame_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])),h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''pptr_C''])),SCAST(32 signed \<rightarrow> 32) VMKernelOnly,\<acute>ret__struct_vm_attributes_C)));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (IF h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0xC\<rbrace> (Guard ShiftError \<lbrace>0xC <s 0x20\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL reserve_region_'proc(p_region_C.end_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])) + (1 << unat 0xC)) (p_region_C.start_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C'']))) (p_region_C 0 0)))))))
FI);;
Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint \<acute>i___int + sint 1 \<and> sint \<acute>i___int + sint 1 \<le> 2147483647\<rbrace> (\<acute>i___int :== \<acute>i___int + 1);;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> SKIP); id s \<in> com_initial_guards (Guard ArrayBounds \<lbrace>\<acute>i___int <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s \<acute>i___int\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace> (Guard MemorySafety \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>frame___ptr_to_struct_kernel_frame_C :== PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')) +\<^sub>p sint \<acute>i___int))));;
SKIP;;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (\<acute>ret__struct_vm_attributes_C :== CALL vm_attributes_new_'proc(SCAST(32 signed \<rightarrow> 32) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''armExecuteNever_C'']))),SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL map_kernel_frame_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])),h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''pptr_C''])),SCAST(32 signed \<rightarrow> 32) VMKernelOnly,\<acute>ret__struct_vm_attributes_C)));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (IF h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0xC\<rbrace> (Guard ShiftError \<lbrace>0xC <s 0x20\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL reserve_region_'proc(p_region_C.end_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])) + (1 << unat 0xC)) (p_region_C.start_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C'']))) (p_region_C 0 0)))))))
FI);;
Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint \<acute>i___int + sint 1 \<and> sint \<acute>i___int + sint 1 \<le> 2147483647\<rbrace> (\<acute>i___int :== \<acute>i___int + 1);;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> SKIP) \<or> s \<in> UNIV\<rbrakk> \<Longrightarrow> (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace>) = (id s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace>)
 4. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. id s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. id s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. id s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>\<acute>i___int <s 3\<rbrace>
 5. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. id s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. id s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. id s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>
 6. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. id s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. id s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. id s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>c_guard (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))\<rbrace>
 7. UNIV \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 8. UNIV \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 9. UNIV \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 10. UNIV \<inter> {s. id s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
A total of 1888 subgoals... proof (prove)
goal (1888 subgoals):
 1. UNIV \<inter> {s. s \<in> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>} \<subseteq> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>
 2. bij (\<lambda>x. x)
 3. \<And>s. \<lbrakk>s \<in> UNIV \<inter> {s. s \<in> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>} \<or> s \<in> com_final_guards UNIV (Guard ArrayBounds \<lbrace>\<acute>i___int <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s \<acute>i___int\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace> (Guard MemorySafety \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>frame___ptr_to_struct_kernel_frame_C :== PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')) +\<^sub>p sint \<acute>i___int))));;
SKIP;;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (\<acute>ret__struct_vm_attributes_C :== CALL vm_attributes_new_'proc(SCAST(32 signed \<rightarrow> 32) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''armExecuteNever_C'']))),SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL map_kernel_frame_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])),h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''pptr_C''])),SCAST(32 signed \<rightarrow> 32) VMKernelOnly,\<acute>ret__struct_vm_attributes_C)));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (IF h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0xC\<rbrace> (Guard ShiftError \<lbrace>0xC <s 0x20\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL reserve_region_'proc(p_region_C.end_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])) + (1 << unat 0xC)) (p_region_C.start_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C'']))) (p_region_C 0 0)))))))
FI);;
Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint \<acute>i___int + sint 1 \<and> sint \<acute>i___int + sint 1 \<le> 2147483647\<rbrace> (\<acute>i___int :== \<acute>i___int + 1);;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> SKIP); s \<in> com_initial_guards (Guard ArrayBounds \<lbrace>\<acute>i___int <s 3\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s \<acute>i___int\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace> (Guard MemorySafety \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>frame___ptr_to_struct_kernel_frame_C :== PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')) +\<^sub>p sint \<acute>i___int))));;
SKIP;;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (\<acute>ret__struct_vm_attributes_C :== CALL vm_attributes_new_'proc(SCAST(32 signed \<rightarrow> 32) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''armExecuteNever_C'']))),SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL map_kernel_frame_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])),h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''pptr_C''])),SCAST(32 signed \<rightarrow> 32) VMKernelOnly,\<acute>ret__struct_vm_attributes_C)));;
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (IF h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0xC\<rbrace> (Guard ShiftError \<lbrace>0xC <s 0x20\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace> (CALL reserve_region_'proc(p_region_C.end_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C''])) + (1 << unat 0xC)) (p_region_C.start_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''paddr_C'']))) (p_region_C 0 0)))))))
FI);;
Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint \<acute>i___int + sint 1 \<and> sint \<acute>i___int + sint 1 \<le> 2147483647\<rbrace> (\<acute>i___int :== \<acute>i___int + 1);;
Guard Div_0 \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace> SKIP) \<or> s \<in> UNIV\<rbrakk> \<Longrightarrow> (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace>) = (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace>)
 4. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>\<acute>i___int <s 3\<rbrace>
 5. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>
 6. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>c_guard (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))\<rbrace>
 7. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 8. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 9. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 10. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
A total of 1888 subgoals... proof (prove)
goal (1511 subgoals):
 1. UNIV \<inter> {s. s \<in> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>} \<subseteq> \<lbrace>word_of_int (int (size_of TYPE(kernel_frame_C))) \<noteq> 0\<rbrace>
 2. bij (\<lambda>x. x)
 3. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>\<acute>i___int <s 3\<rbrace>
 4. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>
 5. \<lbrace>SCAST(32 signed \<rightarrow> 32) \<acute>i___int < word_of_int (int (size_of TYPE(kernel_frame_C[3]))) div word_of_int (int (size_of TYPE(kernel_frame_C)))\<rbrace> \<inter> {s. s \<in> \<lbrace>\<acute>i___int <s 3\<rbrace>} \<inter> {s. s \<in> \<lbrace>0 \<le>s \<acute>i___int\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames'')\<rbrace>} \<inter> {s. s \<in> \<lbrace>ptr_add_assertion' (PTR_COERCE(kernel_frame_C[3] \<rightarrow> kernel_frame_C) (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))) (sint \<acute>i___int) False (hrs_htd \<acute>t_hrs)\<rbrace>} \<subseteq> \<lbrace>c_guard (PTR(kernel_frame_C[3]) (symbol_table ''kernel_device_frames''))\<rbrace>
 6. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 7. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 8. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 9. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>c_guard \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>
 10. UNIV \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(32 signed word) &(\<acute>frame___ptr_to_struct_kernel_frame_C\<rightarrow>[''userAvailable_C''])) = 0\<rbrace> \<inter> {s. s \<in> \<lbrace>0 \<le>s 0xC\<rbrace>} \<inter> {s. s \<in> \<lbrace>0xC <s 0x20\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<inter> {s. s \<in> \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>frame___ptr_to_struct_kernel_frame_C\<rbrace>} \<subseteq> \<lbrace>0 \<le>s 0xC\<rbrace>
A total of 1511 subgoals... proof (prove)
goal (59 subgoals):
 1. bij (\<lambda>x. x)
 2. bij (\<lambda>x. x)
 3. bij (\<lambda>x. x)
 4. bij (\<lambda>x. x)
 5. bij (\<lambda>x. x)
 6. bij (\<lambda>x. x)
 7. bij (\<lambda>x. x)
 8. bij (\<lambda>x. x)
 9. bij (\<lambda>x. x)
 10. bij (\<lambda>x. x)
A total of 59 subgoals... proof (prove)
goal (59 subgoals):
 1. bij (\<lambda>x. x)
 2. bij (\<lambda>x. x)
 3. bij (\<lambda>x. x)
 4. bij (\<lambda>x. x)
 5. bij (\<lambda>x. x)
 6. bij (\<lambda>x. x)
 7. bij (\<lambda>x. x)
 8. bij (\<lambda>x. x)
 9. bij (\<lambda>x. x)
 10. bij (\<lambda>x. x)
A total of 59 subgoals... proof (prove)
goal:
No subgoals!