/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | windows_specific.cpp | 677 LRESULT res; local
|
H A D | network.cpp | 767 int res = connect(strm->device.sock, psock, (int)psAddr->length); local
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sml | 197 val res as (tm',_) = conv tm value 314 val res as (lit',_) = literule lit value
|
H A D | Useful.sml | 850 val res = f a value [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sml | 197 val res as (tm',_) = conv tm value 314 val res as (lit',_) = literule lit value
|
H A D | Useful.sml | 850 val res = f a value [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/arm/machine/ |
H A D | l2c_310.c | 110 uint32_t res[62]; member in struct:l2cc_map::__anon221 118 uint32_t res[60]; member in struct:l2cc_map::__anon222 131 uint32_t res[55]; member in struct:l2cc_map::__anon223 135 uint32_t res[64]; member in struct:l2cc_map::__anon224 138 uint32_t res[64]; member in struct:l2cc_map::__anon225 141 uint32_t res[64]; member in struct:l2cc_map::__anon226 144 uint32_t res[64]; member in struct:l2cc_map::__anon227 148 uint32_t res[12]; member in struct:l2cc_map::__anon228 167 uint32_t res[64]; member in struct:l2cc_map::__anon229 187 uint32_t res[ member in struct:l2cc_map::__anon230 194 uint32_t res[64]; member in struct:l2cc_map::__anon231 197 uint32_t res[64]; member in struct:l2cc_map::__anon232 203 uint32_t res[62]; member in struct:l2cc_map::__anon233 207 uint32_t res[64]; member in struct:l2cc_map::__anon234 210 uint32_t res[64]; member in struct:l2cc_map::__anon235 214 uint32_t res[16]; member in struct:l2cc_map::__anon236 [all...] |
/seL4-l4v-10.1.1/seL4/src/object/ |
H A D | tcb.c | 602 getBreakpoint_t res; local
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 249 val res = map process cls' value 413 val res = rw tm value 421 val res = QCONV RW tm value 467 val res = [(empty_subst, cl', rule')] value 879 val res = map (process vars lit) matches value 894 val res = map (process vars lit) matches value 928 val res = fvars [] [tm] value 943 val res = mk_comb (k, g) value 976 val res = mk_comb (mk_comb (s, g1), g2) value 994 val res = map (s_set_var vars (pos, atom)) funvars value 1039 val res = value 1136 val res = map (finalize lit) (perform_para pos_db vars atom) value 1162 val res = map snd (trans cons_subsume [] (map tag l)) value 1253 val res = value 1268 val res = value 1315 val res = (post_process goal o frule) input value [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Pmatch.sml | 475 val res = run_heu heu value
|
/seL4-l4v-10.1.1/HOL4/src/meson/src/ |
H A D | mesonLib.sml | 961 val res = tac infs g value
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folMapping.sml | 829 val res = mlibThm.proof th value 842 val res = proof_step parm prev p value
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | blastLib.sml | 1141 val res = FORALL_EQ_RULE vars value
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | Portable.sml | 669 val res = f x handle e => (flag := fval; raise e) value
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | simpLib.sml | 676 val res = Lib.with_flag(track_rewrites,true) f x value
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holmake_tools.sml | 72 val res = OS.Process.system (String.concatWith " " [s,"1>",outfile,"2>&1"]) value
|
/seL4-l4v-10.1.1/HOL4/tools/mllex/ |
H A D | mllex.sml | 1025 val res = makeEntry(trans,nil,empty) value
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | derive_specsLib.sml | 466 val res = wrap_get_spec f instruction value 493 val res = wrap_get_spec f instruction value 509 val res = get_specs code value 516 val res = calc_addresses 0 res value 517 val res = inst_pc_var tools res value 574 val res = map delete_long_jump res value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | cearTools.sml | 123 val res = mk_lthm (fn _ => (gl,jf)) jf value 143 val res = PBETA_RULE (GEN_ALL (ISPECL [ksname,mk_var("e",stringLib.string_ty-->(type_of st1)-->bool),aht] th5)) value 627 val res value 824 val res = List.foldl (fn ((ip,(g,ap)),th) => value 861 val res = if is_existential mf orelse (not (isSome aapl)) value 867 val (res,mu_ic) = muCheck (Array.fromList []) I1 T1 state vm Ric (ref NONE) (NONE,NONE) value 880 val (res,mu_ic_snd) = absCheck_aux I1 ITdf T1 RTm Ric state (apl,ks_def,wfKS_ks) value 885 val res = finalise (apl,ks_def,wfKS_ks,ITdf) apsubs state mf2 res value [all...] |
H A D | muCheck.sml | 45 val res = lzPBETA_RULE (PURE_REWRITE_RULE [Tth] (SPEC nm modth)) value 152 val res = BddEqMp sth tb value 163 val res = BddEqMp sth (BddCon b vm) value 178 val res = BddEqMp sth (snd(Array.sub(ee,ix))) value 222 val res = if is_RV mf (* RV case *) value 256 val res = value 289 val res = mk_lthm (fn _ => (goal,jf)) jf value 306 val res = if (Term.compare(env,ie)=EQUAL) value 613 val res = let value 851 val res = value [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | OS.sml | 553 val res = toString{isAbs=isAbs, vol=vol, arcs=newArcs} value
|
H A D | TopLevelPolyML.sml | 1352 val res = compilerLoop() value
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Message.sml | 3660 val res: SysWord.word = oldDefProc(hw, m, w, l) value 3708 val res = peekMsg(msg, getOpt(hWnd, hNull), wMsgFilterMin, wMsgFilterMax, opts) value 3750 val res = peekMsg(msg, hNull, 0, 0, 1) value 3844 val res = getQueueStatus(fromQS flags) value [all...] |
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | parse_term.sml | 829 val res = valOf (Polyhash.peek prec_matrix ((x2,false),x1)) value 849 val res = valOf (Polyhash.peek prec_matrix ((x2,true), x1)) value
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
H A D | ind_rel.sml | 1000 val res = (uncurry DISCH) (itlist chfn vs (hh,nthm)) value [all...] |