From 55eafc3dc845902d64ba6af3c03830ba67d18d30 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Wed, 7 Oct 2015 15:01:12 +0100
Subject: Start expanding annot for more refined effect tracking

---
 language/l2.lem | 1 +
 language/l2.ml  | 1 +
 language/l2.ott | 1 +
 3 files changed, 3 insertions(+)

(limited to 'language')

diff --git a/language/l2.lem b/language/l2.lem
index 54b31eb5..4d26f9b7 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -74,6 +74,7 @@ type base_effect_aux =  (* effect *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
+ | BE_lset (* Local mutation happend; not user-writable *)
 
 
 type base_effect = 
diff --git a/language/l2.ml b/language/l2.ml
index d5ea7c33..faae6e3f 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -71,6 +71,7 @@ base_effect_aux =  (* effect *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
+ | BE_lset (* Local mutation happend; not user-writable *)
 
 
 type 
diff --git a/language/l2.ott b/language/l2.ott
index eea0fba1..1dcc27da 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -193,6 +193,7 @@ base_effect :: 'BE_' ::=
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
+  | lset                                :: :: lset {{ com Local mutation happend; not user-writable }}
 
 
 effect :: 'Effect_' ::=
-- 
cgit v1.2.3