/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | cond_cleanLib.sml | 16 val (guard,next1,next2) = dest_IF next value 17 in (guard,dest_ASM next1, dest_ASM next2) end 24 val (guard,asm1,asm2) = dest_IMPL_INST_IF_ASM_ASM th value 64 val (guard,_,(s2,u2,j2)) = dest_IMPL_INST_IF_ASM_ASM th value 68 val assum = negate_guard guard 75 val (guard,_,(s2,u2,j2)) = dest_IMPL_INST_IF_ASM_ASM th value 83 val (guard,(s1,u1,j1),_) = dest_IMPL_INST_IF_ASM_ASM th value 87 val assum = guard 94 val (guard,(s1,u1,j1),_) = dest_IMPL_INST_IF_ASM_ASM th value
|
H A D | derive_specsLib.sml | 84 val guard = cdr (find_term (can (match_term ``GUARD n b``)) (concl th)) value 85 in (th,bool_normal_form guard) end handle HOL_ERR _ => (th,T) 91 fun guard_conj guard (th,pre) = 92 (th,if resets_status_bits th then pre else bool_normal_form (mk_conj(pre,guard))) 105 fun aux (p:int) (seen:int list) (guard:term) = 106 if mem (p,guard) (!aux_calls) then TRACE_CUT p else 107 (aux_calls := (p,guard)::(!aux_calls); 113 (* combine with current guard if theorem does not reset status bits *) 114 val xs = map (guard_conj guard) xs
|
H A D | GraphLangScript.sml | 191 (exec_next locs (IF guard n1 n2) s t w call = 192 if guard s then exec_next locs n1 s t w call 366 !guard. IMPL_INST code locs (Inst pc1 assert1 (IF guard next1 next2))``, 372 !guard. IMPL_INST code locs 373 (Inst pc1 (\s. if guard s then assert1 s else assert2 s) 374 (IF guard next1 next2))``, 379 (Inst pc assert (IF guard (ASM (SOME s1) up1 j1) 382 (Inst pc assert (IF guard (ASM (SOME (\s. guard [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | tailrecScript.sml | 14 TAILREC_PRE f1 guard precondition (x:'a) = 15 (!k. (!m. m < k ==> guard (FUNPOW f1 m x)) ==> precondition (FUNPOW f1 k x)) /\ 16 ?n. ~guard (FUNPOW f1 n x)`; 69 ``!step guard side. 70 (?R. WF R /\ !x. guard x ==> R (step x) x) /\ (!x. side x) ==> 71 !x. TAILREC_PRE step guard side x = T``,
|
/seL4-l4v-10.1.1/seL4/libsel4/include/sel4/ |
H A D | deprecated.h | 124 typedef seL4_Word seL4_CapData_t SEL4_DEPRECATED("Badge and guard data are just seL4_Word type"); 131 static inline SEL4_DEPRECATED("Use seL4_CNode_CapData_new().words[0]") seL4_Word seL4_CapData_Guard_new(seL4_Word guard, seL4_Word bits) argument 133 return seL4_CNode_CapData_new(guard, bits).words[0];
|
/seL4-l4v-10.1.1/HOL4/src/monad/ |
H A D | monadsyntax.sig | 28 guard : term option }
|
H A D | monadsyntax.sml | 20 guard : term option } 26 fun toSexp {bind,ignorebind,unit,fail,choice,guard} = 30 Option (Option.map Term guard)] 39 fail = determOpt failopt, guard = determOpt guardopt, 358 val {bind,ignorebind,unit,fail,choice,guard} = getMI fname s 366 Option.app (fn g => ovl("assert", g)) guard 371 val {bind,ignorebind,unit,fail,choice,guard} = getMI fname s 379 Option.app (rmovl "assert") guard 452 guard = SOME (prim_mk_const {Name = "OPTION_GUARD", Thy = "option"}),
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | antiquote.scala | 26 "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | antiquote.scala | 26 "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
|
/seL4-l4v-10.1.1/seL4/src/kernel/ |
H A D | cspace.c | 141 word_t radixBits, guardBits, levelBits, guard; local 168 guard = (capptr >> ((n_bits - guardBits) & MASK(wordRadix))) & MASK(guardBits); 169 if (unlikely(guardBits > n_bits || guard != capGuard)) {
|
/seL4-l4v-10.1.1/HOL4/examples/STE/ |
H A D | Conversion.sml | 66 fun TrajForm (guard:term, n:string, value:term, START, END) = 69 ``((Is_1 ^node) WHEN (^value/\ ^guard)) 71 ((Is_0 ^node) WHEN ~(^value /\ ^guard))``;
|
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/ |
H A D | readerMonadScript.sml | 81 ignorebind = NONE, choice = NONE, guard = NONE, fail = NONE
|
H A D | selftest.sml | 108 guard = SOME ``OPTION_GUARD``})
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | cspace.tex | 86 the original and a different guard (see 92 capability has the same badge and guard as the original. 324 also carries a \emph{guard} value, explained in 335 then compares that \obj{CNode}'s \emph{guard} value against the most 354 all levels, various guard and radix sizes and internal CNode 363 \item a top level CNode object with a 12-bit guard set to 0x000 and 421 \item[Cap A.] The first CNode has a 4-bit guard set to 0x0, and an 428 \item[Cap B.] Again, the first CNode has a 4-bit guard set to 0x0, and 430 It also has a 4-bit guard of 0x0 and Cap B resides at index 436 of the second CNode. The third CNode has no guard an [all...] |
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaShell.sml | 121 * conditional expressions that repeat the same guard should have 122 the case-split done on the guard just once. *)
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesSyntax.sig | 60 abstracted variables for the pattern, guard and right hand side 67 abstracted variables for the pattern, guard and right hand side 135 it extracts the pattern [f x1 ... xn] and guard [g1 x1 ... xn /\ ...]. 139 the guard. It gets the list of free variables and the pattern.
|
H A D | patternMatchesScript.sml | 79 - guard g 85 val PMATCH_ROW_COND_def = zDefine `PMATCH_ROW_COND pat guard inp v = 86 (pat v = inp) /\ (guard v)` 89 val PMATCH_ROW_def = zDefine `PMATCH_ROW pat guard rhs i = 90 (OPTION_MAP rhs (some v. PMATCH_ROW_COND pat guard i v))` 218 ``PMATCH_ROW_COND pat guard inp v = 219 ((inp = pat v) /\ (guard v))``, 1176 var to the guard. *) 1207 and add the guard in form of a conditional. 1208 Notice that all the rows after the guard ar [all...] |
H A D | patternMatchesSyntax.sml | 753 fun pmatch_printer_fix_wildcards (vars, pat, guard, rh) = let 763 variant (free_varsl [pat, guard, rh]) (mk_var("_", oneSyntax.one_ty)) 768 val guard' = Term.subst fake_subst guard 771 (vars', pat', guard', rh') 772 end handle HOL_ERR _ => (vars, pat, guard, rh) 808 fun pp_row (vars, pat, guard, rh) = 833 (if aconv guard T then nothing 836 sys (Top, Top, Top) (d - 1) guard) >>
|
H A D | patternMatchesLib.sig | 58 (* Use same variable names for pattern, guard and rhs *) 61 (* Rename pattern variables unused in guard and rhs into 267 the guard is T. See below for functions using this 297 of triples (`bound-vars`, `pattern`, `guard`) *)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | boolSimps.sig | 19 those of the same guard or
|
/seL4-l4v-10.1.1/seL4/src/object/ |
H A D | objecttype.c | 343 word_t guard, guardSize; local 353 guard = seL4_CNode_CapData_get_guard(w) & MASK(guardSize); 354 new_cap = cap_cnode_cap_set_capCNodeGuard(cap, guard);
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | for_monadicScript.sml | 30 guard = NONE, fail = NONE, choice = NONE
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootLib.sig | 95 (* group guard, inferences are just applied to 96 terms that satisfy this guard *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_opsemScript.sml | 421 (\ (rip,guard,new_ecx). 424 (if ~(new_ecx = 0w) /\ guard
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_evalScript.sml | 337 if exp = Sym "nil" then (* guard is false *) 343 else (* guard is true *)
|