/seL4-l4v-master/HOL4/tools/Holmake/tests/gh604/final/ |
H A D | finalScript.sml | 3 val _ = new_theory "final";
|
/seL4-l4v-master/HOL4/tools/Holmake/tests/noprereqs/dir4/ |
H A D | finalScript.sml | 5 val _ = new_theory "final";
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Match.sig | 13 final : bool list} 19 final : bool vector}
|
H A D | regexpLib.sig | 15 final:bool vector,
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/ |
H A D | regexMarkedScript.sml | 49 (final (MEps) <=> F ) /\ 50 (final (MSym b _) <=> b ) /\ 51 (final (MAlt p q) <=> (final p) \/ (final q) ) /\ 52 (final (MSeq p q) <=> ((final p) /\ (empty q)) \/ (final q)) /\ 53 (final (MRep r) <=> final [all...] |
H A D | regexCachedMarkedScript.sml | 204 ((cempty s = (empty (UNCACHE_REG s))) /\ (cfinal s = (final (UNCACHE_REG s)))) 212 (CMREG_WELLFORMED (CMAlt e f p q) = (e = empty (UNCACHE_REG p) \/ empty (UNCACHE_REG q)) /\ (f = final (UNCACHE_REG p) \/ final (UNCACHE_REG q)) /\ CMREG_WELLFORMED p /\ CMREG_WELLFORMED q) /\ 213 (CMREG_WELLFORMED (CMSeq e f p q) = (e = empty (UNCACHE_REG p) /\ empty (UNCACHE_REG q)) /\ (f = (final (UNCACHE_REG p) /\ empty (UNCACHE_REG q)) \/ final (UNCACHE_REG q)) /\ CMREG_WELLFORMED p /\ CMREG_WELLFORMED q) /\ 214 (CMREG_WELLFORMED (CMRep f r) = (f = final (UNCACHE_REG r)) /\ CMREG_WELLFORMED r) 266 (!cmr. (CMREG_WELLFORMED cmr) ==> ((cfinal cmr) = final (UNCACHE_REG cmr)))
|
/seL4-l4v-master/l4v/misc/regression/ |
H A D | timeout_output | 17 echo final timing log:
|
/seL4-l4v-master/HOL4/src/proofman/ |
H A D | goalStack.sml | 71 Need both initial goal and final theorem in PROVED case, because 81 final : thm -> thm, 106 then GSTK{prop=POSED g, stack=[], final=f} 109 fun finalizer(GSTK{final,...}) = final; 116 | rotate(GSTK{prop, stack, final}) n = 125 else GSTK{prop=prop, final=final, 133 fun return(GSTK{stack={goals=[],validation}::rst, prop as POSED g,final}) = 137 (let val thm = final t [all...] |
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | MD5.sig | 14 val final : md5state -> Word8Vector.vector value
|
/seL4-l4v-master/HOL4/tools/Holmake/tests/gh604/ |
H A D | selftest.sml | 3 val _ = OS.FileSys.chDir "final"
|
/seL4-l4v-master/seL4/src/arch/x86/object/ |
H A D | objecttype.c | 180 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final) argument 186 if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) { 196 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 206 if (final) { 222 if (final) { 230 if (final) { 236 if (final && cap_io_page_table_cap_get_capIOPTIsMapped(cap)) { 244 if (final) { 249 if (final && cap_ept_pml4_cap_get_capPML4IsMapped(cap)) { 256 if (final [all...] |
/seL4-l4v-master/seL4/include/arch/x86/arch/object/ |
H A D | objecttype.h | 18 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final); 31 finaliseCap_ret_t Mode_finaliseCap(cap_t cap, bool_t final);
|
/seL4-l4v-master/seL4/src/arch/arm/64/object/ |
H A D | objecttype.c | 138 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final) argument 144 if (final) { 157 if (final && cap_page_global_directory_cap_get_capPGDIsMapped(cap)) { 171 if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 176 if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 186 if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) { 194 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 211 if (final) { 221 if (final) { 226 if (final) { [all...] |
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | waaSimplScript.sml | 216 ��� branchFixP b f ��� f ��� (reduceTransSimpl aut).final` suffices_by ( 222 >> `���b f. infBranchOf run b ��� branchFixP b f ��� f ��� aut.final` 273 >> rpt strip_tac >> `f ��� aut.final` suffices_by metis_tac[] 290 >- (`���b x. infBranchOf run b ��� branchFixP b x ��� x ��� aut.final` 294 >> `aut.final = (reduceTransSimpl aut).final` by 495 equivalentStates final trans s s' = 496 (trans s = trans s') ��� (s ��� final = s' ��� final)`; 596 (* (FINITE s ��� s ��� ��� ��� P (REST s) ((mergeState final) (CHOIC [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sig | 36 (message, final state)
|
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleCombinSynt.sig | 23 (* final testing
|
H A D | mleDiophSynt.sig | 25 (* final testing
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | pegLib.sml | 77 fun final c = CONV_RULE function 82 {lookups = map final cs, fdom_thm = fdom_thm, applieds = fapps}
|
/seL4-l4v-master/seL4/include/arch/arm/arch/object/ |
H A D | objecttype.h | 18 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final);
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/object/ |
H A D | objecttype.h | 18 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final);
|
/seL4-l4v-master/seL4/src/arch/arm/32/object/ |
H A D | objecttype.c | 143 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final) argument 149 if (final) { 156 if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) { 163 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 222 if (final) { 230 if (final) { 236 if (final && cap_io_page_table_cap_get_capIOPTIsMapped(cap)) {
|
/seL4-l4v-master/seL4/src/object/ |
H A D | objecttype.c | 104 finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed) argument 109 return Arch_finaliseCap(cap, final); 114 if (final) { 123 if (final) { 137 if (final) { 169 if (final) { 183 if (final) { 216 if (final) { 243 if (final) {
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | regexpMatch.sig | 47 final : bool vector}
|
/seL4-l4v-master/seL4/src/arch/x86/64/object/ |
H A D | objecttype.c | 77 finaliseCap_ret_t Mode_finaliseCap(cap_t cap, bool_t final) argument 84 if (final && cap_pml4_cap_get_capPML4IsMapped(cap)) { 93 if (final && cap_pdpt_cap_get_capPDPTIsMapped(cap)) {
|
/seL4-l4v-master/seL4/src/arch/riscv/object/ |
H A D | objecttype.c | 71 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final) argument 86 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 105 if (final) {
|