From cd33f38664c620f1eec5d97bde5b837770e7abbc Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 9 May 2018 16:36:54 +0100
Subject: Use latex support for generating cheri documentation and remove sed
 based hack. Also some minor code cleanups and comments.

---
 mips/mips_prelude.sail | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'mips/mips_prelude.sail')

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 9e81a5d0..f9049b5d 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -469,11 +469,18 @@ function int_of_AccessLevel level =
     Kernel      => 2
   }
 
+/*!
+Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level.
+ */
 val grantsAccess : (AccessLevel, AccessLevel) -> bool
 function grantsAccess (currentLevel, requiredLevel) =
   int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel)
 
-function getAccessLevel() : unit -> AccessLevel=
+/*!
+Returns the current effective access level determined by accessing the relevant parts of the MIPS status register.
+ */
+val getAccessLevel : unit -> AccessLevel effect {rreg}
+function getAccessLevel() =
   if ((CP0Status.EXL()) | (CP0Status.ERL())) then
     Kernel
   else match CP0Status.KSU()
-- 
cgit v1.2.3