Searched refs:msgInfo (Results 1 - 25 of 26) sorted by relevance

12

/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Dbugzilla213.c15 fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
18 register word_t r1 asm ("r1") = msgInfo;
H A Dvolatile_asm.c15 fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
18 register word_t r1 asm ("r1") = msgInfo;
/seL4-l4v-master/seL4/libsel4/include/sel4/
H A Dsyscalls_master.h24 * @param[in] msgInfo The messageinfo structure for the IPC.
27 seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
62 * @param[in] msgInfo The messageinfo structure for the IPC.
70 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
81 * @param[in] msgInfo The messageinfo structure for the IPC.
84 seL4_Reply(seL4_MessageInfo_t msgInfo);
95 * @param[in] msgInfo The messageinfo structure for the IPC.
98 seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
109 * @param[in] msgInfo The messageinfo structure for the IPC.
123 seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Wor
[all...]
H A Dsyscalls_mcs.h24 * @param[in] msgInfo The messageinfo structure for the IPC.
27 seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
63 * @param[in] msgInfo The messageinfo structure for the IPC.
71 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
83 * @param[in] msgInfo The messageinfo structure for the IPC.
86 seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
98 * @param[in] msgInfo The messageinfo structure for the IPC.
114 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply);
152 * @param[in] msgInfo The messageinfo structure for the IPC.
168 seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPt
[all...]
/seL4-l4v-master/seL4/include/arch/arm/arch/kernel/
H A Dtraps.h25 void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
29 void c_handle_fastpath_call(word_t cptr, word_t msgInfo)
33 void c_handle_fastpath_reply_recv(word_t cptr, word_t msgInfo, word_t reply)
35 void c_handle_fastpath_reply_recv(word_t cptr, word_t msgInfo)
/seL4-l4v-master/seL4/src/arch/arm/
H A Dc_traps.c126 void VISIBLE c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall) argument
132 benchmark_debug_syscall_start(cptr, msgInfo, syscall);
142 void VISIBLE c_handle_fastpath_call(word_t cptr, word_t msgInfo)
148 benchmark_debug_syscall_start(cptr, msgInfo, SysCall);
152 fastpath_call(cptr, msgInfo);
158 void VISIBLE c_handle_fastpath_reply_recv(word_t cptr, word_t msgInfo, word_t reply)
160 void VISIBLE c_handle_fastpath_reply_recv(word_t cptr, word_t msgInfo)
167 benchmark_debug_syscall_start(cptr, msgInfo, SysReplyRecv);
172 fastpath_reply_recv(cptr, msgInfo, reply);
174 fastpath_reply_recv(cptr, msgInfo);
[all...]
/seL4-l4v-master/seL4/libsel4/arch_include/arm/sel4/arch/
H A Dsyscalls.h20 LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
22 arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
25 LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, argument
28 arm_sys_send(seL4_SysSend, dest, msgInfo.words[0],
29 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
30 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
31 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
32 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
36 LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
38 arm_sys_send(seL4_SysNBSend, dest, msgInfo
41 seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
53 seL4_Reply(seL4_MessageInfo_t msgInfo) argument
58 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
168 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
187 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
230 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply) argument
267 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument
322 seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) argument
355 seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument
404 seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender) argument
437 seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
[all...]
/seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/
H A Dsyscalls.h194 LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
196 riscv_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1),
200 LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, argument
203 riscv_sys_send(seL4_SysSend, dest, msgInfo.words[0],
204 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
205 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
206 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
207 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
212 LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
214 riscv_sys_send(seL4_SysNBSend, dest, msgInfo
219 seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
232 seL4_Reply(seL4_MessageInfo_t msgInfo) argument
238 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
350 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
386 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
428 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply) argument
466 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument
521 seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) argument
555 seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument
605 seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender) argument
638 seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
[all...]
/seL4-l4v-master/seL4/include/benchmark/
H A Dbenchmark_track.h50 static inline void benchmark_debug_syscall_start(word_t cptr, word_t msgInfo, word_t syscall) argument
52 seL4_MessageInfo_t info = messageInfoFromWord_raw(msgInfo);
/seL4-l4v-master/seL4/include/arch/x86/arch/kernel/
H A Dtraps.h28 void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply)
30 void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
/seL4-l4v-master/seL4/include/arch/riscv/arch/kernel/
H A Dtraps.h21 void c_handle_syscall(word_t cptr, word_t msgInfo, word_t unused1, word_t unused2, word_t unused3, word_t unused4,
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/
H A Dsyscalls.h24 LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
26 x64_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
29 LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, argument
32 x64_sys_send(seL4_SysSend, dest, msgInfo.words[0],
40 LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
42 x64_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
45 LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, argument
48 x64_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
57 LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo) argument
59 x64_sys_reply(seL4_SysReply, msgInfo
62 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
250 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
269 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
310 seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply) argument
339 seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument
392 seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) argument
417 seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument
464 seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender) argument
494 seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument
[all...]
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/
H A Dsyscalls.h380 LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
382 x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1)));
386 LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) argument
388 LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1)
391 x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0,
395 LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
397 x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1)));
401 LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) argument
403 LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1)
406 x86_sys_send(seL4_SysNBSend, dest, msgInfo
411 seL4_Reply(seL4_MessageInfo_t msgInfo) argument
416 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) argument
565 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) argument
582 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) argument
618 seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply) argument
645 seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_CPtr reply) argument
687 seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender, seL4_CPtr reply) argument
708 seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender, seL4_Word *mr0, seL4_CPtr reply) argument
736 seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender) argument
754 seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender, seL4_Word *mr0) argument
[all...]
/seL4-l4v-master/seL4/include/arch/arm/arch/32/mode/fastpath/
H A Dfastpath.h82 in the bottom of the msgInfo word, is <= 4 and that msgExtraCaps
88 fastpath_mi_check(word_t msgInfo) argument
90 return ((msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits))
115 static inline void NORETURN FORCE_INLINE fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
130 register word_t msgInfo_reg asm("r1") = msgInfo;
/seL4-l4v-master/seL4/include/arch/x86/arch/32/mode/fastpath/
H A Dfastpath.h84 in the bottom of the msgInfo word, is <= seL4_FastMessageRegisters and that msgExtraCaps
88 static inline int fastpath_mi_check(word_t msgInfo) argument
90 return (msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits)) > seL4_FastMessageRegisters;
93 static inline void NORETURN FORCE_INLINE fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
130 "S"(msgInfo),
/seL4-l4v-master/seL4/include/arch/arm/arch/64/mode/fastpath/
H A Dfastpath.h67 in the bottom of the msgInfo word, is <= 4 and that msgExtraCaps
73 fastpath_mi_check(word_t msgInfo) argument
75 return (msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits)) > 4;
99 static inline void NORETURN FORCE_INLINE fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
110 register word_t msgInfo_reg asm("x1") = msgInfo;
/seL4-l4v-master/seL4/src/arch/riscv/
H A Dc_traps.c160 void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, word_t unused1, word_t unused2, word_t unused3, argument
169 fastpath_call(cptr, msgInfo);
173 fastpath_reply_recv(cptr, msgInfo, reply);
175 fastpath_reply_recv(cptr, msgInfo);
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/fastpath/
H A Dfastpath.h110 in the bottom of the msgInfo word, is <= 4 and that msgExtraCaps
116 fastpath_mi_check(word_t msgInfo) argument
118 return ((msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits))
122 static inline void NORETURN FORCE_INLINE fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
210 "S"(msgInfo),
254 "S"(msgInfo)
/seL4-l4v-master/seL4/include/arch/riscv/arch/fastpath/
H A Dfastpath.h65 in the bottom of the msgInfo word, is <= 4 and that msgExtraCaps
71 fastpath_mi_check(word_t msgInfo) argument
73 return (msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits)) > 4;
95 static inline void NORETURN FORCE_INLINE fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument
114 register word_t msgInfo_reg asm("a1") = msgInfo;
/seL4-l4v-master/seL4/src/fastpath/
H A Dfastpath.c24 void NORETURN fastpath_call(word_t cptr, word_t msgInfo) argument
39 info = messageInfoFromWord_raw(msgInfo);
45 if (unlikely(fastpath_mi_check(msgInfo) ||
219 msgInfo = wordFromMessageInfo(seL4_MessageInfo_set_capsUnwrapped(info, 0));
221 fastpath_restore(badge, msgInfo, NODE_STATE(ksCurThread));
231 void NORETURN fastpath_reply_recv(word_t cptr, word_t msgInfo, word_t reply) argument
233 void NORETURN fastpath_reply_recv(word_t cptr, word_t msgInfo)
251 info = messageInfoFromWord_raw(msgInfo);
257 if (unlikely(fastpath_mi_check(msgInfo) ||
491 msgInfo
[all...]
/seL4-l4v-master/seL4/src/arch/x86/
H A Dc_traps.c142 void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply) argument
144 void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
158 benchmark_debug_syscall_start(cptr, msgInfo, syscall);
172 fastpath_call(cptr, msgInfo);
176 fastpath_reply_recv(cptr, msgInfo, reply);
178 fastpath_reply_recv(cptr, msgInfo);
/seL4-l4v-master/l4v/camkes/glue-proofs/
H A DRPCFrom.c1494 msgInfo
1518 msgInfo
1681 msgInfo
1709 msgInfo
H A DRPCTo.c1204 msgInfo
1232 msgInfo
/seL4-l4v-master/seL4/src/kernel/
H A Dthread.c225 seL4_MessageInfo_t msgInfo; local
228 msgInfo = seL4_MessageInfo_new(
230 setRegister(receiver, msgInfoRegister, wordFromMessageInfo(msgInfo));
/seL4-l4v-master/seL4/src/arch/x86/64/
H A Dtraps.S609 push %rsi # save RSI (msgInfo register)
653 push %rsi # save RSI (msgInfo register)

Completed in 106 milliseconds

12