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 | 1 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 |
5 files changed, 5 insertions, 0 deletions
diff --git a/language/l2.lem b/language/l2.lem index 5441587d..6291acba 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -68,6 +68,7 @@ type base_effect_aux = (* effect *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) | BE_barr (* memory barrier *) + | BE_depend (* dynamic footprint *) | 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 2b5f04ce..6ce6a064 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -65,6 +65,7 @@ base_effect_aux = (* effect *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) | BE_barr (* memory barrier *) + | BE_depend (* dynamic footprint *) | 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 59de79cd..b1e1dfb1 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -187,6 +187,7 @@ base_effect :: 'BE_' ::= | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} | barr :: :: barr {{ com memory barrier }} + | depend :: :: depend {{ com dynamic footprint }} | 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 f4cb278a..f2ee40c1 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -47,6 +47,7 @@ base_effect_aux = (* effect *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) | BE_barr (* memory barrier *) + | BE_depend (* dynmically dependent footprint *) | 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 7126b9e0..1945c926 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -156,6 +156,7 @@ base_effect :: 'BE_' ::= | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} | barr :: :: barr {{ com memory barrier }} + | depend :: :: depend {{ com dynmically dependent footprint }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} |