diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 1 | ||||
| -rw-r--r-- | language/l2.ml | 1 | ||||
| -rw-r--r-- | language/l2.ott | 3 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 |
5 files changed, 6 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index b19639bb..af6b1485 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -66,6 +66,7 @@ type base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_barr (* memory barrier *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) diff --git a/language/l2.ml b/language/l2.ml index 76b27874..e46014dc 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -63,6 +63,7 @@ base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_barr (* memory barrier *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) diff --git a/language/l2.ott b/language/l2.ott index 5d1994e2..c56a186b 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -117,7 +117,7 @@ id :: '' ::= | unit :: M :: unit {{ ichlo (Id "unit") }} | nat :: M :: nat {{ ichlo (Id "nat") }} | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }} - | enum :: M :: enum {{ ichlo (Id "enum") }} + | range :: M :: range {{ ichlo (Id "range") }} | vector :: M :: vector {{ ichlo (Id "vector") }} | list :: M :: list {{ ichlo (Id "list") }} | set :: M :: set {{ ichlo (Id "set") }} @@ -184,6 +184,7 @@ base_effect :: 'BE_' ::= | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} + | barr :: :: barr {{ com memory barrier }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 3146ad2b..b54491bc 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -46,6 +46,7 @@ base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_barr (* memory barrier *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 03c50d08..e62e4587 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -155,6 +155,7 @@ base_effect :: 'BE_' ::= | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} + | barr :: :: barr {{ com memory barrier }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} |