/seL4-l4v-master/HOL4/examples/countable/ |
H A D | countableScript.sml | 19 ``���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 D | smmu.c | 13 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 D | smmuv2.c | 467 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 D | QbfConv.sml | 47 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 D | QbfConv.sig | 40 (* [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 D | graphics_file.scala | 69 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 D | graphics_file.scala | 69 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 D | vspace.h | 71 #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 D | smmu.h | 34 void smmu_cb_delete_vspace(word_t cb, asid_t asid);
|
/seL4-l4v-master/seL4/include/drivers/smmu/ |
H A D | smmuv2.h | 426 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 D | cheriScript.sml | 8733 ("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 D | ml_bind.sml | 33 structure cb = Clipboard structure
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_decoderScript.sml | 80 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 D | x86_encodeLib.sml | 164 [("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 D | x64_decoderScript.sml | 106 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 D | x64_encodeLib.sml | 249 [("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 D | match_goal.sml | 185 fun cb p = (Conclusion,p,false) function 186 val bc = cb
|
H A D | match_goal.sig | 99 val cb : pattern -> matcher value
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | windows_specific.cpp | 263 startupInfo.cb = sizeof(startupInfo); 360 startupInfo.cb = sizeof(startupInfo);
|
/seL4-l4v-master/HOL4/examples/ |
H A D | taut.sml | 4987 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 D | Makefile | 232 rm -f *.aux *.toc *.bbl *.blg *.dvi *.log *.pstex* *.eps *.cb *.brf \
|
/seL4-l4v-master/seL4/src/arch/x86/32/ |
H A D | traps.S | 299 INT_HANDLER_WITHOUT_ERR_CODE(cb)
|
/seL4-l4v-master/HOL4/src/temporal/src/ |
H A D | Omega_AutomataScript.sml | 2175 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 D | traps.S | 391 INT_HANDLER_WITHOUT_ERR_CODE(cb,0)
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | config.guess | 1117 if test -f /usr/options/cb.name; then 1118 UNAME_REL=`sed -n 's/.*Version //p' </usr/options/cb.name`
|