Merge

2 files changed, 10 insertions, 4 deletions

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index f65b7ca7..aed741d8 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -786,6 +786,7 @@ WhileCmd<out WhileCmd/*!*/ wcmd>
      Expr guard;  Expr/*!*/ e;  bool isFree;

      List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();

      StmtList/*!*/ body;

+     QKeyValue kv = null;

   .)

   "while"             (. x = t; .)

   Guard<out guard>    (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)

@@ -793,10 +794,11 @@ WhileCmd<out WhileCmd/*!*/ wcmd>
     [ "free"          (. isFree = true;  .)

     ]

     "invariant"

+    { Attribute<ref kv> }

     Expression<out e> (. if (isFree) {

-                           invariants.Add(new AssumeCmd(z, e));

+                           invariants.Add(new AssumeCmd(z, e, kv));

                          } else {

-                           invariants.Add(new AssertCmd(z, e));

+                           invariants.Add(new AssertCmd(z, e, kv));

                          }

                       .)

     ";"

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 8a63294c..5a6f8098 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1093,6 +1093,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		Expr guard;  Expr/*!*/ e;  bool isFree;

 		List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();

 		StmtList/*!*/ body;

+		QKeyValue kv = null;

 		

 		Expect(40);

 		x = t; 

@@ -1105,11 +1106,14 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				isFree = true;  

 			}

 			Expect(41);

+			while (la.kind == 25) {

+				Attribute(ref kv);

+			}

 			Expression(out e);

 			if (isFree) {

-			 invariants.Add(new AssumeCmd(z, e));

+			 invariants.Add(new AssumeCmd(z, e, kv));

 			} else {

-			 invariants.Add(new AssertCmd(z, e));

+			 invariants.Add(new AssertCmd(z, e, kv));

 			}

 			

 			Expect(7);