Boogie: white-space formating

3 files changed, 169 insertions, 151 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 67500c88..7f5642f3 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1751,7 +1751,7 @@ namespace Microsoft.Boogie {
   public class Function : DeclWithFormals {

     public string Comment;

 

-    // the body is only set if the function is declared with {:expand true}

+    // the body is only set if the function is declared with {:inline}

     public Expr Body;

     public List<Expansion/*!*/> expansions;

     public bool doingExpansion;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index ec27422e..6b8bb178 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -148,19 +148,26 @@ BoogiePL
      Implementation/*!*/ nnim;

   .)

   { Consts<out vs>             (. foreach(Bpl.Variable/*!*/ v in vs){

-Contract.Assert(v != null);

- Pgm.TopLevelDeclarations.Add(v); } .)

+                                    Contract.Assert(v != null);

+                                    Pgm.TopLevelDeclarations.Add(v);

+                                  }

+                               .)

   | Function<out ds>           (. foreach(Bpl.Declaration/*!*/ d in ds){

-Contract.Assert(d != null);

- Pgm.TopLevelDeclarations.Add(d); } .)

+                                    Contract.Assert(d != null);

+                                    Pgm.TopLevelDeclarations.Add(d);

+                                  }

+                               .)

   | Axiom<out ax>              (. Pgm.TopLevelDeclarations.Add(ax); .)

   | UserDefinedTypes<out ts>   (. foreach(Declaration/*!*/ td in ts){

-Contract.Assert(td != null);

-                                        Pgm.TopLevelDeclarations.Add(td);

-                                      } .)

+                                    Contract.Assert(td != null);

+                                    Pgm.TopLevelDeclarations.Add(td);

+                                  }

+                               .)

   | GlobalVars<out vs>         (. foreach(Bpl.Variable/*!*/ v in vs){

-Contract.Assert(v != null);

- Pgm.TopLevelDeclarations.Add(v); } .)

+                                    Contract.Assert(v != null);

+                                    Pgm.TopLevelDeclarations.Add(v);

+                                  }

+                               .)

   | Procedure<out pr, out im>  (. Pgm.TopLevelDeclarations.Add(pr);

                                    if (im != null) {

                                      Pgm.TopLevelDeclarations.Add(im);

@@ -178,7 +185,7 @@ GlobalVars<out VariableSeq/*!*/ ds>
   { Attribute<ref kv> }

   IdsTypeWheres<true, tyds> ";"

   (. foreach(TypedIdent/*!*/ tyd in tyds){

-Contract.Assert(tyd != null);

+       Contract.Assert(tyd != null);

        ds.Add(new GlobalVariable(tyd.tok, tyd, kv));

      }

   .)

@@ -190,7 +197,7 @@ LocalVars<VariableSeq/*!*/ ds>
   { Attribute<ref kv> }

   IdsTypeWheres<true, tyds> ";"

   (. foreach(TypedIdent/*!*/ tyd in tyds){

-Contract.Assert(tyd != null);

+       Contract.Assert(tyd != null);

        ds.Add(new LocalVariable(tyd.tok, tyd, kv));

      }

   .)

@@ -202,7 +209,7 @@ ProcFormals<bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds>
   [ IdsTypeWheres<allowWhereClauses, tyds> ]

   ")"

   (. foreach(TypedIdent/*!*/ tyd in tyds){

-Contract.Assert(tyd != null);

+       Contract.Assert(tyd != null);

        ds.Add(new Formal(tyd.tok, tyd, incoming));

      }

   .)

@@ -212,7 +219,7 @@ BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>
 = (. Contract.Requires(x != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); .)

   IdsTypeWheres<false, tyds>

   (. foreach(TypedIdent/*!*/ tyd in tyds){

-Contract.Assert(tyd != null);

+       Contract.Assert(tyd != null);

        ds.Add(new BoundVariable(tyd.tok, tyd));

      }

   .)

@@ -225,7 +232,7 @@ IdsType<out TypedIdentSeq/*!*/ tyds>
   Idents<out ids> ":" Type<out ty>

   (. tyds = new TypedIdentSeq();

      foreach(Token/*!*/ id in ids){

-Contract.Assert(id != null);

+       Contract.Assert(id != null);

        tyds.Add(new TypedIdent(id, id.val, ty, null));

      }

   .)

@@ -250,7 +257,7 @@ IdsTypeWhere<bool allowWhereClauses, TypedIdentSeq/*!*/ tyds>
                                  .)

   ]

   (. foreach(Token/*!*/ id in ids){

-Contract.Assert(id != null);

+       Contract.Assert(id != null);

        tyds.Add(new TypedIdent(id, id.val, ty, wh));

      }

   .)

@@ -320,7 +327,7 @@ TypeParams<out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams>
   (.

     typeParams = new TypeVariableSeq ();

     foreach(Token/*!*/ id in typeParamToks){

-Contract.Assert(id != null);

+      Contract.Assert(id != null);

       typeParams.Add(new TypeVariable(id, id.val));}

    .)

   .

@@ -348,13 +355,14 @@ Consts<out VariableSeq/*!*/ ds>
   [ OrderSpec<out ChildrenComplete, out Parents> ]

   (. bool makeClone = false;

      foreach(TypedIdent/*!*/ x in xs){

-Contract.Assert(x != null);

+       Contract.Assert(x != null);

 

        // ensure that no sharing is introduced

        List<ConstantParent/*!*/> ParentsClone;

        if (makeClone && Parents != null) {

          ParentsClone = new List<ConstantParent/*!*/> ();

-         foreach (ConstantParent/*!*/ p in Parents){Contract.Assert(p != null);

+         foreach (ConstantParent/*!*/ p in Parents){

+           Contract.Assert(p != null);

            ParentsClone.Add(new ConstantParent (

                             new IdentifierExpr (p.Parent.tok, p.Parent.Name),

                             p.Unique));}

@@ -432,7 +440,7 @@ ds = new DeclarationSeq(); IToken/*!*/ z;
     ds.Add(func);

     bool allUnnamed = true;

     foreach(Formal/*!*/ f in arguments){

-Contract.Assert(f != null);

+      Contract.Assert(f != null);

       if (f.TypedIdent.Name != "") {

         allUnnamed = false;

 	break;

@@ -469,7 +477,7 @@ Contract.Assert(f != null);
         ExprSeq callArgs = new ExprSeq();

         int i = 0;

         foreach(Formal/*!*/ f in arguments){

-Contract.Assert(f != null);

+          Contract.Assert(f != null);

           string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

           dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

           callArgs.Add(new IdentifierExpr(f.tok, nm));

@@ -477,20 +485,21 @@ Contract.Assert(f != null);
         }

         TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

         foreach(TypeVariable/*!*/ t in typeParams){

-Contract.Assert(t != null);

-          quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));}

+          Contract.Assert(t != null);

+          quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

+        }

 

         Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

         // specify the type of the function, because it might be that

         // type parameters only occur in the output type

         call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

-		    Expr def = Expr.Eq(call, definition);

-		    if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-		      def = new ForallExpr(z, quantifiedTypeVars, dummies, 

-		                           kv, 

-		                           new Trigger(z, true, new ExprSeq(call), null),

-		                           def);

-		    }

+        Expr def = Expr.Eq(call, definition);

+        if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

+          def = new ForallExpr(z, quantifiedTypeVars, dummies,

+                               kv,

+                               new Trigger(z, true, new ExprSeq(call), null),

+                               def);

+        }

         ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

       }

     }

@@ -544,7 +553,7 @@ UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>
      if (synonym) {

        TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();

        foreach(Token/*!*/ t in paramTokens){

-Contract.Assert(t != null);

+         Contract.Assert(t != null);

          typeParams.Add(new TypeVariable(t, t.val));}

        decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);

      } else {

@@ -618,7 +627,7 @@ Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
 = (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)

   ( "modifies"

     [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){

-Contract.Assert(m != null);

+                                 Contract.Assert(m != null);

                                  mods.Add(new IdentifierExpr(m, m.val));

                                }

                             .)

@@ -726,8 +735,8 @@ TransferCmd<out TransferCmd/*!*/ tc>
   .)

   ( "goto"             (. y = t; .)

     Idents<out xs>     (. foreach(IToken/*!*/ s in xs){

-Contract.Assert(s != null);

- ss.Add(s.val); }

+                            Contract.Assert(s != null);

+                            ss.Add(s.val); }

                           tc = new GotoCmd(y, ss);

                        .)

   | "return"           (. tc = new ReturnCmd(t); .)

@@ -828,7 +837,7 @@ LabelOrCmd<out Cmd c, out IToken label>
   | "havoc"               (. x = t; .)

     Idents<out xs> ";"    (. ids = new IdentifierExprSeq();

                              foreach(IToken/*!*/ y in xs){

-Contract.Assert(y != null);

+                               Contract.Assert(y != null);

                                ids.Add(new IdentifierExpr(y, y.val));

                              }

                              c = new HavocCmd(x,ids);

@@ -1323,8 +1332,8 @@ SpecBlock<out Block/*!*/ b>
   }

   ( "goto"             (. y = t; .)

     Idents<out xs>     (. foreach(IToken/*!*/ s in xs){

-Contract.Assert(s != null);

- ss.Add(s.val); }

+                            Contract.Assert(s != null);

+                            ss.Add(s.val); }

                           b = new Block(x,x.val,cs,new GotoCmd(y,ss));

                        .)

   | "return" Expression<out e>

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 5e5dd178..cab72087 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -205,15 +205,19 @@ private class BvBounds : Expr {
 			case 19: {

 				Consts(out vs);

 				foreach(Bpl.Variable/*!*/ v in vs){

-				Contract.Assert(v != null);

-				 Pgm.TopLevelDeclarations.Add(v); } 

+				 Contract.Assert(v != null);

+				 Pgm.TopLevelDeclarations.Add(v);

+				}

+				

 				break;

 			}

 			case 23: {

 				Function(out ds);

 				foreach(Bpl.Declaration/*!*/ d in ds){

-				Contract.Assert(d != null);

-				 Pgm.TopLevelDeclarations.Add(d); } 

+				 Contract.Assert(d != null);

+				 Pgm.TopLevelDeclarations.Add(d);

+				}

+				

 				break;

 			}

 			case 27: {

@@ -224,16 +228,19 @@ private class BvBounds : Expr {
 			case 28: {

 				UserDefinedTypes(out ts);

 				foreach(Declaration/*!*/ td in ts){

-				Contract.Assert(td != null);

-				                                        Pgm.TopLevelDeclarations.Add(td);

-				                                      } 

+				 Contract.Assert(td != null);

+				 Pgm.TopLevelDeclarations.Add(td);

+				}

+				

 				break;

 			}

 			case 6: {

 				GlobalVars(out vs);

 				foreach(Bpl.Variable/*!*/ v in vs){

-				Contract.Assert(v != null);

-				 Pgm.TopLevelDeclarations.Add(v); } 

+				 Contract.Assert(v != null);

+				 Pgm.TopLevelDeclarations.Add(v);

+				}

+				

 				break;

 			}

 			case 30: {

@@ -276,13 +283,14 @@ private class BvBounds : Expr {
 		}

 		bool makeClone = false;

 		foreach(TypedIdent/*!*/ x in xs){

-		Contract.Assert(x != null);

+		  Contract.Assert(x != null);

 		

 		       // ensure that no sharing is introduced

 		       List<ConstantParent/*!*/> ParentsClone;

 		       if (makeClone && Parents != null) {

 		         ParentsClone = new List<ConstantParent/*!*/> ();

-		         foreach (ConstantParent/*!*/ p in Parents){Contract.Assert(p != null);

+		         foreach (ConstantParent/*!*/ p in Parents){

+		           Contract.Assert(p != null);

 		           ParentsClone.Add(new ConstantParent (

 		                            new IdentifierExpr (p.Parent.tok, p.Parent.Name),

 		                            p.Unique));}

@@ -360,65 +368,66 @@ private class BvBounds : Expr {
 		ds.Add(func);

 		bool allUnnamed = true;

 		foreach(Formal/*!*/ f in arguments){

-		Contract.Assert(f != null);

-		      if (f.TypedIdent.Name != "") {

-		        allUnnamed = false;

-			break;

-		      }

-		    }

-		    if (!allUnnamed) {

-		      Type prevType = null;

-		      for (int i = arguments.Length - 1; i >= 0; i--) {

-		        TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;

-		        if (curr.Name == "") {

-			  if (prevType == null) {

-			    this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");

-			    break;

-			  }

-			  Type ty = curr.Type;

-		          if (ty is UnresolvedTypeIdentifier &&

-		              cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {

-			    curr.Name = cce.NonNull(ty as UnresolvedTypeIdentifier).Name;

-			    curr.Type = prevType;

-			  } else {

-			    this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");

-			  }

-			} else {

-			  prevType = curr.Type;

-			}

-		      }

-		    }

-		    if (definition != null) {

-		      // generate either an axiom or a function body

-		      if (QKeyValue.FindBoolAttribute(kv, "inline")) {

-		        func.Body = definition;

-		      } else {

-		        VariableSeq dummies = new VariableSeq();

-		        ExprSeq callArgs = new ExprSeq();

-		        int i = 0;

-		        foreach(Formal/*!*/ f in arguments){

-		Contract.Assert(f != null);

-		          string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

-		          dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

-		          callArgs.Add(new IdentifierExpr(f.tok, nm));

-		          i++;

-		        }

-		        TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

-		        foreach(TypeVariable/*!*/ t in typeParams){

-		Contract.Assert(t != null);

-		          quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));}

+		  Contract.Assert(f != null);

+		  if (f.TypedIdent.Name != "") {

+		    allUnnamed = false;

+		break;

+		     }

+		   }

+		   if (!allUnnamed) {

+		     Type prevType = null;

+		     for (int i = arguments.Length - 1; i >= 0; i--) {

+		       TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;

+		       if (curr.Name == "") {

+		  if (prevType == null) {

+		    this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");

+		    break;

+		  }

+		  Type ty = curr.Type;

+		         if (ty is UnresolvedTypeIdentifier &&

+		             cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {

+		    curr.Name = cce.NonNull(ty as UnresolvedTypeIdentifier).Name;

+		    curr.Type = prevType;

+		  } else {

+		    this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");

+		  }

+		} else {

+		  prevType = curr.Type;

+		}

+		     }

+		   }

+		   if (definition != null) {

+		     // generate either an axiom or a function body

+		     if (QKeyValue.FindBoolAttribute(kv, "inline")) {

+		       func.Body = definition;

+		     } else {

+		       VariableSeq dummies = new VariableSeq();

+		       ExprSeq callArgs = new ExprSeq();

+		       int i = 0;

+		       foreach(Formal/*!*/ f in arguments){

+		         Contract.Assert(f != null);

+		         string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

+		         dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

+		         callArgs.Add(new IdentifierExpr(f.tok, nm));

+		         i++;

+		       }

+		       TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

+		       foreach(TypeVariable/*!*/ t in typeParams){

+		         Contract.Assert(t != null);

+		         quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

+		       }

 		

 		        Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

 		        // specify the type of the function, because it might be that

 		        // type parameters only occur in the output type

 		        call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

-				    Expr def = Expr.Eq(call, definition);

-				    if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-				      def = new ForallExpr(z, quantifiedTypeVars, dummies, 

-				                           kv, 

-				                           new Trigger(z, true, new ExprSeq(call), null),

-				                           def);

-				    }

+		        Expr def = Expr.Eq(call, definition);

+		        if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

+		          def = new ForallExpr(z, quantifiedTypeVars, dummies,

+		                               kv,

+		                               new Trigger(z, true, new ExprSeq(call), null),

+		                               def);

+		        }

 		        ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

 		      }

 		    }

@@ -462,10 +471,10 @@ private class BvBounds : Expr {
 		IdsTypeWheres(true, tyds);

 		Expect(7);

 		foreach(TypedIdent/*!*/ tyd in tyds){

-		Contract.Assert(tyd != null);

-		       ds.Add(new GlobalVariable(tyd.tok, tyd, kv));

-		     }

-		  

+		 Contract.Assert(tyd != null);

+		 ds.Add(new GlobalVariable(tyd.tok, tyd, kv));

+		}

+		

 	}

 

 	void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {

@@ -538,10 +547,10 @@ private class BvBounds : Expr {
 		IdsTypeWheres(true, tyds);

 		Expect(7);

 		foreach(TypedIdent/*!*/ tyd in tyds){

-		Contract.Assert(tyd != null);

-		       ds.Add(new LocalVariable(tyd.tok, tyd, kv));

-		     }

-		  

+		 Contract.Assert(tyd != null);

+		 ds.Add(new LocalVariable(tyd.tok, tyd, kv));

+		}

+		

 	}

 

 	void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds) {

@@ -552,20 +561,20 @@ private class BvBounds : Expr {
 		}

 		Expect(9);

 		foreach(TypedIdent/*!*/ tyd in tyds){

-		Contract.Assert(tyd != null);

-		       ds.Add(new Formal(tyd.tok, tyd, incoming));

-		     }

-		  

+		 Contract.Assert(tyd != null);

+		 ds.Add(new Formal(tyd.tok, tyd, incoming));

+		}

+		

 	}

 

 	void BoundVars(IToken/*!*/ x, out VariableSeq/*!*/ ds) {

 		Contract.Requires(x != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); 

 		IdsTypeWheres(false, tyds);

 		foreach(TypedIdent/*!*/ tyd in tyds){

-		Contract.Assert(tyd != null);

-		       ds.Add(new BoundVariable(tyd.tok, tyd));

-		     }

-		  

+		 Contract.Assert(tyd != null);

+		 ds.Add(new BoundVariable(tyd.tok, tyd));

+		}

+		

 	}

 

 	void IdsType(out TypedIdentSeq/*!*/ tyds) {

@@ -575,10 +584,10 @@ private class BvBounds : Expr {
 		Type(out ty);

 		tyds = new TypedIdentSeq();

 		foreach(Token/*!*/ id in ids){

-		Contract.Assert(id != null);

-		       tyds.Add(new TypedIdent(id, id.val, ty, null));

-		     }

-		  

+		  Contract.Assert(id != null);

+		  tyds.Add(new TypedIdent(id, id.val, ty, null));

+		}

+		

 	}

 

 	void Idents(out TokenSeq/*!*/ xs) {

@@ -624,10 +633,10 @@ private class BvBounds : Expr {
 			

 		}

 		foreach(Token/*!*/ id in ids){

-		Contract.Assert(id != null);

-		       tyds.Add(new TypedIdent(id, id.val, ty, wh));

-		     }

-		  

+		 Contract.Assert(id != null);

+		 tyds.Add(new TypedIdent(id, id.val, ty, wh));

+		}

+		

 	}

 

 	void Expression(out Expr/*!*/ e0) {

@@ -716,9 +725,9 @@ private class BvBounds : Expr {
 		Expect(18);

 		typeParams = new TypeVariableSeq ();

 		foreach(Token/*!*/ id in typeParamToks){

-		Contract.Assert(id != null);

-		      typeParams.Add(new TypeVariable(id, id.val));}

-		   

+		  Contract.Assert(id != null);

+		  typeParams.Add(new TypeVariable(id, id.val));}

+		

 	}

 

 	void Types(TypeSeq/*!*/ ts) {

@@ -804,13 +813,13 @@ private class BvBounds : Expr {
 		if (synonym) {

 		 TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();

 		 foreach(Token/*!*/ t in paramTokens){

-		Contract.Assert(t != null);

-		         typeParams.Add(new TypeVariable(t, t.val));}

-		       decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);

-		     } else {

-		       decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);

-		     }

-		   

+		   Contract.Assert(t != null);

+		   typeParams.Add(new TypeVariable(t, t.val));}

+		 decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);

+		} else {

+		  decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);

+		}

+		

 	}

 

 	void WhiteSpaceIdents(out TokenSeq/*!*/ xs) {

@@ -849,10 +858,10 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			if (la.kind == 1) {

 				Idents(out ms);

 				foreach(IToken/*!*/ m in ms){

-				Contract.Assert(m != null);

-				                                 mods.Add(new IdentifierExpr(m, m.val));

-				                               }

-				                            

+				 Contract.Assert(m != null);

+				 mods.Add(new IdentifierExpr(m, m.val));

+				}

+				

 			}

 			Expect(7);

 		} else if (la.kind == 33) {

@@ -999,11 +1008,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			Expect(7);

 			ids = new IdentifierExprSeq();

 			foreach(IToken/*!*/ y in xs){

-			Contract.Assert(y != null);

-			                               ids.Add(new IdentifierExpr(y, y.val));

-			                             }

-			                             c = new HavocCmd(x,ids);

-			                          

+			  Contract.Assert(y != null);

+			  ids.Add(new IdentifierExpr(y, y.val));

+			}

+			c = new HavocCmd(x,ids);

+			

 		} else if (la.kind == 48) {

 			CallCmd(out cn);

 			Expect(7);

@@ -1037,10 +1046,10 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			y = t; 

 			Idents(out xs);

 			foreach(IToken/*!*/ s in xs){

-			Contract.Assert(s != null);

+			 Contract.Assert(s != null);

 			 ss.Add(s.val); }

-			                          tc = new GotoCmd(y, ss);

-			                       

+			tc = new GotoCmd(y, ss);

+			

 		} else if (la.kind == 37) {

 			Get();

 			tc = new ReturnCmd(t); 

@@ -1910,10 +1919,10 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			y = t; 

 			Idents(out xs);

 			foreach(IToken/*!*/ s in xs){

-			Contract.Assert(s != null);

+			 Contract.Assert(s != null);

 			 ss.Add(s.val); }

-			                          b = new Block(x,x.val,cs,new GotoCmd(y,ss));

-			                       

+			b = new Block(x,x.val,cs,new GotoCmd(y,ss));

+			

 		} else if (la.kind == 37) {

 			Get();

 			Expression(out e);