/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | wordScript.sml | 3 val _ = new_theory "word" 5 val _ = Datatype` word = WORD (num -> 'a set)`;
|
/seL4-l4v-master/seL4/libsel4/include/sel4/ |
H A D | benchmark_track_types.h | 45 seL4_Word word: 26; member in struct:kernel_entry::__anon168::__anon169
|
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_spell_checker.scala | 38 Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) 39 } yield (spell_checker, word) 42 case Some((spell_checker, word)) => 52 if (spell_checker.check(word))
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_spell_checker.scala | 38 Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) 39 } yield (spell_checker, word) 42 case Some((spell_checker, word)) => 52 if (spell_checker.check(word))
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Windows.581.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 | Byte.sml | 23 val byteToChar : Word8.word -> char 24 val charToByte : char -> Word8.word 34 (* Chars and Word8.word values are both tagged integers in the 36 fun byteToChar (w: Word8.word): char = RunCall.unsafeCast w 37 fun charToByte (c: char) : Word8.word = RunCall.unsafeCast c
|
H A D | Word8Array.sml | 24 way as strings, with a length word in the first word, or we 34 val System_move_bytes: address*address*word*word*word->unit = RunCall.moveBytes 36 fun System_move_str(src: vector, dst: address, srcOffset: word, dstOffset: word, length: word): unit = 43 val wVecLength: vector -> word = LibrarySupport.Word8Array.wVecLength 46 (* Casts between int and word [all...] |
H A D | Word32.sml | 20 (* On 32-bit LargeWord has a 32-bit word length. *) 22 val () = if Word32.wordSize <> 32 then raise Fail "Not 32 bit word" else ();
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_coretypesScript.sml | 51 <| RFR : bool; NSASEDIS : bool; NSD32DIS : bool; cp : 14 word |>`; 141 `align (w : 'a word, n : num) : 'a word = n2w (n * (w2n w DIV n))`; 144 aligned (w : 'a word, n : num) = (w = align(w,n))`; 147 count_leading_zeroes (w : 'a word) = 154 lowest_set_bit (w : 'a word) = 184 signed_sat_q (i:int, N:num) : ('a word # bool) = 196 unsigned_sat_q (i:int, N:num) : ('a word # bool) = 211 LSL_C (x: 'a word, shift:num) = 219 LSR_C (x: 'a word, shif [all...] |
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_coretypesScript.sml | 51 <| RFR : bool; NSASEDIS : bool; NSD32DIS : bool; cp : 14 word |>`; 144 `align (w : 'a word, n : num) : 'a word = n2w (n * (w2n w DIV n))`; 147 aligned (w : 'a word, n : num) = (w = align(w,n))`; 150 count_leading_zeroes (w : 'a word) = 157 lowest_set_bit (w : 'a word) = 187 signed_sat_q (i:int, N:num) : ('a word # bool) = 199 unsigned_sat_q (i:int, N:num) : ('a word # bool) = 214 LSL_C (x: 'a word, shift:num) = 222 LSR_C (x: 'a word, shif [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | assemblerLib.sig | 12 val word: int -> string -> BitsN.nbit value
|
/seL4-l4v-master/seL4/include/arch/arm/arch/machine/ |
H A D | gic_v2.h | 130 int word = irq >> 4; local 132 return !!(gic_dist->config[word] & BIT(bit + 1)); 137 int word = IRQ_REG(irq); local 140 gic_dist->pending_clr[word] = BIT(bit); 145 int word = IRQ_REG(irq); local 148 gic_dist->enable_clr[word] = BIT(bit); 153 int word = IRQ_REG(irq); local 155 gic_dist->enable_set[word] = BIT(bit);
|
H A D | gic_v3.h | 175 int word = irq >> 4; local 184 icfgr = gic_dist->icfgrn[word]; 192 int word = IRQ_REG(irq); local 199 gic_dist->icpendrn[word] = BIT(bit); 205 int word = IRQ_REG(irq); local 211 gic_dist->icenablern[word] = BIT(bit); 218 int word = IRQ_REG(irq); local 224 gic_dist->isenablern[word] = BIT(bit);
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | notifications.tex | 14 A \obj{Notification} object contains a single data word, called the 15 \emph{notification word}. Such an object supports two operations: 30 notification word by bit-wise \texttt{or}-ing it with the \emph{badge} 39 select-style wait on the set of semaphores: If the notification word is 42 notification word to zero and returning to the invoker the previous 43 notification-word value. 46 no signals are pending (the notification word is 0) the call will return immediately
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | incn.ml | 72 ([],"!n w. WordVal n (w:^word) < 2 EXP (SUC n)"), 78 BOOL_CASES_TAC "(w:^word) 0" THEN 81 BOOL_CASES_TAC "(w:^word) (SUC n)" THENL 94 let th9 = MATCH_MP lemma2 (SPECL ["n";"(WordAbs (o t)):^word"] th6);; 95 let th10 = MATCH_MP lemma3 (SPECL ["n";"(WordAbs (o t)):^word"] th6);;
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | HolSmtScript.sml | 414 val _ = s ("r236", W ``(x :'a word) + y = y + x``) 417 (wordsLib.WORD_ARITH_CONV ``((x :'a word) + z = y + x) <=> (y = z)``)) 421 ((0w :'a word) @@ (n2w x :'b word) = (n2w x :'c word))``)) 424 ``x < dimword(:'a) ==> (w2w (n2w x :'a word) = (n2w x :'b word))``)) 428 (((0w :'a word) @@ (x :'b word) = (n2w y :'c word)) < [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Print.sig | 60 datatype word = Word of {word : string, size : int} type 62 val mkWord : string -> word 64 val emptyWord : word 66 val charWord : char -> word 68 val ppWord : word pp
|
H A D | Portable.sig | 37 val randomWord : unit -> Word.word
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | exportLib.sml | 172 (``word_1comp (x:'a word)``,"BWNot"), 173 (``word_add (x:'a word) y``,"Plus"), 174 (``word_sub (x:'a word) y``,"Minus"), 175 (``word_mul (x:'a word) y``,"Times"), 176 (``word_and (x:'a word) y``,"BWAnd"), 177 (``word_or (x:'a word) y``,"BWOr"), 178 (``word_xor (x:'a word) y``,"BWXOR"), 179 (``ShiftLeft (x:'a word) y``,"ShiftLeft"), 180 (``ShiftRight (x:'a word) y``,"ShiftRight"), 181 (``SignedShiftRight (x:'a word) [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sig | 60 datatype word = Word of {word : string, size : int} type 62 val mkWord : string -> word 64 val emptyWord : word 66 val charWord : char -> word 68 val ppWord : word pp
|
H A D | Portable.sig | 37 val randomWord : unit -> Word.word
|
/seL4-l4v-master/HOL4/examples/machine-code/multiword/ |
H A D | multiwordScript.sml | 51 (k2mw 0 n = []:('a word) list) /\ 56 (mw2n (x::xs) = w2n (x:'a word) + dimword (:'a) * mw2n xs)`; 63 n2mw n = if n = 0 then []:'a word list else 77 ``~(n = 0) ==> (n2mw n = (n2w (n MOD dimword (:'a)):'a word) :: 102 ``!k n. k2mw (SUC k) n = SNOC ((n2w (n DIV dimwords k (:'a))):'a word) (k2mw k n)``, 121 ``!k m. k2mw k (m MOD dimwords k (:'a)):('a word) list = k2mw k m``, 130 ``!xs ys. mw2n (xs ++ ys) = mw2n xs + dimwords (LENGTH xs) (:'a) * mw2n (ys:'a word list)``, 136 k2mw (k+l) (m MOD dimwords k (:'a) + dimwords k (:'a) * n) :('a word) list``, 164 ``!i m n. k2mw i (m MOD dimwords i (:'a) + n) = k2mw i (m + n) :('a word)list``, 172 ``!xs. mw2n xs < dimwords (LENGTH (xs:'a word lis [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | basic.sml | 14 (* Is the term a word? *) 20 (* Is the term a word or num literal? *) 59 (* Is the operator an arithmetic word operator? *) 78 (* Is the operator a word comparison operator? Includes equality *) 83 Lib.can (match_term (mk_const("=",``:'a word -> 'a word -> bool``))); 94 (* Is the operator a bitwise word operator? *) 105 (* Is the operator a bitwise word operator? *)
|
/seL4-l4v-master/seL4/src/arch/arm/ |
H A D | c_traps.c | 26 ksKernelEntry.word = getRegister(NODE_STATE(ksCurThread), NextIP); 72 ksKernelEntry.word = getRegister(NODE_STATE(ksCurThread), NextIP); 97 ksKernelEntry.word = IRQT_TO_IRQ(getActiveIRQ()); 112 /* ksKernelEntry.word word is already set to syscall */ 190 ksKernelEntry.word = hsr;
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | wordsLib.sml | 229 val err = ERR "word_EQ_CONV" "not a ground word equality" 316 `!n. w2n ((n2w n) : 'a word) = 321 `!n. word_2comp (n2w n) : 'a word = 327 `!n m. (n2w m : 'a word) << n = 358 word_join_def, Q.SPECL [`^n2w n`, `n2w m:'b word`] word_concat_def, 369 Q.SPECL [`w:'a word`, `^Na`] word_rol_def, word_rrx_n2w, 409 (``min$= : 'a word -> 'a word -> bool``, 2, word_EQ_CONV)] @ 568 evaluation of word expressions. 584 simpLib.named_merge_ss "word groun [all...] |