diff options
Diffstat (limited to 'cheri/sail_latex/sailfnexecuteClearRegs.tex')
| -rw-r--r-- | cheri/sail_latex/sailfnexecuteClearRegs.tex | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/cheri/sail_latex/sailfnexecuteClearRegs.tex b/cheri/sail_latex/sailfnexecuteClearRegs.tex deleted file mode 100644 index 5283918f..00000000 --- a/cheri/sail_latex/sailfnexecuteClearRegs.tex +++ /dev/null @@ -1,21 +0,0 @@ -function clause #\hyperref[zexecute]{execute}# (#\hyperref[zClearRegs]{ClearRegs}#(regset, m)) = -{ - if ((regset == CLo) | (regset == CHi)) then - #\hyperref[zcheckCPtwousable]{checkCP2usable}#(); - if (regset == CHi) then - foreach (i from 0 to 15) - let r = #\hyperref[ztozybits]{to\_bits}#(5, i+16) in - if (m[i] & #\hyperref[zregisterzyinaccessible]{register\_inaccessible}#(r)) then - #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_AccessSystemRegsViolation, r); - foreach (i from 0 to 15) - if (m[i]) then - match regset { - GPLo => #\hyperref[zwGPR]{wGPR}#(#\hyperref[ztozybits]{to\_bits}#(5, i)) = #\hyperref[zzzeros]{zeros}#(), - GPHi => #\hyperref[zwGPR]{wGPR}#(#\hyperref[ztozybits]{to\_bits}#(5, i+16)) = #\hyperref[zzzeros]{zeros}#(), - CLo => if i == 0 then - DDC = #\hyperref[zcapStructToCapReg]{capStructToCapReg}#(null_cap) - else - #\hyperref[zwriteCapReg]{writeCapReg}#(#\hyperref[ztozybits]{to\_bits}#(5, i)) = null_cap, - CHi => #\hyperref[zwriteCapReg]{writeCapReg}#(#\hyperref[ztozybits]{to\_bits}#(5, i+16)) = null_cap - } -} |