diff options
Diffstat (limited to 'cheri/sail_latex/sailfncheckDDCPerms.tex')
| -rw-r--r-- | cheri/sail_latex/sailfncheckDDCPerms.tex | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/cheri/sail_latex/sailfncheckDDCPerms.tex b/cheri/sail_latex/sailfncheckDDCPerms.tex deleted file mode 100644 index 1675c666..00000000 --- a/cheri/sail_latex/sailfncheckDDCPerms.tex +++ /dev/null @@ -1,12 +0,0 @@ -function #\hyperref[zcheckDDCPerms]{checkDDCPerms}#(ddc : CapStruct, accessType: MemAccessType) = - { - if (#\hyperref[znot]{not}# (ddc.tag)) then - #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_TagViolation, 0b00000) - else if (ddc.sealed) then - #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_SealViolation, 0b00000); - match accessType { - Instruction => assert(false), /* Only data accesses use DDC */ - LoadData => if (~(ddc.permit_load)) then (#\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_PermitLoadViolation, 0b00000)), - StoreData => if (~(ddc.permit_store)) then (#\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_PermitStoreViolation, 0b00000)) - }; - } |