/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | UnclockedSemanticsScript.sml | 92 * where w is a word, i.e. a list of letters: w : ('prop -> bool)list 117 * where w is a finite or infinite word i.e. w : ('prop -> bool)path 169 * where w is a finite or infinite word i.e. w : ('prop -> bool)path
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | IntArray2.sml | 64 where type elem = Word8.word = 67 type elem = Word8.word 69 type elem = Word8.word
|
H A D | String.sml | 31 address*address*word*word*word->unit = RunCall.moveBytes 33 val wordSize : word = LibrarySupport.wordSize 36 fun singleCharString(c: word): string = 46 val intAsWord: int -> word = RunCall.unsafeCast 58 val bcopy: string*string*word*word*word -> unit = RunCall.moveBytes 61 fun unsafeStringSub(s: string, i: word) [all...] |
H A D | BoolArray.sml | 22 (* TODO: Use a single word for vectors of size <= number of bits in a word. *) 23 (* We use int here for the length rather than word because the number of bits 24 could be more than the maximum value of Word.word. *) 28 val wordSize : word = LibrarySupport.wordSize 30 (* Casts between int and word. *) 31 val intAsWord: int -> word = RunCall.unsafeCast 32 and wordAsInt: word -> int = RunCall.unsafeCast 45 val words : word = 150 fun do_move last byte len : word [all...] |
H A D | Windows.sml | 60 | DWORD of SysWord.word 70 val platformWin32s : SysWord.word 71 val platformWin32Windows : SysWord.word 72 val platformWin32NT : SysWord.word 73 val platformWin32CE : SysWord.word 76 { majorVersion: SysWord.word, minorVersion: SysWord.word, 77 buildNumber: SysWord.word, platformId: SysWord.word, 98 serialNumber : SysWord.word, [all...] |
H A D | Posix.sml | 23 val toWord : syserror -> SysWord.word 24 val fromWord : SysWord.word -> syserror 77 val toWord : signal -> SysWord.word 78 val fromWord : SysWord.word -> signal 105 val wordToPid : SysWord.word -> pid 106 val pidToWord : pid -> SysWord.word 116 W_EXITED | W_EXITSTATUS of Word8.word 131 val exit : Word8.word -> 'a 147 val uidToWord : uid -> SysWord.word 148 val wordToUid : SysWord.word [all...] |
H A D | VectorOperations.sml | 29 val length: vector -> word 30 val unsafeSub: vector * word -> elem 31 val unsafeSet: vector * word * elem -> unit (* Array only *) 49 val wordAsInt: word -> int = RunCall.unsafeCast
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | wordspp.sml | 13 val _ = Feedback.register_btrace ("word cast printing", word_cast_on) 14 val _ = Feedback.register_trace ("word printing", word_pp_mode, 6) 15 val _ = Feedback.register_btrace ("word pp as 2's comp", int_word_pp)
|
/seL4-l4v-master/seL4/src/arch/arm/machine/ |
H A D | gic_v3.c | 301 int word = hw_irq >> 4; local 307 icfgr = gic_dist->icfgrn[word]; 322 gic_dist->icfgrn[word] = icfgr;
|
/seL4-l4v-master/HOL4/src/floating-point/ |
H A D | machine_ieeeScript.sml | 22 convert (to_float: 'a word -> ('b, 'c) float) 23 (from_float: ('d, 'e) float -> 'f word) from_real_with_flags
|
H A D | binary_ieeeScript.sml | 30 float = <| Sign : word1; Exponent : 'w word; Significand : 't word |>` 124 Exponent := UINT_MAXw: 'w word; 125 Significand := 0w: 't word |>` 130 Exponent := 0w: 'w word; 131 Significand := 0w: 't word |>` 136 Exponent := UINT_MAXw - 1w: 'w word; 137 Significand := UINT_MAXw: 't word |>` 142 Exponent := 0w: 'w word; 143 Significand := 1w: 't word |>` [all...] |
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Thread_Attributes.sml | 27 abstype attributes = Attributes of Word.word 47 fun load_word () : word =
|
/seL4-l4v-master/seL4/src/arch/x86/32/ |
H A D | head.S | 136 .word (3 * 8) - 1 /* Limit: 3 segments * 8 bytes - 1 byte */
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Message.sml | 329 set the first word to the length of the buffer. *) 342 (* The first word is supposed to contain the length *) 763 val toHMENU: SysWord.word -> HMENU = handleOfVoidStar o Memory.sysWord2VoidStar 764 and fromHMENU: HMENU -> SysWord.word = Memory.voidStar2Sysword o voidStarOfHandle 765 val toHWND: SysWord.word -> HWND = handleOfVoidStar o Memory.sysWord2VoidStar 766 and fromHWND: HWND -> SysWord.word = Memory.voidStar2Sysword o voidStarOfHandle 767 val toHDC: SysWord.word -> HDC = handleOfVoidStar o Memory.sysWord2VoidStar 768 and fromHDC: HDC -> SysWord.word = Memory.voidStar2Sysword o voidStarOfHandle 769 val toHFONT: SysWord.word -> HFONT = handleOfVoidStar o Memory.sysWord2VoidStar 770 and fromHFONT: HFONT -> SysWord.word [all...] |
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Numerics.sig | 5 type word8 = Word8.word;
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | MutableMapFunctor.sml | 5 functor MutableMap (val arrayBits : Word.word) :> Map =
|
H A D | Ptree.sml | 11 | Branch of IntInf.int * word * 'a ptree * 'a ptree
|
H A D | assemblerLib.sml | 61 fun word n s = Option.valOf (BitsN.fromHexString (s, Nat.fromNativeInt n)) function
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patricia_castsLib.sml | 36 "At least one key is larger than the required word length.";
|
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ClockedSemanticsScript.sml | 61 * where v is a finite word, i.e. a list of letters: v : ('a letter)list. 119 * where v is a finite word, i.e. a list of letters: v : ('a letter)list. 157 * where v is a finite or infinite word i.e. v : ('prop letter)path 228 * where v is a finite or infinite word i.e. v : ('prop letter)path
|
H A D | UnclockedSemanticsScript.sml | 82 * where v is a finite word, i.e. a list of letters: v : ('a letter)list. 136 * where v is a finite word, i.e. a list of letters: v : ('a letter)list. 201 * where v is a finite or infinite word i.e. v : ('prop -> bool)path 262 * where v is a finite or infinite word i.e. v : ('prop -> bool)path
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_astScript.sml | 42 | Pbc of word5 => crbit => 14 word (* conditional branch *) 101 | Pstb of ireg => ppc_constant => ireg (* store 8-bit word *) 107 | Psth of ireg => ppc_constant => ireg (* store 16-bit word *) 109 | Pstw of ireg => ppc_constant => ireg (* store 32-bit word*)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/step/ |
H A D | mips_stepScript.sml | 280 ((39 >< 0) w = (a4 @@ a3 @@ a2 @@ a1 @@ a0) : 40 word) /\ 282 ((55 >< 0) w = (a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : 56 word) /\ 291 ((63 >< 8) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1) : 56 word) /\ 293 ((63 >< 24) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3) : 40 word) /\ 348 ((((63 >< 3) a) : 61 word) @@ (b : word3)) && ~7w = a && ~7w`, 352 `!a:word64. (((63 >< 3) a) : 61 word) @@ ((2 >< 0) a : word3) = a`, 437 wordsLib.WORD_DECIDE ``!a b:'a word. a <=+ b /\ b <=+ a = (a = b)``
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_encoderLib.sml | 534 [(``0b101100001w:9 word``,7), (imm32$(8,2),0)] 554 [(``0b100001001w:9 word``,6), (n,3), (d,0)] 614 [(``0b100001010w:9 word``,6), (m,3), (n,0)] 950 [(``0b100111101111010001111w:21 word``,8), (imm12$(7,0),0)] 1003 [(``0b110110101w:9 word``,20), (n,16), (a,12), (d,8), (r,4), (m,0)] 1043 [(``0b110101011w:9 word``,20), (m,16), (PC,12), (d,8), (T,7), (m,0)] 1045 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), 1048 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), (T,7), (m,0)] 1050 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), 1053 [(``0b110101001w:9 word``,2 [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | GraphLangScript.sml | 22 | VarWord ('a word) 23 | VarMem ('a word -> word8) 24 | VarDom ('a word set) 161 jump = Jump ('a word) | Return` 169 inst = Inst ('a word) ('a assert) ('a next) (* name, inv, what happens *)` 172 func = Func string ('a word) ('a inst list) (* name, entry point, insts *)`; 403 IMPL_INST code locs (Inst (n:'a word) assert next) = 758 ?a t. find_inst ((n2w n) :'a word) l = SOME (Inst (n2w n) a t)``, 919 (find_inst (n2w i) l = SOME (Inst ((n2w i) :'a word) a next)) ==> 933 \\ Cases_on `next_trans (w2n (c:'a word)) k [all...] |