Searched refs:fp (Results 1 - 25 of 57) sorted by relevance

123

/seL4-l4v-master/HOL4/src/floating-point/
H A Dfp16Syntax.sml3 val fp = "fp16" value
H A Dfp32Syntax.sml3 val fp = "fp32" value
H A Dfp64Syntax.sml3 val fp = "fp64" value
H A Dmachine_ieeeLib.sml48 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 Dfp-functor.sml2 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 Dmachine_ieeeScript.sml28 | NaN => (check_for_signalling [f], from_float (@fp. float_is_nan fp))
H A Dbinary_ieeeLib.sml159 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 DProof.C43 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 DProof.h46 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 Dfc_examples.sml77 [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 DGraphExtra.sml22 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 DdaisyScript.sml155 ���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 DfunCall.sml40 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 DIRSyntax.sml20 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 DfunCall.sml28 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 DIRSyntax.sml20 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 DfunCall.sml28 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 DbigInstScript.sml51 (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 DfunCallScript.sml167 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 DIRSyntax.sml20 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 DgrammarScript.sml301 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 Darm_core_decompScript.sml33 (* fp registers *) (word5 -> word64) =>
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Droot.tex65 \input{fp}
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Droot.tex65 \input{fp}
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_tests.sml2 "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...]

Completed in 126 milliseconds

123