Searched refs:guard (Results 1 - 25 of 55) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dcond_cleanLib.sml16 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 Dderive_specsLib.sml84 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 DGraphLangScript.sml191 (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 DtailrecScript.sml14 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 Ddeprecated.h124 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 Dmonadsyntax.sig28 guard : term option }
H A Dmonadsyntax.sml20 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 Dantiquote.scala26 "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dantiquote.scala26 "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
/seL4-l4v-10.1.1/seL4/src/kernel/
H A Dcspace.c141 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 DConversion.sml66 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 DreaderMonadScript.sml81 ignorebind = NONE, choice = NONE, guard = NONE, fail = NONE
H A Dselftest.sml108 guard = SOME ``OPTION_GUARD``})
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dcspace.tex86 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 DOmegaShell.sml121 * 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 DpatternMatchesSyntax.sig60 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 DpatternMatchesScript.sml79 - 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 DpatternMatchesSyntax.sml753 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 DpatternMatchesLib.sig58 (* 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 DboolSimps.sig19 those of the same guard or
/seL4-l4v-10.1.1/seL4/src/object/
H A Dobjecttype.c343 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 Dfor_monadicScript.sml30 guard = NONE, fail = NONE, choice = NONE
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootLib.sig95 (* 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 Dx64_opsemScript.sml421 (\ (rip,guard,new_ecx).
424 (if ~(new_ecx = 0w) /\ guard
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_evalScript.sml337 if exp = Sym "nil" then (* guard is false *)
343 else (* guard is true *)

Completed in 300 milliseconds

123