/seL4-l4v-master/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/ |
H A D | syscalls_sysenter.h | 26 register seL4_Word mr1 asm("r8") = msg1; 40 "r"(mr1), 52 register seL4_Word mr1 asm("r8") = msg1; 65 "r"(mr1), 92 register seL4_Word mr1 asm("r8"); 105 "=r"(mr1), 115 *out_mr1 = mr1; 125 register seL4_Word mr1 asm("r8") = *in_out_mr1; 137 "=r"(mr1), 145 "r"(mr1), [all...] |
H A D | syscalls_syscall.h | 25 register seL4_Word mr1 asm("r8") = msg1; 38 "r"(mr1), 50 register seL4_Word mr1 asm("r8") = msg1; 62 "r"(mr1), 89 register seL4_Word mr1 asm("r8"); 101 "=r"(mr1), 110 *out_mr1 = mr1; 120 register seL4_Word mr1 asm("r8") = *in_out_mr1; 131 "=r"(mr1), 139 "r"(mr1), [all...] |
H A D | syscalls.h | 30 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 34 (mr1 != seL4_Null) ? *mr1 : 0, 46 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 50 (mr1 != seL4_Null) ? *mr1 : 0, 63 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 67 (mr1 != seL4_Null) ? *mr1 : 0, 88 seL4_Word mr1; local 29 seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 45 seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 62 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 107 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply) argument 152 seL4_Word mr1; local 176 seL4_Word mr1; local 194 seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 231 seL4_Word mr1; local 255 seL4_Word mr1 = seL4_GetMR(1); local 269 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 319 seL4_Word mr1 = seL4_GetMR(1); local 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 398 seL4_Word mr1 = seL4_GetMR(1); local 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 470 seL4_Word mr1 = seL4_GetMR(1); local 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 561 seL4_Word mr1 = seL4_GetMR(1); local [all...] |
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | syscalls.h | 33 static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, argument 50 "D"(mr1) 60 static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2) argument 75 "D"(mr1), 212 static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, seL4_Word mr2) argument 228 "D"(mr1) 239 static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2) argument 252 "D"(mr1), 375 #define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 416 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) argument 437 LIBSEL4_UNUSED seL4_Word mr1; local 493 LIBSEL4_UNUSED seL4_Word mr1; local 569 LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); local 627 LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); local 792 LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); local [all...] |
/seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/ |
H A D | syscalls.h | 25 static inline void riscv_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, argument 33 register seL4_Word msg1 asm("a3") = mr1; 48 static inline void riscv_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2, argument 55 register seL4_Word msg1 asm("a3") = mr1; 201 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 205 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 220 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 224 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 200 seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 219 seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 238 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 285 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 386 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 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 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 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 718 seL4_WaitWithMRs(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/arm/sel4/arch/ |
H A D | syscalls.h | 26 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 30 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 42 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 46 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 59 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 63 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 105 seL4_Word *mr0, seL4_Word *mr1, seL4_Wor 25 seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 41 seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 58 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 104 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 187 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 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 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 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 517 seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument [all...] |
/seL4-l4v-master/HOL4/src/real/ |
H A D | netsScript.sml | 249 ���!(g:'a->'a->bool) f. bounded(mr1,g) f = 278 (x tends x0)(mtop(mr1),g) = ((\n. x(n) - x0) tends &0)(mtop(mr1),g)���, 285 (x tends x0)(mtop(mr1),g) ==> bounded(mr1,g) x���, 296 (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==> 310 (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==> 311 bounded(mr1,g) (\n. inv(x n))���, 355 !x y. (x tends &0)(mtop(mr1),g) /\ (y tends &0)(mtop(mr1), [all...] |
H A D | metricScript.sml | 226 val mr1 = new_definition("mr1", value 227 ���mr1 = metric(\(x,y). abs(y - x))���); 230 ���!x y. (dist mr1)(x,y) = abs(y - x)���, 231 REPEAT GEN_TAC THEN REWRITE_TAC[mr1, REWRITE_RULE[metric_tybij] ISMET_R1] 235 ���!x d. (dist mr1)(x,x + d) = abs(d)���, 239 ���!x d. (dist mr1)(x,x - d) = abs(d)���, 243 ���!x d. &0 <= d ==> ((dist mr1)(x,x + d) = d)���, 247 ���!x d. &0 <= d ==> ((dist mr1)(x,x - d) = d)���, 251 ���!x d. &0 < d ==> ((dist mr1)( [all...] |
H A D | seqScript.sml | 63 ���$--> x x0 = (x tends x0)(mtop(mr1), ^geq)���,750); 204 ���!s. bounded(mr1, ^geq) s = ?k. !n. abs(s n) < k���, 222 ���!f k k'. (!n. k <= f(n) /\ f(n) <= k') ==> bounded(mr1, ^geq) f���, 247 ���!f. cauchy f ==> bounded(mr1, ^geq) f���, 261 ���!f. bounded(mr1, ^geq) f /\ (!m n:num. m >= n ==> f(m) >= f(n)) 326 ���!f. bounded(mr1, ^geq)(\n. ~(f n)) = bounded(mr1, ^geq) f���, 331 ���!f. bounded(mr1, ^geq) f /\ mono f ==> convergent f���, 431 ���!s f. bounded(mr1,^geq) s ==> bounded(mr1, [all...] |
H A D | limScript.sml | 30 (f tends l)(mtop(mr1),tendsto(mr1,x0))���);
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/ |
H A D | syscalls.h | 57 static inline void arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, argument 65 register seL4_Word msg1 asm("x3") = mr1; 80 static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2, argument 87 register seL4_Word msg1 asm("x3") = mr1;
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/ |
H A D | syscalls.h | 56 static inline void arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, argument 64 register seL4_Word msg1 asm("r3") = mr1; 79 static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2, argument 86 register seL4_Word msg1 asm("r3") = mr1;
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/ |
H A D | syscalls.h | 56 static inline void arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, argument 64 register seL4_Word msg1 asm("r3") = mr1; 79 static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2, argument 86 register seL4_Word msg1 asm("r3") = mr1;
|
/seL4-l4v-master/seL4/src/arch/arm/object/ |
H A D | vcpu.c | 399 uint32_t mr0, mr1; local 409 mr1 = getSyscallArg(1, buffer); 413 index = mr1 & 0xff;
|
/seL4-l4v-master/HOL4/src/probability/ |
H A D | real_topologyScript.sml | 157 Dist = dist mr1 2226 ball = metric$B(mr1) [all...] |