Searched refs:word (Results 201 - 225 of 347) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/HolSmt/
H A Dselftest.sml761 (* 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 DYices.sml14 - 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 DImport.sml439 (* 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 Dvsynth.sml85 (* 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 DSERE.ml24 (* 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 Dgraph_specsLib.sml38 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 Dfile_readerLib.sml104 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 DCommonDialog.sml467 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 DCommonControls.sml155 type flags = Word8.word
254 type flags = SysWord.word
H A DClass.sml95 type flags = Word32.word
/seL4-l4v-master/HOL4/src/emit/
H A Dextended_emitScript.sml357 :: MLSIG "type 'a word = 'a wordsML.word"
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DBinaryset.sml56 * 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 Dbreakpoint.c592 ksKernelEntry.word = int_vector;
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/
H A Darm_stepLib.sml65 ``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 DX86FOREIGNCALL.sml367 (* 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 Dcomputer_imp.ml178 % 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 Darm8AssemblerLib.sml192 val w = assemblerLib.word 32 s
/seL4-l4v-master/HOL4/Manual/LaTeX/
H A Dack.tex39 documented new word theories and the associated libraries; Mike
/seL4-l4v-master/HOL4/developers/discussion/
H A Doverloading-extension.tex112 \texttt{:real}, \texttt{:int} and \texttt{:word}). Rather than have
/seL4-l4v-master/HOL4/examples/Crypto/TEA/
H A DteaScript.sml32 (`!w:'a word. ~(w = 0w) ==> ?u. w = u + 1w`,
/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/
H A DClockedSemanticsScript.sml5 (* 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 Dset_sepScript.sml36 (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 DASN1.sml40 val readHeader: (Word8.word, 'a) StringCvt.reader -> ((tagType * int), 'a) StringCvt.reader
H A DTime.sml53 uses a 64-bit number of 100ns ticks, Unix uses one word of seconds
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/
H A Dsyscall_stub_gen.py47 # 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...]

Completed in 201 milliseconds

1234567891011>>