Searched refs:word (Results 301 - 325 of 347) sorted by relevance

<<11121314

/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/
H A Darm_improved_gcScript.sml106 (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 Dlisp_invScript.sml69 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 Disabelle.vim703 " 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 Dlisp_invScript.sml430 ``!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 Dlisp_codegenScript.sml956 (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 Dlisp_opsScript.sml1802 ``!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 DswsepScript.sml113 `(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 DdecompilerLib.sml193 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 Dthreads.tex560 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 Dcspace.tex477 occurred. The description format is explained below. The first word
H A Dobjects.tex306 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 Dmisc.tex401 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 DinstructionSyntax.sml411 raise ERR "index_mod_size" "unknown word size"
/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/
H A DPropertiesScript.sml123 * (i is the first rising edge after j of clock c in word w)
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml43 type priority = Word.word;
H A DMap.sml35 type priority = Word.word;
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/
H A Djit_codegenScript.sml106 val tms = find_terml (can (match_term ``n2w (ORD c):'a word``)) tm
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml43 type priority = Word.word;
H A DMap.sml35 type priority = Word.word;
/seL4-l4v-master/HOL4/examples/ARM_security_properties/
H A Duser_lemma_instructionsScript.sml691 (* byte reverse word *)
/seL4-l4v-master/HOL4/Manual/Description/
H A Dmisc.tex432 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 DCODETREE_FUNCTIONS.sml41 val F_mutable_words : Word8.word = Word8.orb (F_words, F_mutable)
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/model/
H A Dmips.sml4276 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 Darm_compiler_demoScript.sml63 i over natural numbers (<32) and w over 8-bit word constants.
/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/
H A DcoreScript.sml90 (* Memory access on next cycle: Byte (F) or word (T) *)

Completed in 595 milliseconds

<<11121314