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 160 milliseconds