/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | Makefile | 15 DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/string/Manual/ |
H A D | Makefile | 15 DOCTOTEXEXE=../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/unwind/Manual/ |
H A D | Makefile | 15 DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | ArraySignature.sml | 33 val copy : {src : 'a array, dst : 'a array, di : int} -> unit 34 val copyVec : {src : 'a vector, dst : 'a array, di : int} -> unit
|
H A D | Real.sml | 430 fun scan getc src = 433 fun getdigits inp src = 434 case getc src of 435 NONE => (List.rev inp, src) 436 | SOME(ch, src') => 438 then getdigits ((Char.ord ch - Char.ord #"0") :: inp) src' 439 else (List.rev inp, src) 442 fun getNumber sign digits acc src = 443 case getc src of 444 NONE => if digits = 0 then NONE else SOME(if sign then ~acc else acc, src) [all...] |
H A D | Word8Array.sml | 36 fun System_move_str(src: vector, dst: address, srcOffset: word, dstOffset: word, length: word): unit = 37 RunCall.moveBytes(src, RunCall.unsafeCast dst, srcOffset, dstOffset, length) 209 fun copy {src=Array (len, s), dst=Array (dlen, d), di: int} = 219 fun copyVec {src, dst=Array (dlen, d), di: int} = 221 val len = intAsWord(vecLength src) 226 else System_move_str(src, d, wordSize, diW, len) 371 fun copy {src, dst, di: int} = 373 val (src, start, length) = base src value 384 else (Word8Array.update(dst, n+di, Word8Array.sub(src, [all...] |
H A D | Word16.sml | 88 fun scan radix getc src = 89 case wordScan radix getc src of 91 | SOME(res, src') => 94 else SOME(res, src')
|
H A D | Word32In64.sml | 91 fun scan radix getc src = 92 case wordScan radix getc src of 94 | SOME(res, src') => 97 else SOME(res, src')
|
H A D | ArraySliceSignature.sml | 33 val copy : {src : 'a slice, dst : 'a array, di : int} -> unit 34 val copyVec : {src : 'a VectorSlice.slice, dst : 'a array, di : int} -> unit
|
H A D | MONO_ARRAY.sml | 36 val copy : {src : array, dst : array, di : int} -> unit 37 val copyVec : {src : vector, dst : array, di : int} -> unit
|
/seL4-l4v-10.1.1/HOL4/examples/computability/register/ |
H A D | regScript.sml | 770 RPmove src dest basei exiti = 771 RPWhile src basei exiti (basei + 1) 786 ``exiti ��� basei ��� exiti ��� basei + 1 ��� src ��� dest ��� 789 REGfRsub (REGfRsub (PCsub Q exiti) src (K 0)) 791 (��r. r dest + r src)) 793 P ��� (RPmove src dest basei exiti) ��� Q``, 796 map_every qexists_tac [`��n. P && (��pc reg. reg src + reg dest = n)`, 803 qexists_tac `(��pc reg. reg src + reg dest = Z) && 804 REGfRsub (REGfRsub (PCsub Q exiti) src (K 0)) 806 (��r. r dest + r src)` >> [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | CFG.sml | 83 [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 87 ({ instr = Assem.OPER {oper = (bi_operator bop,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 95 [{ instr = Assem.OPER {oper = (Assem.CMP,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 105 src = [one_exp args], 112 [{ instr = Assem.MOVE {dst = one_exp d, src = one_exp s}, 117 [{ instr = Assem.OPER {oper = (Assem.B,SOME Assem.AL,false), dst = [], src = [], jump = SOME [lab]}, 122 [{ instr = Assem.OPER {oper = (Assem.B, SOME (cjump (getTmp e)), false), dst = [], src = [one_exp e], jump = SOME [lab]}, 173 val augmentedInsts = ({instr = Assem.OPER{oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 175 insts @ [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE},
|
H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} 234 fun convert_stm ({oper = op1, dst = dlist, src = slist}) = 327 fun to_inst (Assem.OPER {oper = (oper', cond', flag'), dst = dlist, src = slist, jump = jumps}) = 328 {oper = to_op oper', dst = List.map to_exp dlist, src = List.map to_exp slist} 329 | to_inst (Assem.MOVE {dst = dst', src = src'}) = 330 {oper = mmov, dst = [to_exp dst'], src = [to_exp src']} 334 fun to_cond (Assem.OPER {oper = (Assem.CMP, cond1, flag1), dst = dlist1, src = slist1, jump = jumps1}, 335 Assem.OPER {oper = (Assem.B, cond2, flag2), dst = dlist2, src [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | CFG.sml | 84 [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 88 ({ instr = Assem.OPER {oper = (bi_operator bop,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 96 [{ instr = Assem.OPER {oper = (Assem.CMP,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 106 src = [one_exp args], 113 [{ instr = Assem.MOVE {dst = one_exp d, src = one_exp s}, 118 [{ instr = Assem.OPER {oper = (Assem.B,SOME Assem.AL,false), dst = [], src = [], jump = SOME [lab]}, 123 [{ instr = Assem.OPER {oper = (Assem.B, SOME (cjump (getTmp e)), false), dst = [], src = [one_exp e], jump = SOME [lab]}, 174 val augmentedInsts = ({instr = Assem.OPER{oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 176 insts @ [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE},
|
H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} 234 fun convert_stm ({oper = op1, dst = dlist, src = slist}) = 319 fun to_inst (Assem.OPER {oper = (oper', cond', flag'), dst = dlist, src = slist, jump = jumps}) = 320 {oper = to_op oper', dst = List.map to_exp dlist, src = List.map to_exp slist} 321 | to_inst (Assem.MOVE {dst = dst', src = src'}) = 322 {oper = mmov, dst = [to_exp dst'], src = [to_exp src']} 326 fun to_cond (Assem.OPER {oper = (Assem.CMP, cond1, flag1), dst = dlist1, src = slist1, jump = jumps1}, 327 Assem.OPER {oper = (Assem.B, cond2, flag2), dst = dlist2, src [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFG.sml | 84 [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 88 ({ instr = Assem.OPER {oper = (bi_operator bop,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 96 [{ instr = Assem.OPER {oper = (Assem.CMP,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 106 src = [one_exp args], 113 [{ instr = Assem.MOVE {dst = one_exp d, src = one_exp s}, 118 [{ instr = Assem.OPER {oper = (Assem.B,SOME Assem.AL,false), dst = [], src = [], jump = SOME [lab]}, 123 [{ instr = Assem.OPER {oper = (Assem.B, SOME (cjump (getTmp e)), false), dst = [], src = [one_exp e], jump = SOME [lab]}, 174 val augmentedInsts = ({instr = Assem.OPER{oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 176 insts @ [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE},
|
H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} 234 fun convert_stm ({oper = op1, dst = dlist, src = slist}) = 319 fun to_inst (Assem.OPER {oper = (oper', cond', flag'), dst = dlist, src = slist, jump = jumps}) = 320 {oper = to_op oper', dst = List.map to_exp dlist, src = List.map to_exp slist} 321 | to_inst (Assem.MOVE {dst = dst', src = src'}) = 322 {oper = mmov, dst = [to_exp dst'], src = [to_exp src']} 326 fun to_cond (Assem.OPER {oper = (Assem.CMP, cond1, flag1), dst = dlist1, src = slist1, jump = jumps1}, 327 Assem.OPER {oper = (Assem.B, cond2, flag2), dst = dlist2, src [all...] |
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))) /\ 237 (translate_assignment (MMOV dst src) = ((MOV,NONE,F),SOME (toREG dst), [toEXP src], NON [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)) /\ 44 (translate_assgn (TSUB dst (Rg r) src) = MSUB (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 47 (translate_assgn (TRSB dst (Rg r) src) = MRSB (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 50 (translate_assgn (TMUL dst (Rg r) src) = MMUL (conv_reg dst) (conv_reg r) (conv_roc src)) /\ [all...] |
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | build.sml | 75 fun upload ((src, regulardir), target, symlink) = 78 map_dir (transfer_file symlink target) src) 84 print ("Self-test directory "^src^" built successfully.\n")
|
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/ |
H A D | syscalls.h | 87 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 96 x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3); 111 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 121 x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 144 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 153 x64_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3);
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/fastpath/ |
H A D | fastpath.h | 110 fastpath_copy_mrs(word_t length, tcb_t *src, tcb_t *dest) argument 119 setRegister(dest, reg, getRegister(src, reg));
|
/seL4-l4v-10.1.1/seL4/include/plat/bcm2837/plat/ |
H A D | machine.h | 92 #define FIQCTRL_FIQ_SRC(src) (FIQCTRL_FIQ_SRC_##src)
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
H A D | congLibExamples.sml | 5 loadPath := (concat home_dir "src/deep_embeddings") :: 6 (concat home_dir "src/tools") :: !loadPath;
|
/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/ |
H A D | EventTo.c | 907 src 925 src 1085 src 1103 src
|