Searched refs:final (Results 1 - 25 of 173) sorted by relevance

1234567

/seL4-l4v-master/HOL4/tools/Holmake/tests/gh604/final/
H A DfinalScript.sml3 val _ = new_theory "final";
/seL4-l4v-master/HOL4/tools/Holmake/tests/noprereqs/dir4/
H A DfinalScript.sml5 val _ = new_theory "final";
/seL4-l4v-master/HOL4/examples/formal-languages/regular/
H A DRegexp_Match.sig13 final : bool list}
19 final : bool vector}
H A DregexpLib.sig15 final:bool vector,
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexMarkedScript.sml49 (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 DregexCachedMarkedScript.sml204 ((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 Dtimeout_output17 echo final timing log:
/seL4-l4v-master/HOL4/src/proofman/
H A DgoalStack.sml71 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 DMD5.sig14 val final : md5state -> Word8Vector.vector value
/seL4-l4v-master/HOL4/tools/Holmake/tests/gh604/
H A Dselftest.sml3 val _ = OS.FileSys.chDir "final"
/seL4-l4v-master/seL4/src/arch/x86/object/
H A Dobjecttype.c180 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 Dobjecttype.h18 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 Dobjecttype.c138 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 DwaaSimplScript.sml216 ��� 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 Demit_eval.sig36 (message, final state)
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleCombinSynt.sig23 (* final testing
H A DmleDiophSynt.sig25 (* final testing
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/
H A DpegLib.sml77 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 Dobjecttype.h18 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final);
/seL4-l4v-master/seL4/include/arch/riscv/arch/object/
H A Dobjecttype.h18 finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final);
/seL4-l4v-master/seL4/src/arch/arm/32/object/
H A Dobjecttype.c143 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 Dobjecttype.c104 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 DregexpMatch.sig47 final : bool vector}
/seL4-l4v-master/seL4/src/arch/x86/64/object/
H A Dobjecttype.c77 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 Dobjecttype.c71 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) {

Completed in 235 milliseconds

1234567