1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 */
10
11#ifndef __OBJECT_ENDPOINT_H
12#define __OBJECT_ENDPOINT_H
13
14#include <types.h>
15#include <object/structures.h>
16
17static inline tcb_queue_t PURE
18ep_ptr_get_queue(endpoint_t *epptr)
19{
20    tcb_queue_t queue;
21
22    queue.head = (tcb_t*)endpoint_ptr_get_epQueue_head(epptr);
23    queue.end = (tcb_t*)endpoint_ptr_get_epQueue_tail(epptr);
24
25    return queue;
26}
27
28void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
29             bool_t canGrant, bool_t canDonate, tcb_t *thread, endpoint_t *epptr);
30void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking, cap_t replyCPtr);
31void cancelIPC(tcb_t *tptr);
32void cancelAllIPC(endpoint_t *epptr);
33void cancelBadgedSends(endpoint_t *epptr, word_t badge);
34void replyFromKernel_error(tcb_t *thread);
35void replyFromKernel_success_empty(tcb_t *thread);
36void reorderEP(endpoint_t *epptr, tcb_t *thread);
37#endif
38