| /seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/soundness-thm/ |
| H A D | milawa_soundnessScript.sml | 25 val pc = find_term (can (match_term ``zPC xxx``)) (concl th |> rand) value
|
| /seL4-l4v-master/seL4/include/machine/ |
| H A D | profiler.h | 64 word_t pc; member in struct:__anon158
|
| /seL4-l4v-master/seL4/src/machine/ |
| H A D | profiler.c | 72 void profiler_record_sample(word_t pc) argument
129 void profiler_record_sample(word_t pc) argument
[all...] |
| /seL4-l4v-master/HOL4/polyml/libpolyml/ |
| H A D | gc_progress.cpp | 71 void gcProgressSetPercent(unsigned pc) argument
|
| H A D | profiling.cpp | 376 void incrementCountAsynch(POLYCODEPTR pc) argument
|
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/ |
| H A D | types.h | 19 seL4_Word pc, sp, cpsr, r0, r1, r8, r9, r10, r11, r12; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/ |
| H A D | types.h | 19 seL4_Word pc, sp, cpsr, r0, r1, r8, r9, r10, r11, r12; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
| H A D | problem-set-1-answers.lisp | 231 (defun pc (s) (nth 0 s)) function
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | armAssemblerLib.sml | 31 val pc = ref 0 value
124 val pc = ref 0 value
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8AssemblerLib.sml | 58 val pc = ref 0 value
132 val pc = ref 0 value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/m0/decompiler/ |
| H A D | m0_core_decompLib.sml | 65 val pc = Term.mk_var ("pc", ``:word32``) value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0AssemblerLib.sml | 26 val pc = ref 0 value
130 val pc = ref 0 value
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_correctnessScript.sml | 61 val pc = READ_EVAL_PRINT_LOOP_BASE |> concl |> rand |> find_term (can (match_term ``p + n2w n``)) value
296 val pc = th |> concl |> rand |> find_term (can (match_term ``zPC x``)) value
454 val pc = th |> concl |> rand |> find_term (can (match_term ``p + n2w n``)) value
|
| H A D | lisp_initScript.sml | 79 val pc = find_term (can (match_term (``zPC xx``))) (cdr (concl th)) value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64AssemblerLib.sml | 22 val pc = ref 0 value
108 val pc = ref 0 value
[all...] |
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/ |
| H A D | types.h | 25 seL4_Word pc, sp, spsr, x0, x1, x2, x3, x4, x5, x6, x7, x8, x16, x17, x18, x29, x30; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/ |
| H A D | types.h | 29 seL4_Word pc; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | internal_functions.sml | 115 val pc = sub(patss, i) value
|
| /seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
| H A D | emit_eval.sml | 584 val pc = armML.arm_state_registers s1 value
[all...] |
| /seL4-l4v-master/seL4/src/kernel/ |
| H A D | thread.c | 52 word_t pc; local
55 setNextPC(NODE_STATE(ksCurThread), pc); local
|
| /seL4-l4v-master/HOL4/examples/ARM/v4/ |
| H A D | armScript.sml | 237 and pc = n2w (4 * exceptions2num type):word32 in type
253 and pc = REG_READ r.reg usr 15w in value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/mips/prog/ |
| H A D | mips_progLib.sml | 67 val pc = stateLib.gvar "pc" dword value
|
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | stack_analysisLib.sml | 81 val pc = get_pc_val pre value
97 val pc = get_pc_val pre1 value
159 val (pc,s,t) = state value
259 val (pc,s,t) = state value
[all...] |
| /seL4-l4v-master/HOL4/examples/ARM/arm6-verification/ |
| H A D | armScript.sml | 192 and pc = n2w (4 * exception2num type):word32 in type
208 and pc = REG_READ reg usr 15w in value
|
| /seL4-l4v-master/HOL4/examples/ARM/v7/ |
| H A D | arm_random_testingLib.sml | 111 val pc = mk_word4 15 value
|