1 files changed, 0 insertions, 46 deletions
diff --git a/cheri/sail_latex/sailsailfnexecuteCCallv.tex b/cheri/sail_latex/sailsailfnexecuteCCallv.tex
deleted file mode 100644
index 6a11ddac..00000000
--- a/cheri/sail_latex/sailsailfnexecuteCCallv.tex
+++ /dev/null
@@ -1,46 +0,0 @@
-function clause #\hyperref[zexecute]{execute}# (#\hyperref[zCCall]{CCall}#(cs, cb, 0b00000000001)) = /* selector=1 */
-{
-  /* Jump-like implementation of CCall that unseals arguments */
-  #\hyperref[zcheckCPtwousable]{checkCP2usable}#();
-  cs_val = #\hyperref[zreadCapReg]{readCapReg}#(cs);
-  cb_val = #\hyperref[zreadCapReg]{readCapReg}#(cb);
-  cs_cursor = #\hyperref[zgetCapCursor]{getCapCursor}#(cs_val);
-  if (#\hyperref[zregisterzyinaccessible]{register\_inaccessible}#(cs)) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_AccessSystemRegsViolation, cs)
-  else if (#\hyperref[zregisterzyinaccessible]{register\_inaccessible}#(cb)) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_AccessSystemRegsViolation, cb)
-  else if #\hyperref[znot]{not}# (cs_val.tag) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_TagViolation, cs)
-  else if #\hyperref[znot]{not}# (cb_val.tag) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_TagViolation, cb)
-  else if #\hyperref[znot]{not}# (cs_val.sealed) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_SealViolation, cs)
-  else if #\hyperref[znot]{not}# (cb_val.sealed) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_SealViolation, cb)
-  else if ((cs_val.otype) != (cb_val.otype)) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_TypeViolation, cs)
-  else if #\hyperref[znot]{not}# (cs_val.permit_ccall) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_PermitCCallViolation, cs)
-  else if #\hyperref[znot]{not}# (cb_val.permit_ccall) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_PermitCCallViolation, cb)
-  else if #\hyperref[znot]{not}# (cs_val.permit_execute) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_PermitExecuteViolation, cs)
-  else if (cb_val.permit_execute) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_PermitExecuteViolation, cb)
-  else if (cs_cursor < #\hyperref[zgetCapBase]{getCapBase}#(cs_val)) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_LengthViolation, cs)
-  else if (cs_cursor >= #\hyperref[zgetCapTop]{getCapTop}#(cs_val)) then
-    #\hyperref[zraisezyctwozyexception]{raise\_c2\_exception}#(CapEx_LengthViolation, cs)
-  else
-    {
-      #\hyperref[zexecutezybranchzypcc]{execute\_branch\_pcc}#({cs_val with
-        sealed=false,
-        otype=#\hyperref[zzzeros]{zeros}#()
-      });
-      inCCallDelay  = 0b1;
-      C26 = #\hyperref[zcapStructToCapReg]{capStructToCapReg}#({cb_val with
-        sealed=false,
-        otype=#\hyperref[zzzeros]{zeros}#()
-      });
-    }
-}