/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | bugzilla213.c | 15 fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) argument 18 register word_t r1 asm ("r1") = msgInfo;
|
H A D | volatile_asm.c | 15 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 D | syscalls_master.h | 24 * @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 D | syscalls_mcs.h | 24 * @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 D | traps.h | 25 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 D | c_traps.c | 126 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 D | syscalls.h | 20 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 D | syscalls.h | 194 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 D | benchmark_track.h | 50 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 D | traps.h | 28 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 D | traps.h | 21 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 D | syscalls.h | 24 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 D | syscalls.h | 380 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 D | fastpath.h | 82 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 D | fastpath.h | 84 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 D | fastpath.h | 67 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 D | c_traps.c | 160 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 D | fastpath.h | 110 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 D | fastpath.h | 65 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 D | fastpath.c | 24 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 D | c_traps.c | 142 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 D | RPCFrom.c | 1494 msgInfo 1518 msgInfo 1681 msgInfo 1709 msgInfo
|
H A D | RPCTo.c | 1204 msgInfo 1232 msgInfo
|
/seL4-l4v-master/seL4/src/kernel/ |
H A D | thread.c | 225 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 D | traps.S | 609 push %rsi # save RSI (msgInfo register) 653 push %rsi # save RSI (msgInfo register)
|