summaryrefslogtreecommitdiff
path: root/language/l2.lem
diff options
context:
space:
mode:
Diffstat (limited to 'language/l2.lem')
-rw-r--r--language/l2.lem1
1 files changed, 1 insertions, 0 deletions
diff --git a/language/l2.lem b/language/l2.lem
index dd300c89..94c93fe5 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -257,6 +257,7 @@ type exp_aux 'a = (* Expression *)
| E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
| E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
| E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
+ | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
| E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, 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 *)