Searched refs:cb (Results 1 - 25 of 34) sorted by relevance

12

/seL4-l4v-master/HOL4/examples/countable/
H A DcountableScript.sml19 ``���p1 p2 ca ca' cb cb'. (p1 = p2) ��� (���x. (x = FST p2) ��� (ca x = ca' x)) ��� (���x. (x = SND p2) ��� (cb x = cb' x))
20 ��� (count_prod_aux ca cb p1 = count_prod_aux ca' cb' p2)``,
/seL4-l4v-master/seL4/src/arch/arm/object/
H A Dsmmu.c13 word_t cb = cap_cb_cap_get_capCB(cap); local
14 cte_t *cbSlot = smmuStateCBNode + cb;
136 /*binding the sid to cb in SMMU*/
139 * copy of the given cb cap in sid's cnode*/
189 word_t index, depth, cb; local
211 cb = getSyscallArg(0, buffer);
216 if (cb >= SMMU_MAX_CB) {
220 userError("Rejecting request for CB %u. CB is greater than or equal to SMMU_MAX_CB.", (int)cb);
223 if (smmuStateCBTable[cb]) {
225 userError("Rejecting request for CB %u. Already active.", (int)cb);
258 word_t cb; local
352 word_t cb = cap_cb_cap_get_capCB(cap); local
366 smmu_cb_delete_vspace(word_t cb, asid_t asid) argument
[all...]
/seL4-l4v-master/seL4/src/drivers/smmu/
H A Dsmmuv2.c467 void smmu_cb_assign_vspace(word_t cb, vspace_root_t *vspace, asid_t asid) argument
470 uint32_t vmid = cb;
493 smmu_write_reg32(SMMU_GR1_PPTR, SMMU_CBA2Rn(cb), reg);
511 smmu_write_reg32(SMMU_GR1_PPTR, SMMU_CBARn(cb), reg);
513 smmu_write_reg32(SMMU_CBn_BASE_PPTR(cb), SMMU_CBn_TCR, smmu_stage_table_config.tcr[0]);
518 smmu_write_reg32(SMMU_CBn_BASE_PPTR(cb), SMMU_CBn_TCR2, smmu_stage_table_config.tcr[1]);
519 smmu_write_reg64(SMMU_CBn_BASE_PPTR(cb), SMMU_CBn_TTBR1, smmu_stage_table_config.ttbr[1]);
523 smmu_write_reg64(SMMU_CBn_BASE_PPTR(cb), SMMU_CBn_TTBR0, smmu_stage_table_config.ttbr[0]);
526 smmu_write_reg32(SMMU_CBn_BASE_PPTR(cb), SMMU_CBn_MAIR0, smmu_stage_table_config.mair[0]);
527 smmu_write_reg32(SMMU_CBn_BASE_PPTR(cb), SMMU_CBn_MAIR
534 smmu_cb_disable(word_t cb, asid_t asid) argument
543 smmu_sid_bind_cb(word_t sid, word_t cb) argument
584 smmu_tlb_invalidate_cb(int cb, asid_t asid) argument
601 smmu_tlb_invalidate_cb_va(int cb, asid_t asid, vptr_t vaddr) argument
631 smmu_cb_read_fault_state(int cb, uint32_t *status, word_t *address) argument
637 smmu_cb_clear_fault_state(int cb) argument
[all...]
/seL4-l4v-master/HOL4/src/HolQbf/
H A DQbfConv.sml47 fun last_quant_seq_conv cq cb = let
50 HOL_ERR {origin_function="RAND_CONV",...} => cb t
53 fun last_forall_seq_conv cq cb = let
61 handle Innermost => last_quant_seq_conv cq cb tm
62 else cb tm
H A DQbfConv.sig40 (* [last_quant_seq_conv cq cb] applies cb under the quantifier prefix and
42 Q1 x1. Q2 x2. ... Qn xn. P --> cq (Q1 x1. cq (Q2 x2. ... cq (Qn. xn. cb P))))
46 (* applies cb under the quantifier prefix, and then, if the innermost
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dgraphics_file.scala69 val cb = writer.getDirectContent()
70 val tp = cb.createTemplate(width, height)
76 cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dgraphics_file.scala69 val cb = writer.getDirectContent()
70 val tp = cb.createTemplate(width, height)
76 cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
/seL4-l4v-master/seL4/include/arch/arm/arch/64/mode/kernel/
H A Dvspace.h71 #define cap_vtable_root_ptr_set_mappedCB(_c, cb) \
72 cap_page_upper_directory_cap_ptr_set_capPUDMappedCB(_c, cb)
113 #define cap_vtable_root_ptr_set_mappedCB(_c, cb) \
114 cap_page_global_directory_cap_ptr_set_capPGDMappedCB(_c, cb)
/seL4-l4v-master/seL4/include/arch/arm/arch/object/
H A Dsmmu.h34 void smmu_cb_delete_vspace(word_t cb, asid_t asid);
/seL4-l4v-master/seL4/include/drivers/smmu/
H A Dsmmuv2.h426 void smmu_cb_assign_vspace(word_t cb, vspace_root_t *vspace, asid_t asid);
427 void smmu_sid_bind_cb(word_t sid, word_t cb);
430 void smmu_tlb_invalidate_cb(int cb, asid_t asid);
431 void smmu_tlb_invalidate_cb_va(int cb, asid_t asid, vptr_t vaddr);
432 void smmu_cb_disable(word_t cb, asid_t asid);
436 void smmu_cb_read_fault_state(int cb, uint32_t *status, word_t *address);
437 void smmu_cb_clear_fault_state(int cb);
/seL4-l4v-master/HOL4/examples/l3-machine-code/cheri/
H A DcheriScript.sml8733 ("register_inaccessible",Var("cb",FTy 5),
8744 Var("cb",FTy 5)]),qVar"state"))))
8830 ("dfn'CGetBase",TP[Var("rd",FTy 5),Var("cb",FTy 5)],
8843 (Call("register_inaccessible",ATy(qTy,bTy),Var("cb",FTy 5)),
8849 Var("cb",FTy 5)]),qVar"state"))],
8858 Var("cb",FTy 5)),qVar"state")),Var("rd",FTy 5)]),
8862 ("dfn'CGetOffset",TP[Var("rd",FTy 5),Var("cb",FTy 5)],
8875 (Call("register_inaccessible",ATy(qTy,bTy),Var("cb",FTy 5)),
8881 Var("cb",FTy 5)]),qVar"state"))],
8890 Var("cb",FT
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A Dml_bind.sml33 structure cb = Clipboard structure
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_decoderScript.sml80 else if MEM name ["ib";"cb";"rel8";"imm8"] then (* 8-bit immediate or address *)
138 if name = "rel8" then sw2sw:word8 ->word32 (b2w g "cb") else
301 " EB cb | JMP rel8 ";
303 " 74 cb | JE rel8 ";
304 " 75 cb | JNE rel8 ";
307 " 78 cb | JS rel8 ";
308 " 79 cb | JNS rel8 ";
311 " 77 cb | JA rel8 ";
312 " 76 cb | JNA rel8 ";
315 " 72 cb | J
[all...]
H A Dx86_encodeLib.sml164 [("cb",signed_hex 2 (Arbint.fromString y))]
189 if mem x ["id","iw","ib","cb","cw","cd"] then find x ts else
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_decoderScript.sml106 else if MEM name ["ib";"cb";"rel8";"imm8"] then (* 8-bit immediate or address *)
176 if name = "rel8" then sw2sw:word8 ->word64 (b2w g "cb") else
378 " EB cb | JMP rel8 ";
380 " 74 cb | JE rel8 ";
381 " 75 cb | JNE rel8 ";
384 " 78 cb | JS rel8 ";
385 " 79 cb | JNS rel8 ";
388 " 77 cb | JA rel8 ";
389 " 76 cb | JNA rel8 ";
392 " 72 cb | J
[all...]
H A Dx64_encodeLib.sml249 [("cb",signed_hex 2 (Arbint.fromString y))]
279 if mem x ["iq","id","iw","ib","cb","cw","cd"] then find x ts else
/seL4-l4v-master/HOL4/src/1/
H A Dmatch_goal.sml185 fun cb p = (Conclusion,p,false) function
186 val bc = cb
H A Dmatch_goal.sig99 val cb : pattern -> matcher value
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dwindows_specific.cpp263 startupInfo.cb = sizeof(startupInfo);
360 startupInfo.cb = sizeof(startupInfo);
/seL4-l4v-master/HOL4/examples/
H A Dtaut.sml4987 cb /\ a3 \/
4989 ca /\ ~cb /\ a0 /\ a1 /\ a2 \/
4990 ca /\ ~cb /\ ~a0 /\ a3) /\
4992 cb /\ a2 \/
4994 ca /\ ~cb /\ a0 /\ a1 /\ ~a2 \/
4995 ca /\ ~cb /\ ~a0 /\ a1 /\ a2 \/
4996 ca /\ ~cb /\ ~a1 /\ a2) /\
4998 cb /\ a1 \/
5000 ca /\ ~cb /\ ~a0 /\ a1 /\ ~a3 \/
5001 ca /\ ~cb /\ a
[all...]
/seL4-l4v-master/seL4/manual/
H A DMakefile232 rm -f *.aux *.toc *.bbl *.blg *.dvi *.log *.pstex* *.eps *.cb *.brf \
/seL4-l4v-master/seL4/src/arch/x86/32/
H A Dtraps.S299 INT_HANDLER_WITHOUT_ERR_CODE(cb)
/seL4-l4v-master/HOL4/src/temporal/src/
H A DOmega_AutomataScript.sml2175 let val cb = ���?q. value
2180 ���(NEXT (\t0:num. ^cb)) t0 =
2326 let val cb = ���?q. value
2331 ���(phi SUNTIL (\t0:num. ^cb)) t0 =
2595 let val cb = ���?q. value
2600 ���((\t0:num. ^cb) BEFORE phi) t0 =
2926 let val cb = ���?q. value
2931 ���(phi UNTIL (\t0:num. ^cb)) t0 =
2956 (* in the other case, we have phi UNTIL cb = phi SUNITL cb *)
3050 let val cb = ���?q. value
3371 let val cb = ���?q. value
3675 let val cb = ���?q. value
[all...]
/seL4-l4v-master/seL4/src/arch/x86/64/
H A Dtraps.S391 INT_HANDLER_WITHOUT_ERR_CODE(cb,0)
/seL4-l4v-master/HOL4/polyml/
H A Dconfig.guess1117 if test -f /usr/options/cb.name; then
1118 UNAME_REL=`sed -n 's/.*Version //p' </usr/options/cb.name`

Completed in 321 milliseconds

12