diff options
Diffstat (limited to 'cheri/sail_latex/sailfnMEMwconditionalwrapper.tex')
| -rw-r--r-- | cheri/sail_latex/sailfnMEMwconditionalwrapper.tex | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/cheri/sail_latex/sailfnMEMwconditionalwrapper.tex b/cheri/sail_latex/sailfnMEMwconditionalwrapper.tex deleted file mode 100644 index 04ce8389..00000000 --- a/cheri/sail_latex/sailfnMEMwconditionalwrapper.tex +++ /dev/null @@ -1,11 +0,0 @@ -function #\hyperref[zMEMwzyconditionalzywrapper]{MEMw\_conditional\_wrapper}#(addr, size, data) = - { - /* require that writes don't cross capability #\hyperref[zboundaries]{boundaries}# (should be true due to mips alignment requirements) */ - assert((addr & cap_addr_mask) == ((addr + #\hyperref[ztozybits]{to\_bits}#(64, size - 1)) & cap_addr_mask)); - #\hyperref[zMEMeazyconditional]{MEMea\_conditional}#(addr, size); - success = #\hyperref[zMEMvalzyconditional]{MEMval\_conditional}#(addr,size,#\hyperref[zreversezyendianness]{reverse\_endianness}#(data)); - if success then - /* On cheri non-capability writes must clear the corresponding tag */ - #\hyperref[zMEMwzytag]{MEMw\_tag}#(addr & cap_addr_mask, false); - success; - } |