/seL4-l4v-master/seL4/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...] |
H A D | bitfield_gen.py | 46 # name of return value for standard word sizes 514 %(name)s_get_tag :: "%(name)s_C \<Rightarrow> word%(base)d" 738 '''((word%(base)d[%(words)d]) ptr))"''', 746 '''((word%(base)d[%(words)d]) ptr)) d"''', 1336 " is in a different word (%s) to the others (%s)." 1836 field_updates = {word: [] for word in range(self.multiple)} 2050 "Return a class mask for testing a whole word, i.e., one." 2052 "relevant word." 2223 "crosses a word boundar [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ByteCode/ |
H A D | INTCODECONSSIG.sml | 212 val genEqualWordConst: word * code -> unit
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/src/ |
H A D | riscv.spec | 32 type word = bits(32) 43 Word :: word 501 register FPCSR :: word -- 32-bit control register 1266 st_width :: word option -- width of store (optimization for sub-word store checks) 1294 inline unit recordStore(addr::vAddr, val::regType, width::word) = 1314 string hex32(x::word) = PadLeft(#"0", 8, [x]) 1393 string log_w_fprs(r::reg, data::word) = 1621 component FPRS(n::reg) :: word 1635 unit writeFPRS(rd::reg, val::word) [all...] |
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/ |
H A D | twofishScript.sml | 233 (* Function h takes two inputs--a 32-bit word X and a list L = (L0,...,Lk ) *) 234 (* (here k = 4) of 32-bit words of and produces one word of output. This *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/Examples/ |
H A D | mlEdit.sml | 105 (* The style does not include horizontal scrolling. That causes us to use word-wrapping. *) 341 the text, a line break, the last word break on the line
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/prog/ |
H A D | arm8_progLib.sml | 26 val word = wordsSyntax.mk_int_word_type 32 value 609 val map_tys = [word5, word, dword]
|
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
H A D | bitfield_gen.py | 46 # name of return value for standard word sizes 514 %(name)s_get_tag :: "%(name)s_C \<Rightarrow> word%(base)d" 738 '''((word%(base)d[%(words)d]) ptr))"''', 746 '''((word%(base)d[%(words)d]) ptr)) d"''', 1336 " is in a different word (%s) to the others (%s)." 1836 field_updates = {word: [] for word in range(self.multiple)} 2050 "Return a class mask for testing a whole word, i.e., one." 2052 "relevant word." 2223 "crosses a word boundar [all...] |
/seL4-l4v-master/seL4/tools/ |
H A D | bitfield_gen.py | 46 # name of return value for standard word sizes 514 %(name)s_get_tag :: "%(name)s_C \<Rightarrow> word%(base)d" 738 '''((word%(base)d[%(words)d]) ptr))"''', 746 '''((word%(base)d[%(words)d]) ptr)) d"''', 1336 " is in a different word (%s) to the others (%s)." 1836 field_updates = {word: [] for word in range(self.multiple)} 2050 "Return a class mask for testing a whole word, i.e., one." 2052 "relevant word." 2223 "crosses a word boundar [all...] |
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | windows_specific.cpp | 82 #define SIZEOF(x) (sizeof(x)/sizeof(word))
|
H A D | x86assembly_masm64.S | 228 lock xadd [rax],ecx ;# Rax is an absolute address but this is only a word
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BaseCodeTree.sml | 103 | TagTest of { test: codetree, tag: word, maxTag: word }
|
/seL4-l4v-master/isabelle/src/Pure/ |
H A D | build-jars | 81 src/Pure/General/word.scala
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ |
H A D | build-jars | 81 src/Pure/General/word.scala
|
/seL4-l4v-master/HOL4/examples/dev/sw2/test/ |
H A D | tea.sml | 26 (`!w:'a word. ~(w = 0w) ==> ?u. w = u + 1w`,
|
/seL4-l4v-master/HOL4/examples/formal-languages/ |
H A D | FormalLangScript.sml | 165 (* says that a word in A^n is either empty or can be split into k non-empty *)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
H A D | armAssemblerLib.sml | 230 val w = assemblerLib.word 32 s
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0AssemblerLib.sml | 18 val w16 = assemblerLib.word 16
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | ParseDatatype.sml | 89 "Expected an identifier, got (reserved word) \"of\""
|
H A D | Literal.sml | 281 (* There are other possible literals, e.g. for word[n]. This ref cell is *)
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | ParseDoc.sml | 271 raise ParseError "Multi-word \\STRUCTURE section"
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/prog/ |
H A D | x64_progLib.sml | 26 val word = wordsSyntax.mk_int_word_type 16 value
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | divideScript.sml | 75 (((n2w m):'a word) >>> n = n2w (m DIV (2 ** n)))``,
|
/seL4-l4v-master/HOL4/src/bool/ |
H A D | boolpp.sml | 282 "Invalid use of reserved word and") t1
|
/seL4-l4v-master/HOL4/tools/ |
H A D | holscript-mode.el | 163 (is-a-then (word-at-point)) 177 (or (is-a-then (word-at-point)) 195 ((let ((w (word-at-point))) 198 (- (cdr (bounds-of-thing-at-point 'word)) (point)) 222 ((let ((w (word-at-point))) 225 (- (cdr (bounds-of-thing-at-point 'word)) (point)) 872 ((equal 2 sc) ; word 883 ((equal 2 sc) ; word 1186 (defun word-before-point () 1189 (progn (backward-char 1) (word [all...] |