diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index d097c902..ff3d3d80 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -75,8 +75,8 @@ type base_effect_aux = (* effect *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) | 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_escape (* Internal tracking of expressions and functions that might call exit *) type base_effect = @@ -281,6 +281,7 @@ and exp_aux 'a = (* Expression *) | E_let of (letbind 'a) * (exp 'a) (* let expression *) | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is true, reporting the optional string as an error *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) |