/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | WordSignature.sml | 23 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 D | ForeignMemory.sml | 24 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 D | Word32In64.sml | 31 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 D | Foreign.581.sml | 30 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 D | LibrarySupport.sml | 29 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 D | Word32InLargeWord64.sml | 41 (* 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 D | ForeignConstants.sml | 27 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 D | Word16.sml | 29 (* 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 D | LargeWord.sml | 23 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 D | Word8.sml | 29 (* 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 D | spell_checker.scala | 118 (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 D | spell_checker.scala | 118 (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 D | mc_multiwordScript.sml | 101 :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 D | multiboot.S | 70 .word 0x0 71 .word 0x0
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_random_testingLib.sml | 139 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 D | wordsScript.sml | 31 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 D | bitstringScript.sml | 81 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 D | types.ml | 15 let word = ":^posn->bool";; 17 let wordsig = ":^time->^word";;
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Random.sig | 4 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 D | Random.sig | 4 Simple generator for pseudo-random numbers, using unboxed word 12 val nextWord : unit -> word
|
/seL4-l4v-master/seL4/include/api/ |
H A D | debug.h | 25 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 D | integer_wordScript.sml | 27 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 D | jedit_spell_checker.scala | 45 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 D | jedit_spell_checker.scala | 45 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 D | temporal_stateScript.sml | 150 `!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)``)
|