From 5cd145951c080b05dc9a515fe40bd687c92f0d5c Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Wed, 14 Sep 2016 12:30:25 +0100
Subject: Change reading and writing of tag memory to report the tag/look for
 the tag as the first byte of the byte list on tagged memory operations

---
 src/lem_interp/run_interp_model.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 7b4a13de..aca33e96 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -129,7 +129,12 @@ let rec perform_action ((reg, mem, tagmem) as env) = function
    let naddress = integer_of_address address in
    (match kind with
     | Read_tag ->
-      (Some (register_value_of_memory_value [(Mem.find naddress tagmem)] !default_order), env)
+      let tag = Mem.find naddress tagmem in
+      let rec reading (n : num) length = 
+        if length = 0 
+        then []
+        else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in
+      (Some (register_value_of_memory_value (tag::(reading naddress length)) !default_order), env)
     | _ ->
       let rec reading (n : num) length = 
         if length = 0 
-- 
cgit v1.2.3