diff options
Diffstat (limited to 'src/lem_interp/interp_ast.lem')
| -rw-r--r-- | src/lem_interp/interp_ast.lem | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem index 64fb14b2..c65963d7 100644 --- a/src/lem_interp/interp_ast.lem +++ b/src/lem_interp/interp_ast.lem @@ -119,9 +119,11 @@ type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) | BE_rmem (* read memory *) + | BE_rmemt (* read memory and tag *) | BE_wmem (* write memory *) | BE_eamem (* signal effective address for writing memory *) | BE_wmv (* write memory, sending only value *) + | BE_wmvt (* write memory, sending only value and tag *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) |