| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | rtsentry.cpp | 147 for (struct _entrypts *ep = entryPtTable; ep->entry != NULL; ep++)
149 if (strcmp(entryName, ep->name) == 0)
151 polyRTSFunction entry = ep->entry;
|
| /seL4-l4v-10.1.1/l4v/proof/infoflow/tools/ |
| H A D | authority2infoflow-CaML.ml | 147 let f = (fun ep -> is_in g (x,SyncSend,ep)) in
154 let f = (fun ep -> is_in g (x,Receive,ep)) in
191 let f = (fun ep -> is_in g (l,SyncSend,ep)||is_in g (l,ASyncSend,ep) ) in
200 let f = (fun ep -> is_in g (l,Reset,ep) ) in
209 (those_is_in_such2 (nodes g) (fun ep
[all...] |
| /seL4-l4v-10.1.1/seL4/include/object/ |
| H A D | objecttype.h | 37 exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | envTools.sml | 112 val ep = env_prefix state q' iet value
113 val (ep',(_,_)) = dest_env iet
114 val (ep'',(_,_)) = dest_env ep'
115 val th = MP (ISPECL [ep'',q,q',s,s'] ENV_SWAP)
|
| H A D | lzConv.sml | 592 val ep = mk_exists{Bvar=Bvar, Body=disj1}
594 val ep_or_eq = mk_disj{disj1=ep, disj2=eq}
597 val Pth = EXISTS(ep,Bvar) aP
605 val e1 = CHOOSE (Bvar,ASSUME ep) th1
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | exportLib.sml | 65 val pat = ``GraphFunction inps outps gg ep``
69 val ep = tm |> rand |> numSyntax.int_of_term value
73 in (xs,ys,gs,ep) end
|
| H A D | GraphLangScript.sml | 114 | SOME (GraphFunction inps outps graph1 ep) =>
115 {(NextNode ep, init_vars inps inputs st, fname) :: stack})`;
122 | SOME (GraphFunction inps outps graph ep) =>
|
| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | notifications.tex | 26 capabilities (see \autoref{sec:ep-badges}). As with \obj{Endpoint}
|
| H A D | ipc.tex | 117 \subsection{Endpoint Badges\label{s:ep-badge}}
118 \label{sec:ep-badges}
|
| H A D | cspace.tex | 88 can also create a badged capability (see \autoref{sec:ep-badges})
232 created (see \autoref{s:ep-badge}, \autoref{s:notif-badge}). This new, badged capability to the same object is treated as
|
| /seL4-l4v-10.1.1/seL4/src/object/ |
| H A D | objecttype.c | 612 performInvocation_Endpoint(endpoint_t *ep, word_t badge, argument
616 sendIPC(block, call, badge, canGrant, NODE_STATE(ksCurThread), ep);
|
| H A D | cnode.c | 329 endpoint_t* ep = (endpoint_t*) local
331 cancelBadgedSends(ep, badge);
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | prog_x86Script.sml | 39 x86_2set' (rs,st,ep,ms) (r,e,s,m,i) =
42 (if ep then {xEIP e} else {}) UNION
53 \\ `?rs st ep ms. y = (rs,st,ep,ms)` by METIS_TAC [PAIR]
120 \\ `?rs st ep m st. y = (rs,st,ep,m)` by METIS_TAC [PAIR]
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | prog_x64Script.sml | 41 x64_2set' (rs,st,ep,ms) (r,e,s,m,i) =
44 (if ep then {zRIP e} else {}) UNION
55 \\ `?rs st ep ms. y = (rs,st,ep,ms)` by METIS_TAC [PAIR]
123 \\ `?rs st ep m st. y = (rs,st,ep,m)` by METIS_TAC [PAIR]
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 1567 val ep = mk_exists (x,P) value
1569 val Pth = EXISTS(ep,x)(ASSUME P)
1575 val e1 = CHOOSE (x,ASSUME ep) th1 and e2 = CHOOSE (x,ASSUME eq) th2
1576 val thm2 = DISJ_CASES (ASSUME(mk_disj(ep,eq))) e1 e2
1577 val imp2 = DISCH (mk_disj(ep,eq)) thm2
1591 val ep = mk_exists(x,P) value
1592 val tm = mk_disj(ep,Q)
1597 val thm1 = DISJ_CASES (ASSUME tm) (CHOOSE(x,ASSUME ep)th1) th2
1599 val Pth = EXISTS(ep,x)(ASSUME P) and Qth = ASSUME Q
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Conv.sml | 651 ** val ep = mk_exists {Bvar = Bvar, Body = disj1}
653 ** val ep_or_eq = mk_disj {disj1 = ep, disj2 = eq}
656 ** val Pth = EXISTS (ep, Bvar) aP
664 ** val e1 = CHOOSE (Bvar, ASSUME ep) th1
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | polytypicLib.sml | 298 fun ep x = map fst o filter (curry op= x o snd) function
302 union (all_pairs (x::ep x pairs) (y::sp y pairs)) pairs;
|