diff options
Diffstat (limited to 'src/lem_interp/printing_functions.ml')
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 4922a59a..9594f238 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -425,6 +425,10 @@ let rec format_events = function " Read_mem at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^ format_tracking tracking ^ " for " ^ (string_of_int length) ^ " bytes \n" ^ (format_events events) + | (E_read_memt(read_kind, (Address_lifted(location, _)), length, tracking))::events -> + " Read_memt at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^ + format_tracking tracking ^ " for " ^ (string_of_int length) ^ " bytes \n" ^ + (format_events events) | (E_write_mem(write_kind,(Address_lifted (location,_)), length, tracking, value, v_tracking))::events -> " Write_mem at " ^ (memory_value_to_string E_big_endian location) ^ ", based on registers " ^ format_tracking tracking ^ ", writing " ^ (memory_value_to_string E_big_endian value) ^ @@ -438,6 +442,10 @@ let rec format_events = function " Write_memv of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^ format_tracking v_tracking ^ "\n" ^ (format_events events) + | (E_write_memvt(_, (tag, value), v_tracking))::events -> + " Write_memvt of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^ + format_tracking v_tracking ^ "\n" ^ + (format_events events) | ((E_barrier b_kind)::events) -> " Memory_barrier occurred\n" ^ (format_events events) |