summaryrefslogtreecommitdiff
path: root/src/parser.mly
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-09-26 17:10:06 +0100
committerAlasdair Armstrong2017-09-26 17:10:06 +0100
commitced56765ec9324a0e690cbb4e790280d17413f99 (patch)
tree18584c77dc93b553b840008774fae4b46a622500 /src/parser.mly
parent15309c879d2c877953512c401e66a7a48af6df97 (diff)
Added while-do and repeat-until loops to sail for translating ASL
Diffstat (limited to 'src/parser.mly')
-rw-r--r--src/parser.mly3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/parser.mly b/src/parser.mly
index 5413ac0d..0c3dbb03 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,6 +133,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef
%token Undefined Union With When Val Constraint Try Catch Throw
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
+%token While Do Repeat Until
/* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -689,6 +690,8 @@ right_atomic_exp:
then ATyp_aux(ATyp_inc,(locn 6 6))
else ATyp_aux(ATyp_dec,(locn 6 6)) in
eloc (E_for($3,$5,$7,step,ord,$9)) }
+ | While exp Do exp
+ { eloc (E_loop (While, $2, $4)) }
| letbind In exp
{ eloc (E_let($1,$3)) }