summaryrefslogtreecommitdiff
path: root/language/l2_parse.ml
diff options
context:
space:
mode:
authorKathy Gray2016-07-23 11:59:30 +0100
committerKathy Gray2016-07-23 11:59:30 +0100
commite60e43cb90cf7128cee4f82d84a402ba0cb14dc5 (patch)
tree0ae6b0cd026300d3c1d2be0458a22cb153b2bebc /language/l2_parse.ml
parent4a1e5a3df739abd747e47fb26f8a21228bd30c75 (diff)
Add a return exp form to Sail, supported in type checker and in interpreter.
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
Diffstat (limited to 'language/l2_parse.ml')
-rw-r--r--language/l2_parse.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index b94d16fe..cf1da35a 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -233,6 +233,7 @@ exp_aux = (* Expression *)
| E_assign of exp * exp (* imperative assignment *)
| E_sizeof of atyp
| E_exit of exp
+ | E_return of exp
| E_assert of exp * exp
and exp =