From ac945514d59d91e51a63149b39b472421e59e299 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 29 Dec 2018 14:00:40 +0000
Subject: Add separate termination_measure declarations

---
 src/parser.mly | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index 66902953..3ad0931a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -183,7 +183,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 Constant 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
-- 
cgit v1.2.3