diff options
| author | Robert Norton | 2017-05-11 14:54:32 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-05-24 10:56:59 +0100 |
| commit | e9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 (patch) | |
| tree | f81ad5395520cc66a38d08d8ca1965f4e2bc30a3 /src/pretty_print_t_ascii.ml | |
| parent | a6c4b61f4ae06845663eb06b2a0efc98a42ccac3 (diff) | |
Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
Diffstat (limited to 'src/pretty_print_t_ascii.ml')
| -rw-r--r-- | src/pretty_print_t_ascii.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml index 79897f4b..1313fb37 100644 --- a/src/pretty_print_t_ascii.ml +++ b/src/pretty_print_t_ascii.ml @@ -96,8 +96,10 @@ and pp_format_base_effect_ascii (BE_aux(e,l)) = | BE_rreg -> "rreg" | BE_wreg -> "wreg" | BE_rmem -> "rmem" + | BE_rmemt -> "rmemt" | BE_wmem -> "wmem" | BE_wmv -> "wmv" + | BE_wmvt -> "wmvt" | BE_eamem -> "eamem" | BE_barr -> "barr" | BE_depend -> "depend" |