summaryrefslogtreecommitdiff
path: root/src/parser.mly
diff options
context:
space:
mode:
authorAlasdair2019-01-14 10:36:43 +0000
committerAlasdair2019-01-14 10:36:43 +0000
commit2eb2566c5c3ef5d7250fea604933704d8d94eabe (patch)
tree8bebb52a23c3982514b769beffac82e8ac06cd6c /src/parser.mly
parent9cfa575245a0427a0d35504086de182bd80b7df8 (diff)
parenta3da2efb3ef08e132e16db0c510b1b8fe4ee600c (diff)
Merge remote-tracking branch 'origin/sail2' into asl_flow2
Diffstat (limited to 'src/parser.mly')
-rw-r--r--src/parser.mly4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/parser.mly b/src/parser.mly
index 68720048..7540d1f4 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -182,7 +182,7 @@ let rec desugar_rchain chain s e =
%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
-%token Repeat Until While Do Mutual Var Ref Configuration
+%token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure
%nonassoc Then
%nonassoc Else
@@ -1430,6 +1430,8 @@ def:
{ DEF_internal_mutrec $3 }
| Pragma
{ DEF_pragma (fst $1, snd $1, loc $startpos $endpos) }
+ | TerminationMeasure id pat Eq exp
+ { DEF_measure ($2, $3, $5) }
defs_list:
| def