XXX remove pattern match not handled correctly by ocaml embedding.

1 files changed, 6 insertions, 2 deletions

diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index dd2ec99c..4027d43f 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -227,14 +227,18 @@ val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect
 function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
 {
   (* assumes addr is cap. aligned *)
-  let ((bit[8]) tag : mem) = reverse_endianness(MEMr_tag (addr, cap_size)) in
+  let tagmem = reverse_endianness(MEMr_tag (addr, cap_size)) in
+  let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in
+  let mem = tagmem[((8 * cap_size) - 1) .. 0] in
   (tag[0], mem)
 }
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
 {
   (* assumes addr is cap. aligned *)
-  let ((bit[8]) tag : mem) = reverse_endianness(MEMr_tag_reserve (addr, cap_size)) in
+  let tagmem = reverse_endianness(MEMr_tag_reserve (addr, cap_size)) in
+  let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in
+  let mem = tagmem[((8 * cap_size) - 1) .. 0] in
   (tag[0], mem)
 }