/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | selftest.sml | 761 (* Yices does not support shifting by more than the word length *) 975 (``!(w: 18 word). (sw2sw w): 32 word = w2w ((16 >< 0) w: 17 word) + 976 0xfffe0000w + ((0 >< 0) (~(17 >< 17) w: bool[unit]) << 17): 32 word``,
|
H A D | Yices.sml | 14 - types: 'bool', 'num', 'int', 'real', 'fun', 'prod', word types, data 20 various word operations, data type constructors, data type case 323 (* word literals *) 329 "word literal: bit-vector type of unknown size")
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | Import.sml | 439 (* Sub-word extract *) 741 val mk_word_min = mk_uncurry ``\(m:'a word, n). words$word_min m n`` 742 val mk_word_max = mk_uncurry ``\(m:'a word, n). words$word_max m n`` 743 val mk_word_smin = mk_uncurry ``\(m:'a word, n). words$word_smin m n`` 744 val mk_word_smax = mk_uncurry ``\(m:'a word, n). words$word_smax m n``
|
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | vsynth.sml | 85 (* Test if a ty is ``:word<n>`` for some n *) 91 (* Extraxt <n> from ``:word<n>`` *) 99 (* Currently this means the type is ``:word<n>``, ``:num`` or ``:bool`` *)
|
/seL4-l4v-master/HOL4/examples/PSL/experimental-semantics/ |
H A D | SERE.ml | 24 (* we let \epsilon be the empty (neutral) word *) 160 (* The problem with fusion is that if w is a weak word that matches *) 332 (* Weaken a word *)
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | graph_specsLib.sml | 38 val var_word = mk_const("VarWord",``: ^ty word -> ^ty variable``) 39 val var_mem = mk_const("VarMem",``: (^ty word -> word8) -> ^ty variable``) 270 (false,mk_comb(mk_const("Jump",``:^(tysize()) word -> ^(tysize()) jump``),
|
H A D | file_readerLib.sml | 104 val s2 = if String.isPrefix ".word" s3 then "const:" ^ s2 else s2 312 fun wsize () = ``:^(tysize ()) word``;
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | CommonDialog.sml | 467 type flags = word 845 type flags = word 913 type flags = word 1234 type flags = SysWord.word 1294 type flags = SysWord.word 1415 type flags = SysWord.word
|
H A D | CommonControls.sml | 155 type flags = Word8.word 254 type flags = SysWord.word
|
H A D | Class.sml | 95 type flags = Word32.word
|
/seL4-l4v-master/HOL4/src/emit/ |
H A D | extended_emitScript.sml | 357 :: MLSIG "type 'a word = 'a wordsML.word"
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Binaryset.sml | 56 * T(v,ln+rn+1,l,r). The poor code allocates a 16 word vector 59 * word T node. The values that it retrieves were live in
|
/seL4-l4v-master/seL4/src/arch/x86/machine/ |
H A D | breakpoint.c | 592 ksKernelEntry.word = int_vector;
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_stepLib.sml | 65 ``IncPC ()``, ``PSR_IT``, ``(h >< l) : 'a word -> 'b word``] @ 590 : arm_state -> ('a word # bool) # arm_state`` 601 ``(if n = 0 then (x: 'a word,s) else (x #>> n, ^st)) = (x #>> n, s)`` 605 ``ROR (x: 'a word, n)`` 727 GSYM (Q.ISPEC `MemA x s : 'a word # arm_state` pairTheory.PAIR) 976 ``(a: 'a word - 4w * b + 4w + 4w * c = a + 4w * (c - b + 1w)) /\ 1334 ``aligned c (a + b : 'a word)`` 3267 [``Extend (T, w:'a word): 'b word``, [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 367 (* RTS call with one general (i.e. ML word) argument and a floating point result. 385 (* RTS call with one general (i.e. ML word) argument and a floating point result. 424 (* Code to box an address as a SysWord.word value *) 466 withtype cType = { typeForm: cTypeForm, align: word, size: word } 503 | (CTypeFloatingPt, 0w8) =>(* Double: push the two words. High-order word first, then low-order. *) 622 (* Double: copy the two words. High-order word first, then low-order. *) 629 | _ => (* Everything else is a single word on the stack. *) 931 (* The entry point is in a SysWord.word value in RAX. *) 1431 (* The entry point is in a SysWord.word valu [all...] |
/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/ |
H A D | computer_imp.ml | 178 % microcode such that the 'A_ADDR' field of word 1 is 2 instead of 1. %
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8AssemblerLib.sml | 192 val w = assemblerLib.word 32 s
|
/seL4-l4v-master/HOL4/Manual/LaTeX/ |
H A D | ack.tex | 39 documented new word theories and the associated libraries; Mike
|
/seL4-l4v-master/HOL4/developers/discussion/ |
H A D | overloading-extension.tex | 112 \texttt{:real}, \texttt{:int} and \texttt{:word}). Rather than have
|
/seL4-l4v-master/HOL4/examples/Crypto/TEA/ |
H A D | teaScript.sml | 32 (`!w:'a word. ~(w = 0w) ==> ?u. w = u + 1w`,
|
/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | ClockedSemanticsScript.sml | 5 (* where w is a finite or infinite word i.e. w : ('prop -> bool)path *)
|
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | set_sepScript.sml | 36 (SEP_ARRAY p i a (x::xs) = p a x * SEP_ARRAY p i (a + i:'a word) xs)`;
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | ASN1.sml | 40 val readHeader: (Word8.word, 'a) StringCvt.reader -> ((tagType * int), 'a) StringCvt.reader
|
H A D | Time.sml | 53 uses a 64-bit number of 100ns ticks, Unix uses one word of seconds
|
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
H A D | syscall_stub_gen.py | 47 # Number of bits in a standard word 139 Return code for a C expression that gets word 'word_num' 408 # We need everything to be a power of two, or word sized. 411 # Align up to our own size, or the next word. (Whichever is smaller) 440 We return a list of expressions; one expression per word required 458 # double word type 466 # Single full word? 473 # Part of a word? 510 in them, indicating a read from a word in the message. 758 for word i [all...] |