1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #pragma once
8 
9 #include <object/structures.h>
10 #include <types.h>
11 
12 word_t setMRs_fault(tcb_t *sender, tcb_t *receiver, word_t *receiveIPCBuffer);
13 word_t Arch_setMRs_fault(tcb_t *sender, tcb_t *receiver, word_t *receiveIPCBuffer, word_t faultType);
14 
15 bool_t handleFaultReply(tcb_t *receiver, tcb_t *sender);
16 bool_t Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType);
17 
18