sel4/sel4_arch/syscalls.h

435     seL4_Word badge;
439     x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1));
446         *sender = badge;
461     seL4_Word badge;
465     x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, MCS_COND(reply, &msg1));
478         *sender = badge;
491     seL4_Word badge;
495     x86_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1));
503         *sender = badge;
513     seL4_Word badge;
516     x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &mr0, 0);
521         *sender = badge;
531     seL4_Word badge;
534     x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, 0);
541         *sender = badge;
550     seL4_Word badge;
553     x86_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &mr0, 0);
558         *sender = badge;
625     seL4_Word badge;
629     x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0,
638         *sender = badge;
655     seL4_Word badge;
668     x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1));
680         *sender = badge;
691     seL4_Word badge;
697     x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &mr0, reply);
702         *sender = badge;
713     seL4_Word badge;
723     x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, reply);
730         *sender = badge;
740     seL4_Word badge;
743     x86_sys_nbsend_wait(seL4_SysNBSendWait, src, &badge, msgInfo.words[0], &info.words[0], &mr0, dest);
748         *sender = badge;
759     seL4_Word badge;
766     x86_sys_nbsend_wait(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, dest);
773         *sender = badge;
790     seL4_Word badge;
794     x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, MCS_COND(0, &mr1));
801         *sender = badge;