Searched refs:word (Results 101 - 125 of 347) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/
H A DUnclockedSemanticsScript.sml92 * 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 DIntArray2.sml64 where type elem = Word8.word =
67 type elem = Word8.word
69 type elem = Word8.word
H A DString.sml31 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 DBoolArray.sml22 (* 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 DWindows.sml60 | 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 DPosix.sml23 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 DVectorOperations.sml29 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 Dwordspp.sml13 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 Dgic_v3.c301 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 Dmachine_ieeeScript.sml22 convert (to_float: 'a word -> ('b, 'c) float)
23 (from_float: ('d, 'e) float -> 'f word) from_real_with_flags
H A Dbinary_ieeeScript.sml30 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 DThread_Attributes.sml27 abstype attributes = Attributes of Word.word
47 fun load_word () : word =
/seL4-l4v-master/seL4/src/arch/x86/32/
H A Dhead.S136 .word (3 * 8) - 1 /* Limit: 3 segments * 8 bytes - 1 byte */
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DMessage.sml329 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 DRegexp_Numerics.sig5 type word8 = Word8.word;
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DMutableMapFunctor.sml5 functor MutableMap (val arrayBits : Word.word) :> Map =
H A DPtree.sml11 | Branch of IntInf.int * word * 'a ptree * 'a ptree
H A DassemblerLib.sml61 fun word n s = Option.valOf (BitsN.fromHexString (s, Nat.fromNativeInt n)) function
/seL4-l4v-master/HOL4/src/finite_maps/
H A Dpatricia_castsLib.sml36 "At least one key is larger than the required word length.";
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/
H A DClockedSemanticsScript.sml61 * 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 DUnclockedSemanticsScript.sml82 * 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 Dppc_astScript.sml42 | 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 Dmips_stepScript.sml280 ((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 Darm_encoderLib.sml534 [(``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 DGraphLangScript.sml22 | 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...]

Completed in 145 milliseconds

1234567891011>>