diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 4 | ||||
| -rw-r--r-- | language/l2.ml | 4 | ||||
| -rw-r--r-- | language/l2.ott | 2 | ||||
| -rw-r--r-- | language/l2_parse.ml | 4 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2 |
5 files changed, 13 insertions, 3 deletions
diff --git a/language/l2.lem b/language/l2.lem index adbb38b6..36d64694 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2_typ.ott l2.ott *) +(* generated by Ott 0.24 from: l2_typ.ott l2.ott *) open import Pervasives open import Map @@ -67,6 +67,8 @@ type base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_eamem (* signal effective address for writing memory *) + | BE_wmv (* write memory, sending only value *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) diff --git a/language/l2.ml b/language/l2.ml index 6ce6a064..ea3252da 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2.ott *) +(* generated by Ott 0.24 from: l2.ott *) type text = string @@ -64,6 +64,8 @@ base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_eamem (* signal effective address for writing memory *) + | BE_wmv (* write memory, sending only value *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) diff --git a/language/l2.ott b/language/l2.ott index b1e1dfb1..721ee60f 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -186,6 +186,8 @@ base_effect :: 'BE_' ::= | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} + | wmea :: :: eamem {{ com signal effective address for writing memory }} + | wmv :: :: wmv {{ com write memory, sending only value }} | barr :: :: barr {{ com memory barrier }} | depend :: :: depend {{ com dynamic footprint }} | undef :: :: undef {{ com undefined-instruction exception }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index f2ee40c1..76fa09b8 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2_parse.ott *) +(* generated by Ott 0.24 from: l2_parse.ott *) type text = string @@ -46,6 +46,8 @@ base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_wmv (* write memory value *) + | BE_eamem (* address for write signaled *) | BE_barr (* memory barrier *) | BE_depend (* dynmically dependent footprint *) | BE_undef (* undefined-instruction exception *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 1945c926..83da93ad 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -155,6 +155,8 @@ base_effect :: 'BE_' ::= | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} + | wmv :: :: wmv {{ com write memory value }} + | eamem :: :: eamem {{ com address for write signaled }} | barr :: :: barr {{ com memory barrier }} | depend :: :: depend {{ com dynmically dependent footprint }} | undef :: :: undef {{ com undefined-instruction exception }} |