Searched refs:bits (Results 1 - 25 of 165) sorted by relevance

1234567

/seL4-l4v-10.1.1/l4v/tools/haskell-translator/
H A Dbraces.py32 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 Dpars_skl.py56 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 Dlhs_pars.py66 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 Dobjdump.py18 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 Dsyntax.py153 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 Dinst_logic.py33 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 Dloop_bounds.py373 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 DWord64.sml1 (* Only built if LargeWord is 64-bits *)
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/
H A Dmachine.h51 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 Dfastpath.h20 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 DdecoderScript.sml50 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 Dmicrocode.ml47 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 Dprob_pseudoScript.sml15 (* Theorems to allow pseudo-random bits to be computed. *)
/seL4-l4v-10.1.1/seL4/include/arch/riscv/arch/
H A Dmachine.h44 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 Dm0.sml517 {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 DWordOps.sml20 (* 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 DInterval.sml16 (* 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 Dx64.sml770 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 DBoolArray.sml22 (* 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 Dmips.sml1709 {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 DGdiBase.sml58 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 DLiteral.sml50 <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 Ddeprecated.h131 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 Darm.sml1771 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 Dbitmap.h33 // 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?

Completed in 141 milliseconds

1234567