From 938f06bc6c711ef3e777beaace7da8d4aee158b9 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 10 May 2018 17:38:36 +0100
Subject: Document the register_inaccessible function.

---
 cheri/cheri_prelude_common.sail | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index e6273281..47c8759c 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -261,6 +261,9 @@ function pcc_access_system_regs () =
       let pcc = capRegToCapStruct(PCC) in
       (pcc.access_system_regs)
 
+/*!
+The following function should be called before reading or writing any capability register to check whether it is one of the protected system capabilities. Although it is usually a general purpose capabilty the invoked data capabiltiy (IDC) is restricted in the branch delay slot of the CCall (selector one) instruction to protect the confidentiality and integrity of the invoked sandbox.
+ */
 val register_inaccessible : regno -> bool effect {rreg}
 function register_inaccessible(r) =
   ((r == IDC) & inCCallDelay) |
-- 
cgit v1.2.3