summaryrefslogtreecommitdiff
path: root/src/parse_ast.ml
diff options
context:
space:
mode:
authorShaked Flur2017-05-24 16:45:22 +0100
committerShaked Flur2017-05-24 16:45:22 +0100
commitb400be4ea3917ace2237149e11dd5e1ab4e35078 (patch)
tree2baa7860e625b180c26f61acbc44db347fccfb6b /src/parse_ast.ml
parent9cffd54c6170f8a5cdcc6e54cb9077b62bf6a284 (diff)
parente9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 (diff)
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
Diffstat (limited to 'src/parse_ast.ml')
-rw-r--r--src/parse_ast.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 68ebbf9b..e069462a 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -77,8 +77,10 @@ base_effect_aux = (* effect *)
BE_rreg (* read register *)
| BE_wreg (* write register *)
| BE_rmem (* read memory *)
+ | BE_rmemt (* read memory tagged *)
| BE_wmem (* write memory *)
| BE_wmv (* write memory value *)
+ | BE_wmvt (* write memory value + tag *)
| BE_eamem (* address for write signaled *)
| BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
| BE_barr (* memory barrier *)