From bae82d3a7b383161f1c42312555cc9548ce23733 Mon Sep 17 00:00:00 2001
From: Bernhard Kragl <bernhard.kragl@gmail.com>
Date: Mon, 7 Sep 2020 19:17:35 +0200
Subject: [PATCH] Fix contract and usages of LabelOrCmd in parser (#283)

---
 Source/Core/BoogiePL.atg | 16 +++++++---------
 Source/Core/Parser.cs    | 10 ++++------
 2 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index c253d1874..18838be3a 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -705,15 +705,14 @@ StmtList<out StmtList/*!*/ stmtList>
 
   {
   ( LabelOrCmd<out c, out label>
-    (. if (c != null) {
+    (. Contract.Assert(c == null || label == null);
+       if (c != null) {
          // LabelOrCmd read a Cmd
-         Contract.Assert(label == null);
          if (startToken == null) { startToken = c.tok;  cs = new List<Cmd>(); }
          Contract.Assert(cs != null);
          cs.Add(c);
-       } else {
+       } else if (label != null) {
          // LabelOrCmd read a label
-         Contract.Assert(label != null);
          if (startToken != null) {
            Contract.Assert(cs != null);
            // dump the built-up state into a BigBlock
@@ -854,7 +853,7 @@ BreakCmd<out BreakCmd/*!*/ bcmd>
 /*------------------------------------------------------------------------*/
 
 LabelOrCmd<out Cmd c, out IToken label>
-/* ensures (c == null) != (label != null) */
+/* ensures (c == null) || (label == null) */
 = (. IToken/*!*/ x; Expr/*!*/ e;
      List<IToken>/*!*/ xs;
      List<IdentifierExpr> ids;
@@ -1362,11 +1361,10 @@ SpecBlock<out Block/*!*/ b>
   .)
   Ident<out x> ":"
   { LabelOrCmd<out c, out label>
-                       (. if (c != null) {
-                            Contract.Assert(label == null);
+                       (. Contract.Assert(c == null || label == null);
+                          if (c != null) {
                             cs.Add(c);
-                          } else {
-                            Contract.Assert(label != null);
+                          } else if (label != null) {
                             SemErr("SpecBlock's can only have one label");
                           }
                        .)
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 2866f9f65..26c3adbed 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -952,15 +952,14 @@ void StmtList(out StmtList/*!*/ stmtList) {
 		while (StartOf(7)) {
 			if (StartOf(8)) {
 				LabelOrCmd(out c, out label);
+				Contract.Assert(c == null || label == null);
 				if (c != null) {
 				 // LabelOrCmd read a Cmd
-				 Contract.Assert(label == null);
 				 if (startToken == null) { startToken = c.tok;  cs = new List<Cmd>(); }
 				 Contract.Assert(cs != null);
 				 cs.Add(c);
-				} else {
+				} else if (label != null) {
 				 // LabelOrCmd read a label
-				 Contract.Assert(label != null);
 				 if (startToken != null) {
 				   Contract.Assert(cs != null);
 				   // dump the built-up state into a BigBlock
@@ -2082,11 +2081,10 @@ void SpecBlock(out Block/*!*/ b) {
 		Expect(12);
 		while (StartOf(8)) {
 			LabelOrCmd(out c, out label);
+			Contract.Assert(c == null || label == null);
 			if (c != null) {
-			 Contract.Assert(label == null);
 			 cs.Add(c);
-			} else {
-			 Contract.Assert(label != null);
+			} else if (label != null) {
 			 SemErr("SpecBlock's can only have one label");
 			}