/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | io.tex | 153 PCI identifier of the device as the low 16 bits of the \texttt{badge} argument, and 154 a Domain ID as the high 16 bits of the \texttt{badge} argument. 157 a 16-bit quantity. The first 8 bits identify the bus that the device is on. 158 The next 5 bits are the device identifier: the number of the device on 159 the bus. The last 3 bits are the function number. A single device may
|
H A D | vspace.tex | 40 The size and type of structure at each level, and the number of bits in the virtual address resolved 65 Structures at both levels are indexed by 10 bits in the virtual address. 77 defined, as shown in the table below. All structures are indexed with 9 bits of the virtual 108 \texttt{PageGlobalDirectory}. All paging structures are index by 9 bits of the virtual address. 126 32-bit RISC-V \texttt{PageTables} are indexed by 10 bits of virtual address. 137 64-bit RISC-V follows the SV39 model, where \texttt{PageTables} are indexed by 9 bits of virtual address.
|
H A D | ipc.tex | 69 \ipcparam{seL4\_Word}{}{receiveDepth}{Number of bits of 132 Only the low 28 bits of the badge are available for use. The kernel will 133 silently ignore any usage of the high 4 bits. 151 These fields specify the root CNode, capability address and number of bits to resolve, respectively, to find
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8.sml | 918 tcr_el1'rst = BitsN.@@(BitsN.bits(36,0) x,BitsN.bits(63,39) x)}; 924 [BitsN.bits(24,0) tcr_el1'rst,BitsN.fromBit TBI1, 925 BitsN.fromBit TBI0,BitsN.bits(61,25) tcr_el1'rst]; 933 tcr_el2_el3'rst = BitsN.@@(BitsN.bits(19,0) x,BitsN.bits(31,21) x)}; 939 [BitsN.bits(10,0) tcr_el2_el3'rst,BitsN.fromBit TBI, 940 BitsN.bits(30,11) tcr_el2_el3'rst]; 951 [BitsN.bits(0,0) x,BitsN.bits( [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
H A D | Bitstring.sml | 158 fun bits (h, l) = function 167 fun bit (a, n) = bits (n, n) a = [true]
|
H A D | BitsN.sml | 61 else raise Fail ("Tried to resize bits(" ^ Nat.toString j ^ 62 ") to bits(" ^ Int.toString i ^ ")") 76 fun bits (h, l) = function
|
H A D | BitsN.sig | 69 val bits: Nat.nat * Nat.nat -> nbit -> nbit value
|
H A D | FP64.sml | 21 val byte = Word8.fromLargeInt o BitsN.toNat o L3.uncurry BitsN.bits
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/MARS/ |
H A D | MARS_keyExpansionScript.sml | 142 (* Record the two lowest bits of K[i], by setting j = K[i] & 3, and then 143 consider the word with these two bits set to 1, w = K[i] | 3 *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | dataabs.ml | 5 % logic to boolean logic for single bits and for %
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0AssemblerLib.sml | 17 fun hex32 w = hex (BitsN.bits (31, 16) w) ^ " " ^ hex (BitsN.bits (15, 0) w) 195 if BitsN.toNat (BitsN.bits (15, 12) opc) = 13 197 val code = BitsN.bits (11, 8) opc
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/curried/ |
H A D | word8Script.sml | 11 (* 8 bits per byte, represented as an 8-tuple of truth values. *) 26 (* variables, or as 256 tuples of bits. The former is useful for symbolic *) 197 Compare bits and bytes as if they were numbers. Not currently used
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Word8.sml | 33 that the top 22/23 bits are always zero and mask them after every 35 we could allow these bits to be undefined and mask them before any 53 (* Not the same as Word.notb because it only affects the bottom 8 bits. *)
|
H A D | Int32.sml | 28 open LargeInt (* We need LargeInt on 32-bits. *)
|
H A D | ASN1.sml | 102 (* The type is encoded in the top two bits of the first byte. *) 112 (* The tag is the bottom five bits except that if it is 0x1f
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | logic.py | 370 def split_out_cast (expr, target_typ, bits): 373 have the property that expr' && mask bits = cast expr, 375 bottom n bits, e.g. (1 << n) - 1, and cast is WordCast.""" 378 if x.typ.num >= bits and expr.typ.num >= bits: 379 return split_out_cast (x, target_typ, bits) 388 full_mask = (1 << bits) - 1 390 return split_out_cast (x, target_typ, bits) 395 # at a smaller number of bits than we'll eventually report 396 if expr.typ.num >= bits [all...] |
H A D | pseudo_compile.py | 434 bits = s.split ('.') 435 if len (bits) != 2: 437 if all ([x in '0123456789' for x in bits[1]]): 438 return bits[0]
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Base.sml | 302 (* Int should be 32-bits on Windows. *) 304 orelse raise Fail "unsigned int is not 32-bits" 307 orelse raise Fail "unsigned long is not 32-bits" 561 able to handle multiple bits. Patterns with more than one bit set 562 MUST be placed later than those with a subset of those bits. *) 574 bit entries preceded those with fewer bits but it's much easier to lay 583 | fromInt [] (SOME(res, bits)) x = (* Found something - remove it from the set. *) 584 (res :: fromInt table NONE (andb(x, notb bits))) 586 | fromInt ((res, bits)::tl) sofar x = 587 if bits <> [all...] |
H A D | Menu.sml | 334 (* The options are the other bits in the type field. *) 350 val (bits, typeData, cch, bmp) = value 357 val mtype = Word32.orb(fromMFT menuOptions, bits) 371 val (bits, typeData, cch, bmp) = value 378 val mtype = Word32.orb(fromMFT menuOptions, bits)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
H A D | armAssemblerLib.sml | 231 val c = BitsN.bits (31, 28) w 350 (BitsN.bits (3, 2) opc = BitsN.fromNat (2, 2) orelse d = d') 359 val c = BitsN.bits (31, 28) w
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | div.ml | 4 % The following bits are needed to make this proof run in HOL88. %
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/ |
H A D | amba_apbScript.sml | 16 (* note: psel_x is a family signals, where x identifies the slave, so the x is not bits e.g. psel_2 is a valid signal *)
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/ |
H A D | machine.h | 295 static inline void clearMemory(void* ptr, unsigned int bits) argument 297 memzero(ptr, BIT(bits));
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | MD5.sml | 121 val bits = packLittle [lo,hi] value 125 val {digest= {A,B,C,D},...} = update (state,bits)
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/ |
H A D | teaScript.sml | 6 (* causes all bits of the key and data to be mixed repeatedly.The number of *) 9 (* authors suggest 32. The key is set at 128 bits. *)
|