diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 7 |
1 files changed, 6 insertions, 1 deletions
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 |