diff options
| author | Kathy Gray | 2016-03-08 17:08:53 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-03-08 17:09:06 +0000 |
| commit | dffe66f2e7dd7ce0f18b7c4f25a93743c4bc1ee0 (patch) | |
| tree | bfac5f9dd4bdfecfd96071ac758fcbfabd1b61c8 /src/lem_interp/interp_interface.lem | |
| parent | 8959d3454a6d67a69b54b14eedf106a26f2477d1 (diff) | |
Start task of setting up tagged memory in sequential interpreter
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index e5489bd5..6fe999c9 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -394,6 +394,7 @@ end type read_kind = (* common reads *) Read_plain + | Read_tag (*For reading the tag of tagged memory*) (* Power reads *) | Read_reserve (* AArch64 reads *) @@ -401,7 +402,8 @@ type read_kind = type write_kind = (* common writes *) - Write_plain + Write_plain + | Write_tag (*For writing the tag of tagged memory*) (* Power writes *) | Write_conditional (* AArch64 writes *) |