/seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
H A D | braces.py | 32 def __init__(self, s, l, r, bits=None): 33 if bits is None: 34 bits = self._get_bits(s, l, r) 35 self.bits = bits 42 bits = [''] 46 if bits[-1]: 47 bits.append('') 49 bits[-1] = bits[ [all...] |
H A D | pars_skl.py | 56 bits = line.split() variable 58 call.filename = find_source(bits[1]) 59 call.all_bits = 'all_bits' in bits 60 call.decls_only = 'decls_only' in bits 61 call.instanceproofs = 'instanceproofs' in bits 62 call.bodies_only = 'bodies_only' in bits 64 for bit in bits if '=' in bit]) 66 if 'CONTEXT' in bits: 67 n = bits.index('CONTEXT') 68 call.current_context.append(bits[ [all...] |
H A D | lhs_pars.py | 66 bits = l.split (',') 67 for bit in bits: 483 bits = string.split('=>', 1) 484 if len(bits) == 2: 485 lhs = bits[0].strip() 488 string = ' => '.join(instances + [bits[1]]) 503 transformed = type_transform(bits[1]) 518 bits = bstring.split('->') 520 if len(bits) == 1: 521 bits [all...] |
/seL4-l4v-10.1.1/graph-refine/ |
H A D | objdump.py | 18 bits = line.split () 20 addr = int (bits[0], 16) 21 size = int (bits[-2], 16) 22 section = bits[-3] 23 syms[bits[-1]] = (addr, size, section) 80 bits = line.split () 81 (addr, v) = (int (bits[0][:-1], 16), int (bits[1], 16)) 116 bits = lname.split () 117 assert bits[ [all...] |
H A D | syntax.py | 153 These types encode a machine word with the given number of bits, an array of 419 bits = [repr(self.kind), repr(self.typ)] 420 bits.extend(['%s = %r' % b for b in self.binds()]) 421 return 'Expr (%s)' % ', '.join(bits) 920 def parse_typ(bits, n, symbolic_types = False): 921 if bits[n] == 'Word' or bits[n] == 'BitVec': 922 return (n + 2, Type('Word', parse_int (bits[n + 1]))) 923 elif bits[n] == 'WordArray' or bits[ [all...] |
H A D | inst_logic.py | 33 bits = inst_split_re.split (nm) 36 if len (bits) > 1 and pn_re.match (bits[1]): 37 bits[1] = bits[1][1:] 38 for bit in bits: 115 bits = instname.split('_') 116 assert bits, instname 117 addr = bits[-1] 120 return ('_'.join (bits[ [all...] |
H A D | loop_bounds.py | 373 def parse_ctxt_id (bits, n): 374 return (n + 1, syntax.parse_int (bits[n])) 376 def parse_ctxt (bits, n): 377 return syntax.parse_list (parse_ctxt_id, bits, n) 388 bits = l.split () 389 if bits[:1] not in [['LoopBound'], ['GlobalLoopBound']]: 391 (n, (addr, bound)) = parse_bound (bits, 1) 392 (n, ctxt) = parse_ctxt (bits, n) 393 prob_hash = parse_int (bits[n]) 395 if bits[ [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
H A D | Word64.sml | 1 (* Only built if LargeWord is 64-bits *)
|
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/ |
H A D | machine.h | 51 static inline void clearMemory(word_t* ptr, word_t bits) argument 53 memzero(ptr, BIT(bits)); 54 cleanCacheRange_PoU((word_t)ptr, (word_t)ptr + BIT(bits) - 1, 58 static inline void clearMemoryRAM(word_t* ptr, word_t bits) argument 60 memzero(ptr, BIT(bits)); 61 cleanCacheRange_RAM((word_t)ptr, (word_t)ptr + BIT(bits) - 1,
|
/seL4-l4v-10.1.1/seL4/include/fastpath/ |
H A D | fastpath.h | 20 word_t guardBits, radixBits, bits; local 23 bits = 0; 32 cptr2 = cptr << bits; 48 bits += guardBits + radixBits; 50 } while (unlikely(bits < wordBits && cap_capType_equals(cap, cap_cnode_cap))); 52 if (unlikely(bits > wordBits)) { 53 /* Depth mismatch. We've overshot wordBits bits. The lookup we've done is
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/common/ |
H A D | decoderScript.sml | 50 assign name x (g:string->bool list, bits:bool list) = SOME ((name =+ x) g,bits)`; 53 assign_drop name i (g:string->bool list, bits:bool list) = 54 if LENGTH bits < i then NONE else SOME ((name =+ TAKE i bits) g, DROP i bits)`; 57 drop_eq v (g:string->bool list, bits:bool list) = 59 if LENGTH bits < i \/ ~(v = TAKE i bits) then NONE else SOME (g, DROP i bits)`; [all...] |
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | microcode.ml | 47 mk_ADDR [b4;b3;b2;b1;b0] n gives a list of the positions of bits that 61 mk_A_ADDR n gives a list of the positions of bits in the A-address 64 mk_B_ADDR n gives a list of the positions of bits in the B-address 72 test_button(n,m) gives a list of the bits that are 1 if the address of the 80 test_acc(n,m) gives a list of the bits that are 1 if the address of the 88 jump n gives a list of the bits that are 1 if the address of the 95 jump_knob n gives a list of the bits that are 1 if the address of the 103 jump_opcode n gives a list of the bits that are 1 if the address of the 113 mk_micro_ins l takes a list of numbers representing the positions of bits 116 appropriate bits o [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_pseudoScript.sml | 15 (* Theorems to allow pseudo-random bits to be computed. *)
|
/seL4-l4v-10.1.1/seL4/include/arch/riscv/arch/ |
H A D | machine.h | 44 static inline void clearMemory(void* ptr, unsigned int bits) argument 46 memzero(ptr, BIT(bits));
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0.sml | 517 {PM = BitsN.bit(x,0), primask'rst = BitsN.bits(31,1) x}; 529 {C = BitsN.bit(x,29), ExceptionNumber = BitsN.bits(5,0) x, 532 psr'rst = BitsN.@@(BitsN.bits(23,6) x,BitsN.bits(27,25) x)}; 540 BitsN.bits(2,0) psr'rst,BitsN.fromBit T, 541 BitsN.bits(20,3) psr'rst,ExceptionNumber]; 564 VECTCLRACTIVE = BitsN.bit(x,1), VECTKEY = BitsN.bits(31,16) x, 565 aircr'rst = BitsN.@@(BitsN.bits(0,0) x,BitsN.bits(14,3) x)}; 573 [VECTKEY,BitsN.fromBit ENDIANNESS,BitsN.bits(1 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | WordOps.sml | 20 (* Clear top (all but rightmost width) bits in w *) 46 let fun fus bits = 47 let val N = IntInf.pow(2,bits-1) 48 in if ~N <= n andalso n <= N-1 then bits else fus (bits+1)
|
H A D | Interval.sml | 16 (* where the b1...bn occupy width bits and int_cat i1 width i2 returns a *) 61 (* Width of an interval (in bytes and bits) *)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64.sml | 770 PM = BitsN.bit(x,12), RC = BitsN.bits(14,13) x, 771 Reserved = BitsN.bits(31,16) x, UE = BitsN.bit(x,4), 797 ( write'mem8(BitsN.bits(7,0) w,addr) 801 write'mem8(BitsN.bits(15,8) w,x) 809 ( write'mem16(BitsN.bits(15,0) w,addr) 813 write'mem16(BitsN.bits(31,16) w,x) 821 ( write'mem32(BitsN.bits(31,0) w,addr) 825 write'mem32(BitsN.bits(63,32) w,x) 833 ( write'mem64(BitsN.bits(63,0) w,addr) 837 write'mem64(BitsN.bits(12 [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | BoolArray.sml | 22 (* TODO: Use a single word for vectors of size <= number of bits in a word. *) 23 (* We use int here for the length rather than word because the number of bits 43 fun alloc (bits: int) = 46 if bits < 0 orelse bits > maxLen 48 else (Word.fromInt bits + (bitsPerWord - 0w1)) div bitsPerWord 55 (* We will only set the bits that we actually use. Unused bytes will be uninitialised. 106 (* Accumulate the bits into bytes and store into the array. *) 137 (* Move a set of bits from one vector of bytes to another. The bits [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mips.sml | 1709 {Index = BitsN.bits(7,0) x, P = BitsN.bit(x,31), 1710 index'rst = BitsN.bits(30,8) x}; 1722 {Random = BitsN.bits(7,0) x, random'rst = BitsN.bits(31,8) x}; 1734 {Wired = BitsN.bits(7,0) x, wired'rst = BitsN.bits(31,8) x}; 1745 {C = BitsN.bits(5,3) x, D = BitsN.bit(x,2), G = BitsN.bit(x,0), 1746 PFN = BitsN.bits(33,6) x, V = BitsN.bit(x,1), 1747 entrylo'rst = BitsN.bits(63,34) x}; 1761 {Mask = BitsN.bits(2 [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | GdiBase.sml | 58 bits: Word8Vector.vector option } 64 fun storeBmp(v: voidStar, {width, height, widthBytes, planes, bitsPerPixel, bits}: BITMAP) = 66 val m = case bits of NONE => Memory.null | SOME b => toCWord8vec b 74 val (_, width, height, widthBytes, planes, bitsPerPixel, bits) = 76 val bits = value 77 if bits = Memory.null 79 else SOME (fromCWord8vec (bits, height * widthBytes)) 82 bitsPerPixel = bitsPerPixel, bits = bits}
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Literal.sml | 50 <numeral> ::= 0 | NUMERAL <bits> 51 <bits> ::= ZERO | BIT1 (<bits>) | BIT2 (<bits>) 98 <relaxed_numeral> ::= 0 | NUMERAL <bits> | <bits> 99 <bits> ::= ZERO | BIT1 (<bits>) | BIT2 (<bits>)
|
/seL4-l4v-10.1.1/seL4/libsel4/include/sel4/ |
H A D | deprecated.h | 131 static inline SEL4_DEPRECATED("Use seL4_CNode_CapData_new().words[0]") seL4_Word seL4_CapData_Guard_new(seL4_Word guard, seL4_Word bits) argument 133 return seL4_CNode_CapData_new(guard, bits).words[0];
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
H A D | arm.sml | 1771 F = BitsN.bit(x,6), GE = BitsN.bits(19,16) x, I = BitsN.bit(x,7), 1772 IT = BitsN.@@(BitsN.bits(15,10) x,BitsN.bits(26,25) x), 1773 J = BitsN.bit(x,24), M = BitsN.bits(4,0) x, N = BitsN.bit(x,31), 1775 Z = BitsN.bit(x,30), psr'rst = BitsN.bits(23,20) x}; 1783 BitsN.fromBit Q,BitsN.bits(1,0) IT,BitsN.fromBit J,psr'rst,GE, 1784 BitsN.bits(7,2) IT,BitsN.fromBit E,BitsN.fromBit A, 1800 [BitsN.bits(6,3) x,BitsN.bits(9,8) x,BitsN.bits(1 [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | bitmap.h | 33 // Allocate the bitmap bits 34 bool Create(POLYUNSIGNED bits); 36 // Free the bitmap bits. 48 // Set a range of bits 50 // Clear a range of bits. May already be partly clear 51 // N.B. This may clear more than just the bits specified 55 // How many zero bits (maximum n) are there in the bitmap, starting at location start? 59 // How many set bits are there in the bitmap?
|