Searched refs:SPSR (Results 1 - 10 of 10) sorted by relevance
/seL4-l4v-master/seL4/src/arch/arm/64/ |
H A D | traps.S | 20 #define SPSR spsr_el2 define 27 #define SPSR spsr_el1 define 90 /* Store thread's SPSR, LR, and SP */ 93 mrs x23, SPSR
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | priv_constraints_spsrScript.sml | 11 (* CONSTRAINTS ON SPSR FLAGS IN PRIVILEGED MODE *)
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | assemblerML.sml | 877 h ^ reg2string (#Rd y) ^ ", " ^ (if #R y then "SPSR" else "CPSR") 887 h ^ (if #R y then "SPSR" else "CPSR") ^
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
H A D | arm.sml | 2083 fun SPSR () = function 2086 ("SPSR: BadMode: " ^ (BitsN.toHexString(#M((!CPSR) : PSR)))) 2095 | _ => raise UNPREDICTABLE "SPSR"; 2097 fun write'SPSR value = 2100 ("SPSR: BadMode: " ^ (BitsN.toHexString(#M((!CPSR) : PSR)))) 2109 | _ => raise UNPREDICTABLE "SPSR"; 2281 val x = SPSR () 2284 write'SPSR 2292 val x = SPSR () 2295 write'SPSR [all...] |
H A D | armScript.sml | 1018 ("SPSR",qVar"state", 1029 CC[LS"SPSR: BadMode: ", 1045 Call("UNPREDICTABLE",CTy"exception",LS"SPSR")), 1049 ("write'SPSR",Var("value",CTy"PSR"), 1063 CC[LS"SPSR: BadMode: ", 1089 Call("UNPREDICTABLE",CTy"exception",LS"SPSR")), 1598 (Const("SPSR",ATy(qTy,PTy(CTy"PSR",qTy))), 1602 ("write'SPSR",ATy(qTy,qTy), 1617 (Const("SPSR",ATy(qTy,PTy(CTy"PSR",qTy))), 1621 ("write'SPSR",AT [all...] |
H A D | arm.sig | 678 val SPSR: unit -> PSR value 679 val write'SPSR: PSR -> unit
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/monadic-arm/ |
H A D | armScript.sml | 1570 ("SPSR", 1592 MU(CC[LS"SPSR: BadMode: ",sVar"v"], 1653 LS"SPSR")))]))))))))))) 1656 ("write'SPSR",Var("value",CTy"PSR"), 1678 MU(CC[LS"SPSR: BadMode: ",sVar"v"], 1752 LS"SPSR")))]))))))))))) 2883 MB(Const("SPSR",ATy(qTy,PTy(CTy"PSR",qTy))), 2887 ("write'SPSR",ATy(qTy,PTy(uTy,qTy)), 2901 MB(Const("SPSR",ATy(qTy,PTy(CTy"PSR",qTy))), 2905 ("write'SPSR",AT [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_opsemScript.sml | 2942 where <spec_reg> is APSR, CPSR or SPSR.
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_opsemScript.sml | 2966 where <spec_reg> is APSR, CPSR or SPSR.
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_stepLib.sml | 4059 val SPSR_rwt = EV [SPSR_def, BadMode, CPSR_lem] [] [] ``SPSR`` |> hd
|
Completed in 244 milliseconds