Searched refs:dst (Results 1 - 25 of 83) sorted by relevance

1234

/seL4-l4v-master/isabelle/Admin/lib/Tools/
H A Dregenerate_cooper9 dst='~~/src/HOL/Tools/Qelim/'
12 "${ISABELLE_TOOL}" export -x "${src}" -p 2 -O "${dst}" "${session}"
/seL4-l4v-master/l4v/isabelle/Admin/lib/Tools/
H A Dregenerate_cooper9 dst='~~/src/HOL/Tools/Qelim/'
12 "${ISABELLE_TOOL}" export -x "${src}" -p 2 -O "${dst}" "${session}"
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dgc_copy_phase.cpp93 static inline PolyWord *FindFreeAndAllocate(LocalMemSpace *dst, uintptr_t limit, uintptr_t 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 uintptr_t start = dst->start[truncated_n];
129 free = dst
192 FindNextSpace(LocalMemSpace *src, LocalMemSpace **dst, bool isMutable, GCTaskId *id) argument
[all...]
/seL4-l4v-master/HOL4/polyml/
H A Dinstall-sh80 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-master/seL4/src/arch/x86/64/kernel/
H A Delf.c52 paddr_t dst; local
59 dst = phdr[i].p_vaddr + offset;
61 memcpy((void *)dst, (char *)src, len);
62 dst += len;
63 memset((void *)dst, 0, phdr[i].p_memsz - len);
/seL4-l4v-master/seL4/src/arch/x86/32/kernel/
H A Delf.c55 paddr_t dst; local
62 dst = phdr[i].p_vaddr + offset;
64 memcpy((void *)dst, (char *)src, len);
65 dst += len;
66 memset((void *)dst, 0, phdr[i].p_memsz - len);
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DCFLScript.sml202 (!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 DHSL2CFLScript.sml39 (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 DHSLScript.sml246 (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 DpreARMScript.sml240 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-master/HOL4/examples/muddy/muddyC/buddy/examples/solitare/
H A Dsolitare.cxx91 // 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-master/HOL4/examples/bootstrap/
H A Dx64asm_syntaxScript.sml88 inst (Mov dst src) s = "movq " ++ reg src (", " ++ reg dst s) ���
89 inst (Add dst src) s = "addq " ++ reg src (", " ++ reg dst s) ���
90 inst (Sub dst src) s = "subq " ++ reg src (", " ++ reg dst s) ���
105 inst (Load dst a w) s =
106 "movq " ++ num (w2n w) ("(" ++ reg a ("), " ++ reg dst s)) ���
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DILScript.sml163 (!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 DpreARMScript.sml252 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 DfunCall.sml108 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-master/HOL4/examples/dev/sw/working/0.1/
H A DILScript.sml163 (!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 DpreARMScript.sml248 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 DILTheory.sig1267 |- (!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-master/HOL4/examples/l3-machine-code/x64/model/
H A Dx64.sml1734 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-master/graph-refine/graph-to-graph/
H A Dpydot.py268 dst = node_prefix + edge[1]
270 dst = node_prefix + str(edge[1])
272 e = Edge( src, dst )
843 edge(src, dst, attribute=value, ...)
846 dst: destination node's name
866 def __init__(self, src='', dst='', obj_dict=None, **attrs):
868 if isinstance(src, (list, tuple)) and dst == '':
869 src, dst = src
890 if isinstance(dst, Node):
891 dst
[all...]
/seL4-l4v-master/HOL4/polyml/modules/IntInfAsInt/
H A DArrayVector.sml103 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-master/HOL4/examples/dev/sw2/
H A DSALGen.sml67 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 DfuncCall.sml128 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-master/isabelle/src/Tools/Metis/src/
H A DPortableMosml.sml88 fun Array_copy {src,dst,di} =
92 copy {src = src, si = 0, len = NONE, dst = dst, di = di}
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DPortableMosml.sml88 fun Array_copy {src,dst,di} =
92 copy {src = src, si = 0, len = NONE, dst = dst, di = di}

Completed in 276 milliseconds

1234