/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | install-sh | 80 dst= 254 dst=$src 255 dstdir=$dst 272 dst=$dst_arg 276 if test -d "$dst"; then 281 dstdir=$dst 282 dst=$dstdir/`basename "$src"` 285 dstdir=`dirname "$dst"` 430 { test -z "$chowncmd" || $doit $chowncmd "$dst"; } && 431 { test -z "$chgrpcmd" || $doit $chgrpcmd "$dst"; } [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | install-sh | 80 dst= 254 dst=$src 255 dstdir=$dst 272 dst=$dst_arg 276 if test -d "$dst"; then 281 dstdir=$dst 282 dst=$dstdir/`basename "$src"` 285 dstdir=`dirname "$dst"` 430 { test -z "$chowncmd" || $doit $chowncmd "$dst"; } && 431 { test -z "$chgrpcmd" || $doit $chgrpcmd "$dst"; } [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | gc_copy_phase.cpp | 93 static inline PolyWord *FindFreeAndAllocate(LocalMemSpace *dst, POLYUNSIGNED limit, POLYUNSIGNED n) argument 95 if (dst == 0) return 0; // No current space 109 for (unsigned i = dst->start_index; i < truncated_n; i ++) 111 if (dst->start[i] < dst->start[i+1]) 112 dst->start[i+1] = dst->start[i]; 115 dst->start_index = truncated_n; 116 POLYUNSIGNED start = dst->start[truncated_n]; 121 POLYUNSIGNED free = dst [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/kernel/ |
H A D | elf.c | 64 paddr_t dst; local 71 dst = phdr[i].p_vaddr + offset; 73 memcpy((void*)dst, (char*)src, len); 74 dst += len; 75 memset((void*)dst, 0, phdr[i].p_memsz - len);
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/kernel/ |
H A D | elf.c | 61 paddr_t dst; local 68 dst = phdr[i].p_vaddr + offset; 70 memcpy((void *)dst, (char *)src, len); 71 dst += len; 72 memset((void *)dst, 0, phdr[i].p_memsz - len);
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFLScript.sml | 202 (!dst src.mdecode st (MLDR dst src) = 203 write st (toREG dst) (read st (toMEM src))) /\ 204 (!dst src.mdecode st (MSTR dst src) = 205 write st (toMEM dst) (read st (toREG src))) /\ 206 (mdecode st (MMOV dst src) = 207 write st (toREG dst) (read st (toEXP src))) /\ 208 (mdecode st (MADD dst src1 src2) = 209 write st (toREG dst) (rea [all...] |
H A D | HSL2CFLScript.sml | 39 (translate_assgn (TMOV dst src) = MMOV (conv_reg dst) (conv_roc src)) /\ 41 (translate_assgn (TADD dst (Rg r) src) = MADD (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 42 (translate_assgn (TADD dst (Cn v) (Rg r)) = MADD (conv_reg dst) (conv_reg r) (MC v)) /\ 43 (translate_assgn (TADD dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1+v2))) /\ 44 (translate_assgn (TSUB dst (Rg r) src) = MSUB (conv_reg dst) (conv_re [all...] |
H A D | HSLScript.sml | 246 (transfer (s1,s0) (dst::dstL, src::srcL) = 247 transfer (twrite s1 dst (tread s0 src), s0) (dstL, srcL))`; 250 (!dst src.tdecode hs (TLDR dst src) = 251 twrite hs (inR dst) (tread hs (inE src))) /\ 252 (!dst src.tdecode hs (TSTR dst src) = 253 twrite hs (inE dst) (tread hs (inR src))) /\ 254 (tdecode hs (TMOV dst src) = 255 twrite hs (inR dst) (trea [all...] |
H A D | preARMScript.sml | 240 decode_op (pc,cpsr,s) (op,dst,src,jump) = 242 MOV -> (cpsr, write s (THE dst) (read s (HD src))) 248 LDMFD -> (case THE dst of 262 STMFD -> (case THE dst of 273 ADD -> (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src)))))) 275 SUB -> (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src)))))) 277 RSB -> (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src)))) 279 MUL -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src)))))) 281 MLA -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) + 284 AND -> (cpsr, (write s (THE dst) (rea [all...] |
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/solitare/ |
H A D | solitare.cxx | 91 // there's a move from 'src' to 'dst' over 'tmp' 92 bdd all_other_idle(int src, int tmp, int dst) argument 98 if (n != src && n != tmp && n != dst) 106 // Encode one move from 'src' to 'dst' over 'tmp' 107 bdd make_move(int src, int tmp, int dst) argument 109 bdd move = boardC[src] & boardC[tmp] & !boardC[dst] & 110 !boardN[src] & !boardN[tmp] & boardN[dst]; 112 move &= all_other_idle(src, tmp, dst);
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | ILScript.sml | 163 (!dst src.mdecode st (MLDR dst src) = 164 write st (toREG dst) (read st (toMEM src))) /\ 165 (!dst src.mdecode st (MSTR dst src) = 166 write st (toMEM dst) (read st (toREG src))) /\ 167 (mdecode st (MMOV dst src) = 168 write st (toREG dst) (read st (toEXP src))) /\ 169 (mdecode st (MADD dst src1 src2) = 170 write st (toREG dst) (rea [all...] |
H A D | preARMScript.sml | 252 decode_op (pc,cpsr,s) (op,dst,src,jump) = 254 MOV => (cpsr, write s (THE dst) (read s (HD src))) 260 LDMFD => (case THE dst of 274 STMFD => (case THE dst of 285 ADD => (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src)))))) 287 SUB => (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src)))))) 289 RSB => (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src)))) 291 MUL => (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src)))))) 293 MLA => (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) + 296 AND => (cpsr, (write s (THE dst) (rea [all...] |
H A D | funCall.sml | 108 fun one_stm ({oper = op1, dst = dst1, src = src1}) = 109 {oper = op1, dst = List.map filter_mems dst1, src = List.map filter_mems src1} 143 fun dec_p pt n = {oper = IR.msub, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]} 145 fun inc_p pt n = {oper = IR.madd, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]}; 159 [ {oper = IR.mmov, dst = [IR.REG (IR.fromAlias IR.ip)], src = [IR.REG (IR.fromAlias IR.sp)]}, 160 {oper = IR.mpush, dst = [IR.REG (IR.fromAlias IR.sp)], 164 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.fp)], src = [IR.REG (IR.fromAlias IR.ip), IR.WCONST (Arbint.fromInt 4)]}, 175 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.sp)], src = [IR.REG (IR.fromAlias IR.fp), IR.WCONST (Arbint.fromInt (4* (3 + length rs)))]}, 176 {oper = IR.mpop, dst = rs @ [IR.REG (IR.fromAlias IR.fp), IR.REG (IR.fromAlias IR.sp), IR.REG (IR.fromAlias IR.pc)], 222 {oper = IR.mldr, dst [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ILScript.sml | 163 (!dst src.mdecode st (MLDR dst src) = 164 write st (toREG dst) (read st (toMEM src))) /\ 165 (!dst src.mdecode st (MSTR dst src) = 166 write st (toMEM dst) (read st (toREG src))) /\ 167 (mdecode st (MMOV dst src) = 168 write st (toREG dst) (read st (toEXP src))) /\ 169 (mdecode st (MADD dst src1 src2) = 170 write st (toREG dst) (rea [all...] |
H A D | preARMScript.sml | 248 decode_op (pc,cpsr,s) (op,dst,src,jump) = 250 MOV -> (cpsr, write s (THE dst) (read s (HD src))) 256 LDMFD -> (case THE dst of 270 STMFD -> (case THE dst of 281 ADD -> (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src)))))) 283 SUB -> (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src)))))) 285 RSB -> (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src)))) 287 MUL -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src)))))) 289 MLA -> (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) + 292 AND -> (cpsr, (write s (THE dst) (rea [all...] |
H A D | ILTheory.sig | 1267 |- (!st dst src. 1268 mdecode st (MLDR dst src) = 1269 write st (toREG dst) (read st (toMEM src))) /\ 1270 (!st dst src. 1271 mdecode st (MSTR dst src) = 1272 write st (toMEM dst) (read st (toREG src))) /\ 1273 (!st dst src. 1274 mdecode st (MMOV dst src) = 1275 write st (toREG dst) (read st (toEXP src))) /\ 1276 (!st dst src [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64.sml | 1734 fun dfn'bin_PD (bop,(dst,src)) = 1736 val dst = xmm_reg dst value 1737 val x = XMM dst 1744 ( process_float_flags[f1,f2]; write'XMM(BitsN.@@(r1,r2),dst) ) 1747 fun dfn'bin_PS (bop,(dst,src)) = 1749 val dst = xmm_reg dst value 1750 val x = XMM dst 1762 ; write'XMM(BitsN.concat[r1,r2,r3,r4],dst) 1768 val dst = xmm_reg dst value 1784 val dst = xmm_reg dst value 1800 val dst = xmm_reg dst value 1812 val dst = xmm_reg dst value 1826 val dst = xmm_reg dst value 1839 val dst = xmm_reg dst value 1858 val dst = xmm_reg dst value 1875 val dst = xmm_reg dst value 2228 val dst = xmm_reg dst value 2244 val dst = xmm_reg dst value 2251 val dst = xmm_reg dst value 2264 val dst = xmm_reg dst value 2276 val dst = xmm_reg dst value 2292 val dst = xmm_reg dst value 2305 val dst = xmm_reg dst value 2321 val dst = xmm_reg dst value 2328 val dst = xmm_reg dst value 2342 val dst = xmm_reg dst value 2354 val dst = xmm_reg dst value [all...] |
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | pydot.py | 265 dst = node_prefix + edge[1] 267 dst = node_prefix + str(edge[1]) 269 e = Edge( src, dst ) 840 edge(src, dst, attribute=value, ...) 843 dst: destination node's name 863 def __init__(self, src='', dst='', obj_dict=None, **attrs): 865 if isinstance(src, (list, tuple)) and dst == '': 866 src, dst = src 887 if isinstance(dst, Node): 888 dst [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
H A D | ArrayVector.sml | 103 val copy : {src : array, dst : array, di : FixedInt.int} -> unit 104 val copyVec : {src : vector, dst : array, di : FixedInt.int} -> unit 127 val copy = fn {di, dst, src} => copy {di=FixedInt.fromLarge di, dst=dst, src=src} 128 val copyVec = fn {di, dst, src} => copyVec {di=FixedInt.fromLarge di, dst=dst, src=src} 153 val copy = fn {di, dst, src} => copy {di=FixedInt.fromLarge di, dst [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | SALGen.sml | 67 type spec_type = {body : term, dst : term, entry : term, exit : term, exp : term, thm : thm} 80 {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest} 88 val exp = mk_plet (#dst spec1, #exp spec1, 89 mk_comb(mk_pabs (#dst spec1, #exp spec2), #dst spec1)) 90 val value = mk_pair(exp, #dst spec2) 96 EXISTS_TAC (#exit spec1) THEN EXISTS_TAC (#dst spec1) THEN 102 {entry = #entry spec1, exit = #exit spec2, body = union_body, thm = spec_thm, exp = exp, dst = #dst spec2} 157 {entry = entry_l, exit = exit_l, body = b2, thm = spec_thm, exp = exp', dst [all...] |
H A D | funcCall.sml | 128 fun format_call (fname, dst, src, cont) = 134 val s2 = S.difference(s1, S.addList(S.empty tvarOrder, strip_pair dst)) 137 val t2 = regAlloc.parallel_move dst dst0 t1 152 val (fname, dst, src, cont) = (x, v, y, caller_save N) 154 format_call (fname, dst, src, cont) 195 val (fname, dst, src, cont) = (x, v, y, N') 196 val t' = format_call (fname, dst, src, cont) 280 List.map (fn (fname, ((src, dst), (wS, slot))) => (fname, (src, dst, S.listItems wS, slot))) (M.listItems (!fmap))
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | PortableMosml.sml | 88 fun Array_copy {src,dst,di} = 92 copy {src = src, si = 0, len = NONE, dst = dst, di = di}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | PortableMosml.sml | 88 fun Array_copy {src,dst,di} = 92 copy {src = src, si = 0, len = NONE, dst = dst, di = di}
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | file.scala | 287 def copy(src: JFile, dst: JFile) 289 val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst 301 def move(src: JFile, dst: JFile) 303 val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | file.scala | 287 def copy(src: JFile, dst: JFile) 289 val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst 301 def move(src: JFile, dst: JFile) 303 val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
|