| /seL4-l4v-10.1.1/seL4/include/api/ |
| H A D | types.h | 74 seL4_MessageInfo_t mi; local
76 mi.words[0] = w;
77 return mi;
83 seL4_MessageInfo_t mi; local
86 mi.words[0] = w;
88 len = seL4_MessageInfo_get_length(mi);
90 mi = seL4_MessageInfo_set_length(mi, seL4_MsgMaxLength);
93 return mi;
97 wordFromMessageInfo(seL4_MessageInfo_t mi) argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/monad/ |
| H A D | monadsyntax.sml | 47 fun write_keyval (nm, mi) =
51 List [List [String nm, MonadInfo.toSexp mi]]
353 | SOME mi => mi
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_parseScript.sml | 436 ?r4i r5i r6i r7i r8i gi mi.
438 (a,r4i,k + n2w (LENGTH s),r6i,r7i,r8i,df,dg,dm,f,gi,mi)) /\
439 symbol_table [s] {(a,s)} (a,dm,mi,dg,gi) /\
440 !i. i <+ a ==> (gi i = g i) /\ (mi i = m i)``,
562 ?r3i r4i r6i r7i r8i gi mi.
564 (r3i,r4i,k + n2w (LENGTH s),r6i,r7i,r8i,df,dg,dm,f,gi,mi)) /\
565 symbol_table (add_symbol s xs) ((r3i,s) INSERT x) (a,dm,mi,dg,gi) /\
566 !i. i <+ a ==> (gi i = g i) /\ (mi i = m i)``,
679 ?r3i r4i r5i r6i r7i r8i gi mi.
681 (r3i,r4i,r5i,r6i,r7i,r8i,df,dg,dm,f,gi,mi)) /\
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | codegen_armLib.sml | 129 (* negative *) if tm = ``aS1 psrN`` then ("mi","pl") else
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperMath.sml | 470 val (mi, ax_b) = dest_divides c1 value
478 val m = dest_injected mi
488 extended_gcd (Arbint.toNat (Arbint.*(int_of_term ui, int_of_term mi)),
494 val pum = list_mk_mult [p, ui, mi]
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | armLib.sml | 57 | "mi" => 4
|
| H A D | arm_disassemblerLib.sml | 166 | 4 => "mi"
|
| H A D | arm_parserLib.sml | 698 | "mi" => 4
721 ["eq","ne","cs","hs","cc","lo","mi","pl","vs",
|
| /seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
| H A D | datatypes.sml | 259 (* obj ::= x | [li=mi] i in 1..n | a.l | a.l:=m *)
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
| H A D | objectScript.sml | 49 (* obj1 ::= x | [li=mi] i in 1..n | a.l | a.l:=m *)
|
| H A D | alphaScript.sml | 47 (* obj1 ::= x | [li=mi] i in 1..n | a.l | a.l:=m *)
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
| H A D | emit_eval.sml | 209 | 4 => "mi"
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/ |
| H A D | prog_armLib.sml | 574 val (x,y) = if tm2 = ``aS1 psrN`` then ("mi","pl") else
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | assemblerML.sml | 120 | MI => "mi" | PL => "pl" | VS => "vs" | VC => "vc"
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8.sml | 6874 | "mi" => Option.SOME(BitsN.B(0x4,4))
6896 | "mi" => "pl"
6897 | "pl" => "mi"
8555 | BitsN.B(0x4,_) => "mi"
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0.sml | 3777 | "mi" => Option.SOME(BitsN.B(0x4,4))
4623 | BitsN.B(0x4,_) => "mi"
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/Manual/ |
| H A D | quotient.tex | 5101 (* obj1 ::= x | [li=mi] i in 1..n | a.l | a.l:=m *)
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 23430 | "mi" => Option.SOME(BitsN.B(0x4,4))
26161 | BitsN.B(0x4,_) => "mi"
|