| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | misc.tex | |
| /seL4-l4v-master/HOL4/examples/acl2/ml/ |
| H A D | translateLib.sml | 109 let val (pre,post) = (I ## tl) (split_after n concls); value
|
| /seL4-l4v-master/HOL4/examples/decidable_separationLogic/src/ |
| H A D | decidable_separationLogicLib.sml | 111 val (pre, ante, cons) = (el 1 args, el 2 args, el 3 args); value
600 val (pre, _) = strip_cons c2; value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | funCall.sml | |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | funCall.sml | |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | funCall.sml | |
| /seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 351 val (pre, rhsL) = translate_exp_bool rhs (length lhsL); value
|
| /seL4-l4v-master/HOL4/examples/elliptic/swsep/ |
| H A D | swsepLib.sml | 121 val pre = hd args; value
|
| /seL4-l4v-master/HOL4/examples/lambda/basics/ |
| H A D | binderLib.sml | 211 val (pre,l,r) = let value
213 val (pre, eq) = dest_imp b value
|
| /seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
| H A D | compilerLib.sml | 102 val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH value
103 val pre = RW [IF_IF,WORD_TIMES2] pre value
126 val pre = RW [] (foldr (uncurry CONJ) TRUTH pres) value
139 val pre = fetch "-" (name ^ "_pre_def") value
219 val pre = get_pre tm value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 1698 val pre = (free_vars o cdr o car o car o snd o dest_imp o concl) th1 value
1722 val pre = (free_vars o cdr o car o car o snd o dest_imp o concl) th2 value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/ |
| H A D | prog_armLib.sml | 111 val pre = list_mk_star (map fst pre_post) ((type_of o fst o hd) pre_post) value
113 val (pre,post) = if not (tmem cpsr_var (free_vars g)) then (pre,post) else let value
139 val pre = if null pre_conds then pre else mk_cond_star(pre,mk_comb(``CONTAINER``,list_mk_conj pre_conds)) value
400 val pre = subst [``n:num``|->numSyntax.term_of_int n] ``aSTACK bp (l+n,ss)`` value
466 val (pre,cod value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
| H A D | prog_ppcLib.sml | 66 val pre = list_mk_star (map fst pre_post) ``:ppc_set -> bool`` value
79 val pre = subst ss pre value
81 val pre = if null pre_conds then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) value
167 val (pre,post) = ppc_pre_post g value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | prog_x86Lib.sml | 84 val pre = list_mk_star (map fst pre_post) ``:x86_set -> bool`` value
101 val pre = subst ss pre value
103 val pre = mk_star (pre,``xPC eip``) value
105 val pre = if null pre_conds then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) value
217 val (pre,pos value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | prog_x64Lib.sml | 116 val pre = list_mk_star (map fst pre_post) ``:x64_set -> bool`` value
133 val pre = subst ss pre value
135 val pre = mk_star (``zPC rip``,pre) value
137 val pre = if null pre_conds then pre value
436 val (pre,pos value
[all...] |
| H A D | prog_x64_extraScript.sml | 791 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\ value
824 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\ value
893 val pre = ``k < LENGTH (stack:word64 list) /\ k < 268435456`` value
934 val pre value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_finalScript.sml | 241 val pre = ``aLISP1 (t1,l) * aR 1w r1 * aSTRING_SPACE r1 (LENGTH (sexp2string t1)) * value
302 val pre = ``pLISP1 (t1,l) * pR 1w r1 * pSTRING_SPACE r1 (LENGTH (sexp2string t1)) * value
346 val pre = ``xSTACK (esp-4w) [w] * xR EDI edi * xR ESP esp * xPC p`` value
367 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p`` value
388 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p`` value
464 val pre = ``xLISP1 (t1,l) * xSTRING_SPACE w (LENGTH (sexp2string t1)) * value
[all...] |
| H A D | lisp_opsScript.sml | 80 val pre = (fst o dest_imp o snd o dest_imp) (concl imp) handle e => ``T:bool`` value
|
| /seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_compilerLib.sml | 93 val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH value
94 val pre = RW [IF_IF,WORD_TIMES2] pre value
120 val pre = RW [] (foldr (uncurry CONJ) TRUTH pres) value
|
| /seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | kernel.c | 989 void bdd_default_gbchandler(int pre, bddGbcStat *s) argument
|
| /seL4-l4v-master/HOL4/examples/muddy/muddyC/ |
| H A D | muddy.c | 119 EXTERNML value mlbdd_setprintgc(value print, value pre, value post) /* ML */ argument
|
| /seL4-l4v-master/HOL4/examples/pgcl/src/ |
| H A D | wpTools.sml | 101 val (pre,wlp_post) = dest_leq goal value
|
| /seL4-l4v-master/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceBaseFunctor.sml | [all...] |
| H A D | vars_as_resourceFunctor.sml | 1498 val pre = (fst o dest_imp o concl) thm1 value
1948 val pre = (rand o rator o rator o fst o dest_imp o concl) thm1 value
2206 val (pre,post) = dest_var_res_prog_cond_best_local_action p1'; value
2277 val (pre,post) = dest_var_res_prog_cond_best_local_action p1'; value
2315 val (pre,thm1b) = if (aconv pre_pre pre_post) then (pre_pre,thm1a) else value
2317 val pre = mk_conj (pre_pre, pre_post); value
3802 fun pre (l, (s1, guard, before_flag, continue_simp, cL)) = function
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 627 val pre = th |> concl |> rator |> rand value
|