Searched refs:word (Results 1 - 25 of 347) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/basis/
H A DWordSignature.sml23 eqtype word
25 val toLarge : word -> LargeWord.word
26 val toLargeX : word -> LargeWord.word
27 val toLargeWord : word -> LargeWord.word
28 val toLargeWordX : word -> LargeWord.word
29 val fromLarge : LargeWord.word
[all...]
H A DForeignMemory.sml24 val volatileRef: SysWord.word -> volatileRef
25 val setVolatileRef: volatileRef * SysWord.word -> unit
26 val getVolatileRef: volatileRef -> SysWord.word
29 val voidStar2Sysword: voidStar -> SysWord.word
30 val sysWord2VoidStar: SysWord.word -> voidStar
33 (* Helper functions to add a word value to an address.
34 From 5.8.2 the word value is treated as signed. *)
35 val ++ : voidStar * word -> voidStar
36 val -- : voidStar * word -> voidStar
45 val malloc: word
[all...]
H A DWord32In64.sml31 require boxed word values. DCJM 14/8/09.
44 (* Values of type Word32.word can be in the range 0.. 4294967295 *)
47 val maxWordAsWord: word = (Word.fromInt maxWord)
58 (* Internal function to convert from Word.word. *)
59 fun fromWord (w: Word.word) = andb(w, maxWordAsWord)
61 (* Converting from LargeWord.word. First convert to Word.word and
75 fun op ~>> (a: word, b: Word.word): word
[all...]
H A DForeign.581.sml30 val volatileRef: SysWord.word -> volatileRef
31 val setVolatileRef: volatileRef * SysWord.word -> unit
32 val getVolatileRef: volatileRef -> SysWord.word
42 (* Both volatileRef and SysWord.word are the ADDRESSes of the actual value. *)
43 type volatileRef = word ref
45 val memMove: SysWord.word * SysWord.word * word * word* word
[all...]
H A DLibrarySupport.sml29 val wordSize : word = RunCall.bytesPerWord
32 val sysWordSize: word = RunCall.memoryCellLength(Word.toLargeWord 0w0) * wordSize
40 datatype array = Array of word*address
44 datatype array = Array of word*address
46 val wVecLength: vector -> word
50 val wordSize: word and sysWordSize: word
52 val allocString: word -> string (* Create a mutable string. *)
53 val allocBytes: word -> address
56 val unsignedShortOrRaiseSubscript: int -> word
[all...]
H A DWord32InLargeWord64.sml41 (* Values of type Word32.word can be in the range 0.. 4294967295 *)
44 val maxWordAsWord: word = (LargeWord.fromLargeInt maxWord)
55 (* Internal function to convert from Word.word. *)
56 fun fromWord (w: LargeWord.word) = andb(w, maxWordAsWord)
58 (* Converting from LargeWord.word. First convert to LargeWord.word and
72 fun op ~>> (a: word, b: Word.word): word =
75 (* Convert to a large word b
[all...]
H A DForeignConstants.sml27 val sizeFloat: word = RunCall.rtsCallFast1 "PolySizeFloat" ()
28 and sizeDouble: word = RunCall.rtsCallFast1 "PolySizeDouble" ()
29 and sizeShort: word = RunCall.rtsCallFast1 "PolySizeShort" ()
30 and sizeInt: word = RunCall.rtsCallFast1 "PolySizeInt" ()
31 and sizeLong: word = RunCall.rtsCallFast1 "PolySizeLong" ()
41 and wordSize : word = RunCall.bytesPerWord
42 and sysWordSize: word = LibrarySupport.sysWordSize
H A DWord16.sml29 (* 16-bit words have values that range from 0...65535 and like Word8.word
33 val maxWordAsWord: word = RunCall.unsafeCast maxWord
45 (* Internal function to convert from Word.word. *)
46 fun fromWord (w: Word.word) = andb(w, maxWordAsWord)
48 (* Converting from LargeWord.word. First convert to Word.word and
59 fun op ~>> (a: word, b: Word.word): word =
63 fun op << (a: word,
[all...]
H A DLargeWord.sml23 hold the full machine word values for certain operating-system calls.
26 (* This uses the global definition of type "word" made in the compiler.
30 type largeword = LargeWord.word
31 and shortword = Word.word
33 (* Extract a word value from a character stream. *)
35 Int.scan. A word value may, optionally, be preceded by 0w or
128 (* Conversion from arbitrary precision integer may involve extracting the low-order word
131 val getLowOrderWord: LargeInt.int -> LargeWord.word =
135 fun wordFromLargeInt (i: LargeInt.int): word =
140 and largeWordFromLargeInt (i: LargeInt.int): LargeWord.word
171 structure Word :> WORD where type word = shortword = type
177 type word = word type
228 structure LargeWord:> WORD where type word = largeword = type
231 type word = largeword type
[all...]
H A DWord8.sml29 (* Values of type Word8.word can be in the range 0..255 and
39 Word8.word values and Char.char. It assumes that the underlying
44 val maxWordAsWord: word = RunCall.unsafeCast maxWord
56 (* Internal function to convert from Word.word. *)
57 fun fromWord (w: Word.word) = andb(w, maxWordAsWord)
59 (* Converting from LargeWord.word. First convert to Word.word and
76 fun op ~>> (a: word, b: Word.word): word
[all...]
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dspell_checker.scala118 (word, upd) <- updates.iterator
120 } yield word
122 private def excluded(word: String): Boolean =
123 updates.get(word) match {
135 Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
136 } yield (word, Spell_Checker.Update(include, true))
151 word <- main_dictionary.iterator ++ included_iterator()
152 if !excluded(word)
153 } add.invoke(factory, word)
163 (word, up
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dspell_checker.scala118 (word, upd) <- updates.iterator
120 } yield word
122 private def excluded(word: String): Boolean =
123 updates.get(word) match {
135 Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
136 } yield (word, Spell_Checker.Update(include, true))
151 word <- main_dictionary.iterator ++ included_iterator()
152 if !excluded(word)
153 } add.invoke(factory, word)
163 (word, up
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/multiword/
H A Dmc_multiwordScript.sml101 :num # �� word # �� word list # �� word list -> (num # �� word # �� word list # ��
102 word list + num # �� word # �� word list # �� word list) # bool``;
115 :num # �� word # �� wor
[all...]
/seL4-l4v-master/seL4/src/arch/x86/
H A Dmultiboot.S70 .word 0x0
71 .word 0x0
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_random_testingLib.sml139 fun dp () = case rand_term ``:word4 -> bool -> 'reg word -> 'reg word ->
167 fun mul () = case rand_term ``:bool -> bool -> 'reg word -> 'reg word ->
168 'reg word -> 'reg word``
176 'reg word -> 'reg word``
228 hd (rand_term ``:'reg word``)))
236 'reg word
[all...]
/seL4-l4v-master/HOL4/src/n-bit/
H A DwordsScript.sml31 Type word[pp] = ���:bool['a]���
48 w2n (w:'a word) = SUM ^WL (\i. SBIT (w ' i) i)`
51 (n2w:num->'a word) n = FCP i. BIT i n`
55 val _ = Parse.add_user_printer ("wordspp.words_printer", ``words$n2w x : 'a word``)
58 (w2w:'a word -> 'b word) w = n2w (w2n w)`
61 (sw2sw:'a word -> 'b word) w =
96 word_T = (n2w:num->'a word) (UINT_MAX(:'a))`
99 word_L = (n2w:num->'a word) (INT_MI
[all...]
H A DbitstringScript.sml81 w2v (w : 'a word) =
85 v2w v : 'a word = FCP i. testbit i v`
221 `!w:'a word. LENGTH (w2v w) = dimindex(:'a)`,
291 `!w: 'a word n.
333 !n v. word_bit n (v2w v : 'a word) <=> n < dimindex(:'a) /\ testbit n v
344 `!v i. (v2w v : 'a word) ' i =
349 (v2w v : 'a word) i`,
353 `!n w. testbit n (w2v (w : 'a word)) = word_bit n w`,
369 `!v. w2v (v2w v : 'a word) = fixwidth (dimindex(:'a)) v`,
381 `!v. v2w (fixwidth (dimindex(:'a)) v) = v2w v : 'a word`,
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Dtypes.ml15 let word = ":^posn->bool";;
17 let wordsig = ":^time->^word";;
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DRandom.sig4 Simple generator for pseudo-random numbers, using unboxed word
12 val nextWord : unit -> word
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DRandom.sig4 Simple generator for pseudo-random numbers, using unboxed word
12 val nextWord : unit -> word
/seL4-l4v-master/seL4/include/api/
H A Ddebug.h25 printf("Interrupt, irq %lu\n", (unsigned long) ksKernelEntry.word);
28 printf("Unknown syscall, word: %lu", (unsigned long) ksKernelEntry.word);
31 printf("VM Fault, fault type: %lu\n", (unsigned long) ksKernelEntry.word);
34 printf("User level fault, number: %lu", (unsigned long) ksKernelEntry.word);
38 printf("Debug fault. Fault Vaddr: 0x%lx", (unsigned long) ksKernelEntry.word);
/seL4-l4v-master/HOL4/src/integer/
H A Dinteger_wordScript.sml27 i2w (i : int) : 'a word =
44 saturate_i2w i : 'a word =
53 saturate_i2sw i : 'a word =
62 saturate_sw2sw (w: 'a word) = saturate_i2sw (w2i w)`
65 saturate_w2sw (w: 'a word) = saturate_i2sw (&w2n w)`
68 saturate_sw2w (w: 'a word) = saturate_i2w (w2i w)`
71 signed_saturate_add (a: 'a word) (b: 'a word) =
72 saturate_i2sw (w2i a + w2i b) : 'a word`
75 signed_saturate_sub (a: 'a word) (
[all...]
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Djedit_spell_checker.scala45 Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
46 } yield (spell_checker, word)
49 case Some((spell_checker, word)) =>
56 if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word"))
60 if (spell_checker.check(word))
61 List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
63 List(item("isabelle.include-word"), item("isabelle.include-word
[all...]
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_spell_checker.scala45 Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
46 } yield (spell_checker, word)
49 case Some((spell_checker, word)) =>
56 if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word"))
60 if (spell_checker.check(word))
61 List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
63 List(item("isabelle.include-word"), item("isabelle.include-word
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/
H A Dtemporal_stateScript.sml150 `!x (prefix: 'a word list) (postfix: 'a word list) p c q m i a l1 l2.
162 ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i
163 (a - n2w (LENGTH prefix) * i) (prefix: 'a word list)``)
167 ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i
168 (a - n2w (LENGTH (prefix: 'a word list)) * i +
170 (postfix: 'a word list)``)

Completed in 217 milliseconds

1234567891011>>