Searched defs:pc (Results 1 - 25 of 48) sorted by path

12

/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/
H A DarmScript.sml192 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/v4/
H A DarmScript.sml237 and pc = n2w (4 * exceptions2num type):word32 in type
253 and pc = REG_READ r.reg usr 15w in value
H A Darm_evalLib.sml764 let val pc = eval_word (get_pc (#reg x)) in value
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_parserLib.sml3101 val pc = bit 7 high_bits value
3174 val pc = bit 7 high_bits value
4553 val pc = enc_pc n enc value
[all...]
H A Darm_random_testingLib.sml111 val pc = mk_word4 15 value
H A Darm_stepLib.sml661 val pc = restr_eval (mk_comb (registers,pc_tm)) value
[all...]
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sml584 val pc = armML.arm_state_registers s1 value
[all...]
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/
H A Dproblem-set-1-answers.lisp231 (defun pc (s) (nth 0 s)) function
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/
H A DarmAssemblerLib.sml31 val pc = ref 0 value
124 val pc = ref 0 value
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/
H A Darm8AssemblerLib.sml58 val pc = ref 0 value
132 val pc = ref 0 value
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/decompiler/
H A Dm0_core_decompLib.sml65 val pc = Term.mk_var ("pc", ``:word32``) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/
H A Dm0AssemblerLib.sml26 val pc = ref 0 value
130 val pc = ref 0 value
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/
H A Dx64AssemblerLib.sml22 val pc = ref 0 value
108 val pc = ref 0 value
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/decompiler/
H A DdecompilerLib.sml827 val pc = get_pc () value
1568 val pc = get_pc() value
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml137 val pc = mk_var("r15",``:word32``) value
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_bytecode_stepScript.sml1232 val pc = iprint |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand value
1255 val pc = iparse |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand value
1284 val pc = ieof |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand value
H A Dlisp_correctnessScript.sml61 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 Dlisp_initScript.sml79 val pc = find_term (can (match_term (``zPC xx``))) (cdr (concl th)) value
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/soundness-thm/
H A Dmilawa_soundnessScript.sml25 val pc = find_term (can (match_term ``zPC xxx``)) (concl th |> rand) value
/seL4-l4v-master/HOL4/src/1/
H A DPmatch.sml131 let val (pc,args) = strip_comb p value
/seL4-l4v-master/HOL4/src/tfl/src/
H A DInduction.sml81 let val (pc,args) = strip_comb p value
/seL4-l4v-master/HOL4/tools/Holmake/
H A Dinternal_functions.sml115 val pc = sub(patss, i) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_progLib.sml23 val pc = Term.prim_mk_const {Thy = "arm", Name = "RName_PC"} value
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/
H A Dcore_decompilerLib.sml24 val pc = ref boolSyntax.F value
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/prog/
H A Dm0_progLib.sml23 val pc = Term.prim_mk_const {Thy = "m0", Name = "RName_PC"} value

Completed in 201 milliseconds

12