/seL4-l4v-master/HOL4/src/floating-point/ |
H A D | fp16Syntax.sml | 3 val fp = "fp16" value
|
H A D | fp32Syntax.sml | 3 val fp = "fp32" value
|
H A D | fp64Syntax.sml | 3 val fp = "fp64" value
|
H A D | machine_ieeeLib.sml | 48 fun mk_fp_to_float fp fp_ty float_ty pre_k t t_ty w_ty = 50 val fp_to_float = fp ^ "_to_float" 67 fun mk_float_to_fp fp fp_ty float_ty t_ty w_ty = 69 val float_to_fp = "float_to_" ^ fp 79 fun mk_fp_to_real fp float_to_real fp_to_float fp_ty = 81 val fp_to_real = fp ^ "_to_real" 89 fun mk_fp_to_value fp float_value fp_to_float fp_ty = 91 val fp_to_value = fp ^ "_to_value" 99 fun mk_real_to_fp fp real_to_float float_to_fp fp_ty = 101 val real_to_fp = "real_to_" ^ fp [all...] |
H A D | fp-functor.sml | 2 val fp: string value 12 monop ("float_to_" ^ fp) 15 binop ("int_to_" ^ fp) 18 binop ("real_to_" ^ fp) 22 binop ("real_to_" ^ fp ^ "_with_flags") 24 fun pre s = fp ^ "_" ^ s
|
H A D | machine_ieeeScript.sml | 28 | NaN => (check_for_signalling [f], from_float (@fp. float_is_nan fp))
|
H A D | binary_ieeeLib.sml | 159 val fp = real_to_float0 r value 160 val fpr = float_to_real fp 164 then fp 166 val nfp = nextfloat fp 172 then if evenfloat fp 173 then fp 176 then fp 191 val fp = real_to_float0 r value 193 if float_to_real fp = r orelse negativefloat fp 208 val fp = real_to_float0 r value [all...] |
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.C | 43 char* open(File& fp) argument 49 fp.open(name, "wx+"); 50 if (fp.null()) 67 fp_name = temp_files.open(fp); 92 if (!fp.null()){ 94 fp.setMode(READ); 95 c2fp.push(fp.tell()); 96 fp.seek(0, SEEK_END); 97 fp.setMode(WRITE); 99 putUInt(fp, 178 parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) argument 219 parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, File& fp, uint64 tmp, ClauseId id, std::ofstream* fout) argument [all...] |
H A D | Proof.h | 46 File fp; member in class:Proof 72 ClauseId parseRoot (vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout = NULL); 73 void parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, File& fp, uint64 tmp, ClauseId id, std::ofstream* fout = NULL); 75 ClauseId parseRoot (vec<Lit>& clause, File& fp, uint64 tmp); 76 void parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, File& fp, uint64 tmp, ClauseId id);
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/examples/ |
H A D | fc_examples.sml | 77 [msub sp sp #1w; mstr [sp] r0; msub sp sp #1w; mmov ip sp; mpush sp {r0,fp,ip,lr,pc}; msub fp ip #1w; mldr r0 [ip, #1]; madd ip ip #1w], 80 [madd sp fp #3w; mstr [sp] r0; msub sp sp #1w; mldr r1 [sp, #1]; madd sp sp #1w; msub sp fp #4w; mpop sp {r0,fp,sp,pc}])), 93 4: stmfd sp!, {r0,fp,ip,lr,pc} 94 5: sub fp, ip, #1iw 99 10: add sp, fp, #3iw 104 15: sub sp, fp, #4iw 105 16: ldmfd sp!, {r0,fp,s [all...] |
/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | GraphExtra.sml | 22 val fp = hmdir.extendp {base = master_dir, extension = s} value 23 val {dir,file} = OS.Path.splitDirFile (hmdir.toAbsPath fp)
|
/seL4-l4v-master/HOL4/examples/real-to-float/ |
H A D | daisyScript.sml | 155 ���fp r r'. (FLOOKUP inputs v = SOME r) /\ 156 (FLOOKUP fp_inputs v = SOME fp) /\ 157 (c.to_real fp = Float r') /\ 159 (* each variable without an Err-requirement must be the closes fp *) 161 ���fp. (FLOOKUP fp_inputs v = SOME fp) /\ 162 (c.from_real r = SOME fp)` 165 distance c r fp (i,b,e) <=> 166 ���r'. (c.to_real fp = Float r') /\
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | funCall.sml | 40 caller's fp | saved lr | 1 42 | save fp | 3 59 callee's fp | saved lr | 61 | save fp | 73 (* Calculate the offset based on fp of the temporaries bebing read in a callee *) 95 SOME k => IR.MEM (IR.fromAlias IR.fp, ~2 - k) (* inputs *) 98 SOME j => IR.MEM (IR.fromAlias IR.fp, 3 + j + numSavedRegs) (* existing local variable *) 102 IR.MEM (IR.fromAlias IR.fp, 3 + (!i - 1) + numSavedRegs) (* local variables *) 153 STMFA sp!, {..., fp,ip,lr,pc} 154 SUB fp, i [all...] |
H A D | IRSyntax.sml | 20 datatype alias = fp | ip | sp | lr | pc 43 fun fromAlias fp = 11 49 fun toAlias 11 = fp 442 let fun printAlias fp = "fp"
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | funCall.sml | 28 caller's fp | saved lr | 1 30 | save fp | 3 47 callee's fp | saved lr | 49 | save fp | 61 (* Calculate the offset based on fp of the temporaries bebing read in a callee *) 83 SOME k => IR.MEM (IR.fromAlias IR.fp, ~2 - k) (* inputs *) 86 SOME j => IR.MEM (IR.fromAlias IR.fp, 3 + j + numSavedRegs) (* existing local variable *) 90 IR.MEM (IR.fromAlias IR.fp, 3 + (!i - 1) + numSavedRegs) (* local variables *) 141 STMFA sp!, {..., fp,ip,lr,pc} 142 SUB fp, i [all...] |
H A D | IRSyntax.sml | 20 datatype alias = fp | ip | sp | lr | pc 43 fun fromAlias fp = 11 49 fun toAlias 11 = fp 434 let fun printAlias fp = "fp"
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | funCall.sml | 28 caller's fp | saved lr | 1 30 | save fp | 3 47 callee's fp | saved lr | 49 | save fp | 61 (* Calculate the offset based on fp of the temporaries bebing read in a callee *) 83 SOME k => IR.MEM (IR.fromAlias IR.fp, ~2 - k) (* inputs *) 86 SOME j => IR.MEM (IR.fromAlias IR.fp, 3 + j + numSavedRegs) (* existing local variable *) 90 IR.MEM (IR.fromAlias IR.fp, 3 + (!i - 1) + numSavedRegs) (* local variables *) 138 STMFA sp!, {..., fp,ip,lr,pc} 139 SUB fp, i [all...] |
H A D | bigInstScript.sml | 51 (reade st (isV k) = read st (MEM (fp, NEG k))) /\ 58 (writee st (isV k, v) = write st (MEM (fp, NEG k)) v) /\ 84 (eq_exp st (isR r) (isV v) = (r = fp)) /\ 85 (eq_exp st (isV v) (isR r) = (r = fp)) /\ 197 `!st e v. ~(eq_exp st e1 e2) /\ ~(e1 = isR fp) ==> ((st |# (e1,v) '' e2 = st '' e2))`, 350 [MLDR R9 (fp, NEG k); MSTR (13,offset) R9])`; 358 [MLDR R9 (13,offset); MSTR (fp, NEG (12 + k)) R9])`; 366 [MLDR R9 (fp, NEG k); MSTR (13,NEG 0) R9; MSUB R13 R13 (MC 1w)]) /\ 376 [MLDR R9 (13, POS 1); MSTR (fp,NEG k) R9; MADD R13 R13 (MC 1w)]) /\ 515 `~(isR 9 = isR fp) /\ ~(is [all...] |
H A D | funCallScript.sml | 167 saved_regs_list = [isR 0; isR 1; isR 2; isR 3; isR 4; isR 5; isR 6; isR 7; isR 8; isR fp; isR ip; isR lr]`; 172 MSUB R11 R12 (MC 1w)] (* sub fp ip 1 *) 286 fp | saved sp | 287 | saved fp | 642 (* We need to keep track of how sp,fp and ip are changed. *) 643 (* Note that r0-r8,fp,ip and lr are also pushed into the stack *) 857 run_cfl (BLK [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]) st)`, 880 run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: (APPEND (push_list l) [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st)`, 895 [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ 915 `MSUB R13 R13 (MC (n2w k))::push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; i [all...] |
H A D | IRSyntax.sml | 20 datatype alias = fp | ip | sp | lr | pc 43 fun fromAlias fp = 11 49 fun toAlias 11 = fp 434 let fun printAlias fp = "fp"
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | grammarScript.sml | 301 qabbrev_tac `fp = fsp1 ++ nilps` >> 303 `fsp1 ++ (nilps ++ [[x]] ++ nilss) ++ fss = fp ++ [[x]] ++ fs` 309 fp = MAP ptree_fringe ts1 ��� 315 `FLAT fs = FLAT fss ��� FLAT fp = FLAT fsp1` 340 `���fp. fpx = fp ++ [x]` 350 fp ++ [x] ++ fs = ptree_fringe ptx` 353 map_every qexists_tac [`fp`, `fs`, `pt1`, `ptx`, `pt2`] >>
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_core_decompScript.sml | 33 (* fp registers *) (word5 -> word64) =>
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | root.tex | 65 \input{fp}
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | root.tex | 65 \input{fp}
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_tests.sml | 2 "e28bb001" (* add fp, fp, #1 *) :: 3 "e281b207" (* add fp, r1, #1879048192 *) :: 32 "e08b0200" (* add r0, fp, r0, lsl #4 *) :: 135 "e08b2914" (* add r2, fp, r4, lsl r9 *) :: 320 "1282b001" (* addne fp, r2, #1 *) :: 331 "e20bb002" (* and fp, fp, #2 *) :: 332 "e002ba0b" (* and fp, r2, fp, ls [all...] |