/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Subst.sml | 48 fun shift (0, s) = s function 49 | shift (k, Shift(k',s)) = shift(k+k', s) 50 | shift (k, s) = Shift(k,s) 90 * Cons(shift k (s o s'), mk_cl (Shift(k,s)) x) 91 * or shift k (Cons (s o s', mk_cl s x)) <-- was prefered 97 | (Shift(k,s)) o s' = shift(k, s o s') 99 | (Cons(s,x)) o (Shift(k,s')) = s o shift(k-1, s') 102 then shift(k, s o shift( [all...] |
H A D | Subst.sig | 7 val shift : int * 'a subs -> 'a subs value
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | parse_struct_array.c | 68 int ts20110511_1(struct s *sptr, int i, int shift) argument 70 return ((sptr->data[i]) >> shift); 73 int ts20110511_2(struct s *sptr, int shift) argument 75 return ((sptr->sz) >> shift);
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/ |
H A D | regexMarkedScript.sml | 57 (shift _ (MEps) _ = MEps ) /\ 58 (shift m (MSym _ x) c = MSym (m /\ (x = c)) x ) /\ 59 (shift m (MAlt p q) c = MAlt (shift m p c) (shift m q c) ) /\ 60 (shift m (MSeq p q) c = MSeq (shift m p c) (shift ((m /\ (empty p)) \/ final p) q c)) /\ 61 (shift m (MRep r) c = MRep (shift ( [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_coretypesScript.sml | 212 LSL_C (x: 'a word, shift:num) = 213 if shift = 0 then 216 let extended_x = w2n x * (2 ** shift) in 217 (x << shift, BIT (dimindex(:'a)) extended_x)`; 220 LSR_C (x: 'a word, shift:num) = 221 if shift = 0 then 224 (x >>> shift, BIT (shift - 1) (w2n x))`; 227 ASR_C (x: 'a word, shift:num) = 228 if shift [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_coretypesScript.sml | 216 LSL_C (x: 'a word, shift:num) = 217 if shift = 0 then 220 let extended_x = w2n x * (2 ** shift) in 221 (x << shift, BIT (dimindex(:'a)) extended_x)`; 224 LSR_C (x: 'a word, shift:num) = 225 if shift = 0 then 228 (x >>> shift, BIT (shift - 1) (w2n x))`; 231 ASR_C (x: 'a word, shift:num) = 232 if shift [all...] |
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/kernel/ |
H A D | tlb_bitmap.h | 57 int shift = i * TLBBITMAP_ENTRIES_PER_ROOT; 58 bitmap |= entry << shift;
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | optScript.sml | 49 (shift skip (Lit l) = Lit l) ��� 50 (shift skip (Var n) = 55 (shift skip (Fun e) = Fun (shift (skip + 1) e)) ��� 56 (shift skip (App e1 e2) = App (shift skip e1) (shift skip e2)) ��� 57 (shift skip (Tick e) = Tick (shift skip e))`; 68 (subst skip e2 (Fun e1) = Fun (subst (skip + 1) (shift [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | Interval.sml | 20 fun int_cat w shift i = 21 let val shiftw = Word.fromInt shift 23 val x = clear_top_bits shift i
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | text.scala | 184 def can_edit(string: String, shift: Offset): Boolean = 185 shift <= start && start < shift + string.length 187 def edit(string: String, shift: Offset): (Option[Edit], String) = 188 if (!can_edit(string, shift)) (Some(this), string) 189 else if (is_insert) (None, insert(start - shift, string)) 191 val i = start - shift
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | text.scala | 184 def can_edit(string: String, shift: Offset): Boolean = 185 shift <= start && start < shift + string.length 187 def edit(string: String, shift: Offset): (Option[Edit], String) = 188 if (!can_edit(string, shift)) (Some(this), string) 189 else if (is_insert) (None, insert(start - shift, string)) 191 val i = start - shift
|
/seL4-l4v-10.1.1/HOL4/examples/misc/ |
H A D | contMonadScript.sml | 75 shift f = Cont (runC o f) 81 (a,b) <- reset (do x <- shift (��k. return (3,4)); 97 n <- reset (do x <- shift (��k. return (k (k 10))) ;
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | Data.sml | 3 datatype shift = LSL | LSR | ASR | ROR; type 18 | DpShiftImmediate of {Imm : int, Rm : vregister, Sh : shift} 19 | DpShiftRegister of {Rm : vregister, Rs : vregister, Sh : shift}; 23 | DtShiftImmediate of {Imm : int, Rm : vregister, Sh : shift};
|
H A D | instructionScript.sml | 21 shift = 30 | Dp_shift_immediate of shift=>word5 31 | Dp_shift_register of shift=>word4`; 36 | Dt_shift_immediate of shift=>word5`; 113 | Dp_shift_immediate shift amount => w2w amount << 7 || shift_encode shift 114 | Dp_shift_register shift Rs => 0x10w || w2w Rs << 8 || shift_encode shift`; 120 | Dt_shift_immediate shift amount => 121 0x2000000w || w2w amount << 7 || shift_encode shift`; [all...] |
H A D | armScript.sml | 294 SHIFT_IMMEDIATE2 shift (sh:word2) rm c = 296 0w => LSL rm shift c 297 | 1w => LSR rm (if shift = 0w then 32w else shift) c 298 | 2w => ASR rm (if shift = 0w then 32w else shift) c 299 | _ => if shift = 0w then word_rrx (c,rm) else ROR rm shift c`; 302 SHIFT_REGISTER2 shift (sh:word2) rm c = 304 0w => LSL rm shift 314 and shift = (11 >< 7) opnd2 value 324 and shift = (7 >< 0) (REG_READ reg mode Rs) in value [all...] |
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | coreutils.sml | 158 (* shifts: compute the core sets that result from shift/gotoing on 164 (2) then add the shift/gotos on kernal items. 166 We can do (1) the following way. Keep a table which for each shift/goto 170 item list in sorted order for each possible shift symbol. Scan the nonterminal 171 list from back to front. For each nonterminal, prepend the shift/goto list 172 for each shift symbol to the list already in the table. 174 We end up with the list of items in correct order for each shift/goto 182 (* mergeShiftItems: add an item list for a shift/goto symbol to the table *) 190 kept these items sorted by their shift/goto symbol (the first symbol on 201 (* now create a table which for each shift/got [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/tools/ |
H A D | bitfield_gen.py | 259 ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d; 272 """%(r_shift_op)s %(shift)d; 284 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 286 %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; 294 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 297 """%(shift)d) & 0x%(mask)x; 327 ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d; 344 """%(r_shift_op)s %(shift)d; 358 %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 361 %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift) [all...] |
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/ |
H A D | bitfield_gen.py | 259 ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d; 272 """%(r_shift_op)s %(shift)d; 284 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 286 %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; 294 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 297 """%(shift)d) & 0x%(mask)x; 327 ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d; 344 """%(r_shift_op)s %(shift)d; 358 %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 361 %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift) [all...] |
/seL4-l4v-10.1.1/seL4/tools/ |
H A D | bitfield_gen.py | 259 ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d; 272 """%(r_shift_op)s %(shift)d; 284 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 286 %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; 294 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 297 """%(shift)d) & 0x%(mask)x; 327 ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d; 344 """%(r_shift_op)s %(shift)d; 358 %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); 361 %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift) [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/tile/ |
H A D | ffi.c | 237 /* Find the smallest shift count that doesn't lose information 243 #define OPS(a, b, shift) \ 244 (create_Imm16_X0((a) >> (shift)) | create_Imm16_X1((b) >> (shift)))
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | memmgr.cpp | 938 const unsigned shift = (sizeof(void*)-1) * 8; // Takes the high-order byte local 939 uintptr_t r = startS >> shift; 941 const uintptr_t s = endS == 0 ? 256 : endS >> shift; 949 if ((r << shift) != startS) 962 if ((s << shift) != endS) 977 const unsigned shift = (sizeof(void*)-1) * 8; 978 uintptr_t r = startS >> shift; 979 const uintptr_t s = endS == 0 ? 256 : endS >> shift; 986 if ((r << shift) != startS) 999 if ((s << shift) ! [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Word8.sml | 67 (* Arithmetic shift - sign extends. *) 69 arithmetic shift for Word because the sign bit is in a different 72 shift right down again. *) 89 (* TODO: This could be implemented using shifts. i.e logical shift 90 left by (Word.wordSize-Word8.wordSize) then arithmetic shift
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | syntax_style.scala | 45 def shift(y: Float): Font = 52 if (a > 0.0f) shift(a) 53 else if (b > 0.0f) shift(- b)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | syntax_style.scala | 45 def shift(y: Float): Font = 52 if (a > 0.0f) shift(a) 53 else if (b > 0.0f) shift(- b)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | armScript.sml | 248 SHIFT_IMMEDIATE2 shift (sh:word2) rm c = 249 if shift = 0w then 255 if sh = 0w then LSL rm shift c else 256 if sh = 1w then LSR rm shift c else 257 if sh = 2w then ASR rm shift c else 258 (* sh = 3w *) ROR rm shift c`; 261 SHIFT_REGISTER2 shift (sh:word2) rm c = 262 if sh = 0w then LSL rm shift c else 263 if sh = 1w then LSR rm shift c else 264 if sh = 2w then ASR rm shift 272 and shift = (11 >< 7) opnd2 value 282 and shift = (7 >< 0) (REG_READ reg mode Rs) in value [all...] |