diff options
| author | Kathy Gray | 2016-07-23 13:16:09 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-07-23 13:16:09 +0100 |
| commit | cc61f795555c6e80f2d82f9b6655a5a3115d50f2 (patch) | |
| tree | 00ce98fd1af0bc40c2ec6f858a200eec278ad9c3 /language/l2.ml | |
| parent | 8702b977b43999f0b203f44074ac0abd3bac0e02 (diff) | |
Add effect annotation for return, and actually keep a return after type check.
Diffstat (limited to 'language/l2.ml')
| -rw-r--r-- | language/l2.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/language/l2.ml b/language/l2.ml index 39f430db..1a35432b 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -85,6 +85,7 @@ base_effect_aux = (* effect *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) | BE_escape (* Tracking of expressions and functions that might call exit *) | BE_lset (* Local mutation happend; not user-writable *) + | BE_lret (* Local return happened; not user-writable *) type |