diff options
Diffstat (limited to 'cheri/sail_latex/sailfnSignalException.tex')
| -rw-r--r-- | cheri/sail_latex/sailfnSignalException.tex | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/cheri/sail_latex/sailfnSignalException.tex b/cheri/sail_latex/sailfnSignalException.tex deleted file mode 100644 index a91f582e..00000000 --- a/cheri/sail_latex/sailfnSignalException.tex +++ /dev/null @@ -1,18 +0,0 @@ -function #\hyperref[zSignalException]{SignalException}# (ex) = - { - if (#\hyperref[znot]{not}# (CP0Status.#\hyperref[zEXL]{EXL}#())) then { - let pc = PC in - let pcc = #\hyperref[zcapRegToCapStruct]{capRegToCapStruct}#(PCC) in - let (success, epcc) = #\hyperref[zsetCapOffset]{setCapOffset}#(pcc, pc) in - if (success) then - EPCC = #\hyperref[zcapStructToCapReg]{capStructToCapReg}#(epcc) - else - EPCC = #\hyperref[zcapStructToCapReg]{capStructToCapReg}#(#\hyperref[zintzytozycap]{int\_to\_cap}#(#\hyperref[ztozybits]{to\_bits}#(64, #\hyperref[zgetCapBase]{getCapBase}#(pcc)) + #\hyperref[zunsigned]{unsigned}#(pc))); - }; - - nextPCC = KCC; - delayedPCC = KCC; /* always write delayedPCC together with nextPCC so - that non-capability branches don't override PCC */ - let base = #\hyperref[zgetCapBase]{getCapBase}#(#\hyperref[zcapRegToCapStruct]{capRegToCapStruct}#(KCC)) in - #\hyperref[zSignalExceptionMIPS]{SignalExceptionMIPS}#(ex, #\hyperref[ztozybits]{to\_bits}#(64, base)); - } |