/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | arm_improved_gcScript.sml | 106 (ref_heap_addr (H_DATA w) = n2w (w2n (w:31 word) * 2 + 1)) /\ 177 !(a:num) l (xs:(31 word) heap_address list) b:word8 t:bool ys:word32 list.
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_invScript.sml | 69 set_add a x (b,s) <=> (b - (a:'a word), s) IN x 703 (((n2w m):'a word) >>> n = n2w (m DIV (2 ** n)))``,
|
/seL4-l4v-master/l4v/misc/vim/ |
H A D | isabelle.vim | 703 " Tweak the things that Vim sees as part of a word. This is useful if you 704 " have macros that kick in on word completion or similar.
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_invScript.sml | 430 ``!w v. (w2w (w:29 word) << 3 !! 3w = w2w v << 3 !! 3w:word32) = (w = v)``, 440 (let (x0,w0) = (Sym s, w2w (w:29 word) << 3 !! 3w) in ^LISP) /\ 441 (((w2w w0):word64 = w2w (w:29 word) << 3 !! 3w) = (x0 = Sym s))``, 911 ``w2n (j:29 word) < LENGTH xs ==> ^LISP ==> 961 ``w2n (j:29 word) < LENGTH xs ==> ^LISP ==>
|
H A D | lisp_codegenScript.sml | 956 (w2w (w2w (v:29 word) << 3 + 0x3w:word32) = w2w v << 3 + 0x3w:word64) /\ 1087 \\ `w2w ((n2w k):29 word) = (n2w k):word64` by 1911 ``(w2w:word32->word64) (w2w (w:30 word) << 2 !! 1w) >>> 2 = w2w w``
|
H A D | lisp_opsScript.sml | 1802 ``!j. n2w (SIGN_EXTEND 32 64 (w2n ((0x4w:word32) * w2w (j:29 word)))) = 1818 val th = Q.INST [`imm32`|->`4w*w2w (j:29 word)`] th 1824 val post_tm = set_pc th ``zLISP ^STAT (EL (w2n (j:29 word)) xs,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1837 val th = Q.INST [`imm32`|->`4w*w2w (j:29 word)`] th 1843 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,UPDATE_NTH (w2n (j:29 word)) x0 xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 2554 val lemma = GSYM (SIMP_CONV std_ss [WORD_LOWER_OR_EQ] ``~(x <=+ y:'a word)``)
|
/seL4-l4v-master/HOL4/examples/elliptic/swsep/ |
H A D | swsepScript.sml | 113 `(MREG2REG reg = (n2w (index_of_reg reg)):4 word)` 1987 ``(UNIV:'a word -> bool) = 1998 ``FINITE (UNIV:'a word -> bool)``,
|
/seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
H A D | decompilerLib.sml | 193 else if can (match_term ``(f ((n2w n):'a word) (x:'c)):'d``) tm then 397 val pattern = inst [``:'a``|->aa] ``(p:'a word) + n2w n`` 1578 ``(p:'a word) + n2w n``)
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | threads.tex | 560 message containing the scheduling context data word, as well as the amount of 568 \textbf{Meaning} & \textbf{IPC buffer location} \\ \midrule Data word from
|
H A D | cspace.tex | 477 occurred. The description format is explained below. The first word
|
H A D | objects.tex | 306 is a word-size array of flags, each of which behaves like a binary semaphore. Operations
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 401 These lists use white-space as element separators. If a word needs to 509 words, and then transforms each word by attempting to see if it 510 matches the pattern in \texttt{arg1}. If so, it replaces that word 511 with \texttt{arg2} (suitably instantiated). If not, the word is
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | instructionSyntax.sml | 411 raise ERR "index_mod_size" "unknown word size"
|
/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | PropertiesScript.sml | 123 * (i is the first rising edge after j of clock c in word w)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 43 type priority = Word.word;
|
H A D | Map.sml | 35 type priority = Word.word;
|
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_codegenScript.sml | 106 val tms = find_terml (can (match_term ``n2w (ORD c):'a word``)) tm
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 43 type priority = Word.word;
|
H A D | Map.sml | 35 type priority = Word.word;
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | user_lemma_instructionsScript.sml | 691 (* byte reverse word *)
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | misc.tex | 432 These lists use white-space as element separators. If a word needs to 558 words, and then transforms each word by attempting to see if it 559 matches the pattern in \texttt{arg1}. If so, it replaces that word 560 with \texttt{arg2} (suitably instantiated). If not, the word is
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_FUNCTIONS.sml | 41 val F_mutable_words : Word8.word = Word8.orb (F_words, F_mutable)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mips.sml | 4276 val word = BitsN.??(BitsN.bits(2,2) vAddr,BigEndianCPU ()) value 4278 case (word,byte) of 4328 val word = BitsN.??(BitsN.bits(2,2) vAddr,BigEndianCPU ()) value 4330 case (word,byte) of 4516 val word = BitsN.??(BitsN.bits(2,2) vAddr,BigEndianCPU ()) value 4529 if word = (BitsN.B(0x1,1)) 4548 val word = BitsN.??(BitsN.bits(2,2) vAddr,BigEndianCPU ()) value 4550 case (word,byte) of 12764 | "word" =>
|
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | arm_compiler_demoScript.sml | 63 i over natural numbers (<32) and w over 8-bit word constants.
|
/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/ |
H A D | coreScript.sml | 90 (* Memory access on next cycle: Byte (F) or word (T) *)
|