From 4683962ecbb42167d6d966d731c451ba5eb696d5 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Fri, 21 Jul 2017 19:21:45 +0100
Subject: l2.ott: port across additions to base_effect from rmem

---
 language/l2.ott | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/language/l2.ott b/language/l2.ott
index bf001f5c..803472a8 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -184,11 +184,14 @@ base_effect :: 'BE_' ::=
   | rreg                                :: :: rreg {{ com read register }}
   | wreg                                :: :: wreg {{ com write register }}
   | rmem                                :: :: rmem {{ com read memory }}
+  | rmemt                               :: :: rmemt {{ com read memory and tag }}
   | wmem                                :: :: wmem {{ com write memory }}
-  | wmea				:: :: eamem {{ com signal effective address for writing memory }}
-  | wmv					:: :: wmv   {{ com write memory, sending only value }} 
+  | wmea				                :: :: eamem {{ com signal effective address for writing memory }}
+  | exmem                               :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }}
+  | wmv					                :: :: wmv   {{ com write memory, sending only value }}
+  | wmvt                                :: :: wmvt  {{ com write memory, sending only value and tag }}
   | barr                                :: :: barr {{ com memory barrier }}
-  | depend				:: :: depend {{ com dynamic footprint }}
+  | depend				                :: :: depend {{ com dynamic footprint }}
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }}
-- 
cgit v1.2.3