Fix contract and usages of LabelOrCmd in parser (#283)

boogie-org · Sep 7, 2020 · bae82d3 · bae82d3
1 parent b083fb1
commit bae82d3
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 15 deletions.
diff --git 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
@@ -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");
 			}