Allow ":" in addition to "returns" in function definitions. Make the pretty-printer use ":" not "returns".

Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions.
Consequently foo(int,y:bool) is no longer allowed.
Update the testsuite to match that.

12 files changed, 248 insertions, 145 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index fd54412c..fc706e2c 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -1126,14 +1126,20 @@ namespace Microsoft.Boogie
       // base(that.tok, (!) that.Name);

     }

 

-    protected void EmitSignature (TokenTextWriter! stream)

+    protected void EmitSignature (TokenTextWriter! stream, bool shortRet)

     {

       Type.EmitOptionalTypeParams(stream, TypeParameters);

       stream.Write("(");

       InParams.Emit(stream);

       stream.Write(")");

 

-      if (OutParams.Length > 0)

+      if (shortRet) 

+      {

+        assert OutParams.Length == 1;

+        stream.Write(" : ");

+        ((!)OutParams[0]).TypedIdent.Type.Emit(stream);

+      } 

+      else if (OutParams.Length > 0)

       {

         stream.Write(" returns (");

         OutParams.Emit(stream);

@@ -1262,7 +1268,7 @@ namespace Microsoft.Boogie
       } else {

         stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));

       }

-      EmitSignature(stream);

+      EmitSignature(stream, true);

       if (Body != null) {

         stream.WriteLine();

         stream.WriteLine("{");

@@ -1539,7 +1545,7 @@ namespace Microsoft.Boogie
       stream.Write(this, level, "procedure ");

       EmitAttributes(stream);

       stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));

-      EmitSignature(stream);

+      EmitSignature(stream, false);

       stream.WriteLine(";");

 

       level++;

@@ -1751,7 +1757,7 @@ namespace Microsoft.Boogie
       stream.Write(this, level, "implementation ");

       EmitAttributes(stream);

       stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));

-      EmitSignature(stream);

+      EmitSignature(stream, false);

       stream.WriteLine();

 

       stream.WriteLine(level, "{0}", '{');

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 4fc91b35..eab10ff9 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -380,6 +380,8 @@ Function<out DeclarationSeq! ds>
      TypeVariableSeq! typeParams = new TypeVariableSeq();

      VariableSeq arguments = new VariableSeq();

      TypedIdent! tyd;

+     TypedIdent retTyd = null;

+     Type! retTy;

      QKeyValue kv = null;

      Expr definition = null;

      Expr! tmp;

@@ -390,12 +392,51 @@ Function<out DeclarationSeq! ds>
   [ VarOrType<out tyd>      (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)

   { "," VarOrType<out tyd>  (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)

   } ] ")"

-  "returns" "(" VarOrType<out tyd> ")"

+  ( 

+    "returns" "(" VarOrType<out tyd> ")" (. retTyd = tyd; .)

+    | 

+    ":" Type<out retTy>   (. retTyd = new TypedIdent(retTy.tok, "", retTy); .) 

+  )

   ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )

   (.

+    if (retTyd == null) {

+      // construct a dummy type for the case of syntax error

+      tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));

+    } else {

+      tyd = retTyd;

+    }

     Function! func = new Function(z, z.val, typeParams, arguments,

                            new Formal(tyd.tok, tyd, false), null, kv);

     ds.Add(func);

+    bool allUnnamed = true;

+    foreach (Formal! f in arguments) {

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

+        allUnnamed = false;

+	break;

+      }

+    }

+    if (!allUnnamed) {

+      Type prevType = null;

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

+        TypedIdent! curr = ((!)arguments[i]).TypedIdent;

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

+	  if (prevType == null) {

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

+	    break;

+	  }

+	  Type ty = curr.Type;

+          if (ty is UnresolvedTypeIdentifier &&

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

+	    curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;

+	    curr.Type = prevType;

+	  } else {

+	    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")) {

@@ -1199,9 +1240,9 @@ ArrayExpression<out Expr! e>
     (. if (store)

          e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);

        else if (bvExtract)

-         e = new ExtractExpr(x, e,

-                             ((BvBounds)index0).Upper.ToIntSafe,

-                             ((BvBounds)index0).Lower.ToIntSafe);

+         e = new BvExtractExpr(x, e,

+                               ((BvBounds)index0).Upper.ToIntSafe,

+                               ((BvBounds)index0).Lower.ToIntSafe);

        else

          e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); 

     .)

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index 8ae741ab..a7453d09 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -118,6 +118,10 @@ private class BvBounds : Expr {
 		errDist = 0;

 	}

 

+	public static void SemErr(IToken! tok, string! msg) {

+		Errors.SemErr(tok.filename, tok.line, tok.col, msg);

+	}

+

 	static void Get() {

 		for (;;) {

 			token = t;

@@ -260,6 +264,8 @@ private class BvBounds : Expr {
 		TypeVariableSeq! typeParams = new TypeVariableSeq();

 		VariableSeq arguments = new VariableSeq();

 		TypedIdent! tyd;

+		TypedIdent retTyd = null;

+		Type! retTy;

 		QKeyValue kv = null;

 		Expr definition = null;

 		Expr! tmp;

@@ -283,10 +289,17 @@ private class BvBounds : Expr {
 			}

 		}

 		Expect(9);

-		Expect(24);

-		Expect(8);

-		VarOrType(out tyd);

-		Expect(9);

+		if (t.kind == 24) {

+			Get();

+			Expect(8);

+			VarOrType(out tyd);

+			Expect(9);

+			retTyd = tyd; 

+		} else if (t.kind == 10) {

+			Get();

+			Type(out retTy);

+			retTyd = new TypedIdent(retTy.tok, "", retTy); 

+		} else Error(86);

 		if (t.kind == 25) {

 			Get();

 			Expression(out tmp);

@@ -294,42 +307,78 @@ private class BvBounds : Expr {
 			Expect(26);

 		} else if (t.kind == 7) {

 			Get();

-		} else Error(86);

+		} else Error(87);

+		if (retTyd == null) {

+		 // construct a dummy type for the case of syntax error

+		 tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));

+		} else {

+		  tyd = retTyd;

+		}

 		Function! func = new Function(z, z.val, typeParams, arguments,

-		                      new Formal(tyd.tok, tyd, false), null, kv);

+		                       new Formal(tyd.tok, tyd, false), null, kv);

 		ds.Add(func);

-		if (definition != null) {

-		  // generate either an axiom or a function body

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

-		    func.Body = definition;

+		bool allUnnamed = true;

+		foreach (Formal! f in arguments) {

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

+		    allUnnamed = false;

+		break;

+		     }

+		   }

+		   if (!allUnnamed) {

+		     Type prevType = null;

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

+		       TypedIdent! curr = ((!)arguments[i]).TypedIdent;

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

+		  if (prevType == null) {

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

+		    break;

+		  }

+		  Type ty = curr.Type;

+		         if (ty is UnresolvedTypeIdentifier &&

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

+		    curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;

+		    curr.Type = prevType;

 		  } else {

-		    VariableSeq dummies = new VariableSeq();

-		    ExprSeq callArgs = new ExprSeq();

-		    int i = 0;

-		    foreach (Formal! f in arguments) {

-		      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)

-		      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);

-		    }

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

+		    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) {

+		         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)

+		         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);

+			    }

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

+		     }

+		   }

+		 

 	}

 

 	static void Axiom(out Axiom! m) {

@@ -402,7 +451,7 @@ private class BvBounds : Expr {
 			impl = new Implementation(x, x.val, typeParams,

 			                          Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); 

 			

-		} else Error(87);

+		} else Error(88);

 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 

 	}

 

@@ -506,7 +555,7 @@ private class BvBounds : Expr {
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 

 		} else if (t.kind == 15 || t.kind == 17) {

 			MapType(out ty);

-		} else Error(88);

+		} else Error(89);

 	}

 

 	static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {

@@ -553,7 +602,7 @@ private class BvBounds : Expr {
 			Get();

 			Type(out ty);

 			Expect(9);

-		} else Error(89);

+		} else Error(90);

 	}

 

 	static void Ident(out IToken! x) {

@@ -582,7 +631,7 @@ private class BvBounds : Expr {
 		} else if (t.kind == 15 || t.kind == 17) {

 			MapType(out ty);

 			ts.Add(ty); 

-		} else Error(90);

+		} else Error(91);

 	}

 

 	static void MapType(out Bpl.Type! ty) {

@@ -754,7 +803,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			SpecPrePost(true, pre, post);

 		} else if (t.kind == 34 || t.kind == 35) {

 			SpecPrePost(false, pre, post);

-		} else Error(91);

+		} else Error(92);

 	}

 

 	static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {

@@ -782,7 +831,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				SpecBody(out locals, out blocks);

 				Expect(7);

 				pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(92);

+			} else Error(93);

 		} else if (t.kind == 35) {

 			Get();

 			tok = token; 

@@ -797,8 +846,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				SpecBody(out locals, out blocks);

 				Expect(7);

 				post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(93);

-		} else Error(94);

+			} else Error(94);

+		} else Error(95);

 	}

 

 	static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {

@@ -849,7 +898,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 			Expression(out e);

 			b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); 

-		} else Error(95);

+		} else Error(96);

 		Expect(7);

 	}

 

@@ -893,7 +942,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			CallCmd(out cn);

 			Expect(7);

 			c = cn; 

-		} else Error(96);

+		} else Error(97);

 	}

 

 	static void StmtList(out StmtList! stmtList) {

@@ -977,7 +1026,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 45) {

 			BreakCmd(out bcmd);

 			ec = bcmd; 

-		} else Error(97);

+		} else Error(98);

 	}

 

 	static void TransferCmd(out TransferCmd! tc) {

@@ -995,7 +1044,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 39) {

 			Get();

 			tc = new ReturnCmd(token); 

-		} else Error(98);

+		} else Error(99);

 		Expect(7);

 	}

 

@@ -1020,7 +1069,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				Get();

 				StmtList(out els);

 				elseOption = els; 

-			} else Error(99);

+			} else Error(100);

 		}

 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 

 	}

@@ -1079,7 +1128,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (StartOf(5)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(100);

+		} else Error(101);

 		Expect(9);

 	}

 

@@ -1117,7 +1166,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(7);

 			c = new AssignCmd(x, lhss, rhss); 

-		} else Error(101);

+		} else Error(102);

 	}

 

 	static void CallCmd(out Cmd! c) {

@@ -1180,7 +1229,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				}

 				Expect(9);

 				c = new CallCmd(x, first.val, es, ids); 

-			} else Error(102);

+			} else Error(103);

 		} else if (t.kind == 51) {

 			Get();

 			Ident(out first);

@@ -1234,7 +1283,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(9);

 			c = new CallCmd(x, first.val, es, ids); 

-		} else Error(103);

+		} else Error(104);

 	}

 

 	static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {

@@ -1274,7 +1323,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			exprOptional = e; 

-		} else Error(104);

+		} else Error(105);

 	}

 

 	static void CallOutIdent(out IToken id) {

@@ -1286,7 +1335,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 1) {

 			Ident(out p);

 			id = p; 

-		} else Error(105);

+		} else Error(106);

 	}

 

 	static void Expressions(out ExprSeq! es) {

@@ -1331,7 +1380,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 53) {

 			Get();

-		} else Error(106);

+		} else Error(107);

 	}

 

 	static void LogicalExpression(out Expr! e0) {

@@ -1369,7 +1418,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 55) {

 			Get();

-		} else Error(107);

+		} else Error(108);

 	}

 

 	static void ExpliesOp() {

@@ -1377,7 +1426,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 57) {

 			Get();

-		} else Error(108);

+		} else Error(109);

 	}

 

 	static void RelationalExpression(out Expr! e0) {

@@ -1395,7 +1444,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 59) {

 			Get();

-		} else Error(109);

+		} else Error(110);

 	}

 

 	static void OrOp() {

@@ -1403,7 +1452,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 61) {

 			Get();

-		} else Error(110);

+		} else Error(111);

 	}

 

 	static void BvTerm(out Expr! e0) {

@@ -1470,7 +1519,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			x = token; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

-		default: Error(111); break;

+		default: Error(112); break;

 		}

 	}

 

@@ -1502,7 +1551,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 72) {

 			Get();

 			x = token; op=BinaryOperator.Opcode.Sub; 

-		} else Error(112);

+		} else Error(113);

 	}

 

 	static void UnaryExpression(out Expr! e) {

@@ -1521,7 +1570,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 

 		} else if (StartOf(12)) {

 			CoercionExpression(out e);

-		} else Error(113);

+		} else Error(114);

 	}

 

 	static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {

@@ -1535,7 +1584,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 74) {

 			Get();

 			x = token; op=BinaryOperator.Opcode.Mod; 

-		} else Error(114);

+		} else Error(115);

 	}

 

 	static void NegOp() {

@@ -1543,7 +1592,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 76) {

 			Get();

-		} else Error(115);

+		} else Error(116);

 	}

 

 	static void CoercionExpression(out Expr! e) {

@@ -1567,7 +1616,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

 				}

 				

-			} else Error(116);

+			} else Error(117);

 		}

 	}

 

@@ -1677,7 +1726,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					e = new NAryExpr(x, new FunctionCall(id), es); 

 				} else if (t.kind == 9) {

 					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); 

-				} else Error(117);

+				} else Error(118);

 				Expect(9);

 			}

 			break;

@@ -1710,11 +1759,11 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 

-			} else Error(118);

+			} else Error(119);

 			Expect(9);

 			break;

 		}

-		default: Error(119); break;

+		default: Error(120); break;

 		}

 	}

 

@@ -1739,7 +1788,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 80) {

 			Get();

-		} else Error(120);

+		} else Error(121);

 	}

 

 	static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

@@ -1756,7 +1805,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			}

 		} else if (t.kind == 1) {

 			BoundVars(q, out ds);

-		} else Error(121);

+		} else Error(122);

 		QSep();

 		while (t.kind == 25) {

 			AttributeOrTrigger(ref kv, ref trig);

@@ -1769,7 +1818,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

 		} else if (t.kind == 82) {

 			Get();

-		} else Error(122);

+		} else Error(123);

 	}

 

 	static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {

@@ -1825,7 +1874,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			  trig.AddLast(new Trigger(tok, true, es, null));

 			}

 			

-		} else Error(123);

+		} else Error(124);

 		Expect(26);

 	}

 

@@ -1839,7 +1888,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			o = e; 

-		} else Error(124);

+		} else Error(125);

 	}

 

 	static void QSep() {

@@ -1847,7 +1896,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

 		} else if (t.kind == 84) {

 			Get();

-		} else Error(125);

+		} else Error(126);

 	}

 

 

@@ -1953,45 +2002,46 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			case 84: s = "\\u2022 expected"; break;

 			case 85: s = "??? expected"; break;

 			case 86: s = "invalid Function"; break;

-			case 87: s = "invalid Procedure"; break;

-			case 88: s = "invalid Type"; break;

-			case 89: s = "invalid TypeAtom"; break;

-			case 90: s = "invalid TypeArgs"; break;

-			case 91: s = "invalid Spec"; break;

-			case 92: s = "invalid SpecPrePost"; break;

+			case 87: s = "invalid Function"; break;

+			case 88: s = "invalid Procedure"; break;

+			case 89: s = "invalid Type"; break;

+			case 90: s = "invalid TypeAtom"; break;

+			case 91: s = "invalid TypeArgs"; break;

+			case 92: s = "invalid Spec"; break;

 			case 93: s = "invalid SpecPrePost"; break;

 			case 94: s = "invalid SpecPrePost"; break;

-			case 95: s = "invalid SpecBlock"; break;

-			case 96: s = "invalid LabelOrCmd"; break;

-			case 97: s = "invalid StructuredCmd"; break;

-			case 98: s = "invalid TransferCmd"; break;

-			case 99: s = "invalid IfCmd"; break;

-			case 100: s = "invalid Guard"; break;

-			case 101: s = "invalid LabelOrAssign"; break;

-			case 102: s = "invalid CallCmd"; break;

+			case 95: s = "invalid SpecPrePost"; break;

+			case 96: s = "invalid SpecBlock"; break;

+			case 97: s = "invalid LabelOrCmd"; break;

+			case 98: s = "invalid StructuredCmd"; break;

+			case 99: s = "invalid TransferCmd"; break;

+			case 100: s = "invalid IfCmd"; break;

+			case 101: s = "invalid Guard"; break;

+			case 102: s = "invalid LabelOrAssign"; break;

 			case 103: s = "invalid CallCmd"; break;

-			case 104: s = "invalid CallForallArg"; break;

-			case 105: s = "invalid CallOutIdent"; break;

-			case 106: s = "invalid EquivOp"; break;

-			case 107: s = "invalid ImpliesOp"; break;

-			case 108: s = "invalid ExpliesOp"; break;

-			case 109: s = "invalid AndOp"; break;

-			case 110: s = "invalid OrOp"; break;

-			case 111: s = "invalid RelOp"; break;

-			case 112: s = "invalid AddOp"; break;

-			case 113: s = "invalid UnaryExpression"; break;

-			case 114: s = "invalid MulOp"; break;

-			case 115: s = "invalid NegOp"; break;

-			case 116: s = "invalid CoercionExpression"; break;

-			case 117: s = "invalid AtomExpression"; break;

+			case 104: s = "invalid CallCmd"; break;

+			case 105: s = "invalid CallForallArg"; break;

+			case 106: s = "invalid CallOutIdent"; break;

+			case 107: s = "invalid EquivOp"; break;

+			case 108: s = "invalid ImpliesOp"; break;

+			case 109: s = "invalid ExpliesOp"; break;

+			case 110: s = "invalid AndOp"; break;

+			case 111: s = "invalid OrOp"; break;

+			case 112: s = "invalid RelOp"; break;

+			case 113: s = "invalid AddOp"; break;

+			case 114: s = "invalid UnaryExpression"; break;

+			case 115: s = "invalid MulOp"; break;

+			case 116: s = "invalid NegOp"; break;

+			case 117: s = "invalid CoercionExpression"; break;

 			case 118: s = "invalid AtomExpression"; break;

 			case 119: s = "invalid AtomExpression"; break;

-			case 120: s = "invalid Forall"; break;

-			case 121: s = "invalid QuantifierBody"; break;

-			case 122: s = "invalid Exists"; break;

-			case 123: s = "invalid AttributeOrTrigger"; break;

-			case 124: s = "invalid AttributeParameter"; break;

-			case 125: s = "invalid QSep"; break;

+			case 120: s = "invalid AtomExpression"; break;

+			case 121: s = "invalid Forall"; break;

+			case 122: s = "invalid QuantifierBody"; break;

+			case 123: s = "invalid Exists"; break;

+			case 124: s = "invalid AttributeOrTrigger"; break;

+			case 125: s = "invalid AttributeParameter"; break;

+			case 126: s = "invalid QSep"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc
index eb0c8b04..745f8dc4 100644
--- a/Source/Core/Scanner.ssc
+++ b/Source/Core/Scanner.ssc
@@ -1,8 +1,8 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
 using System;

 using System.IO;

 using System.Collections;

@@ -433,7 +433,7 @@ public class Scanner {
     }

   }

   

-

+
 	static bool Comment0() {

 		int level = 1, line0 = line, lineStart0 = lineStart;

 		NextCh();

@@ -456,7 +456,7 @@ public class Scanner {
 		}

 		return false;

 	}

-

+
 	static bool Comment1() {

 		int level = 1, line0 = line, lineStart0 = lineStart;

 		NextCh();

diff --git a/Source/Core/parser.frame b/Source/Core/parser.frame
index 81c7e67c..c7818e57 100644
--- a/Source/Core/parser.frame
+++ b/Source/Core/parser.frame
@@ -26,6 +26,10 @@ public class Parser {
 		errDist = 0;

 	}

 

+	public static void SemErr(IToken! tok, string! msg) {

+		Errors.SemErr(tok.filename, tok.line, tok.col, msg);

+	}

+

 	static void Get() {

 		for (;;) {

 			token = t;

@@ -96,4 +100,4 @@ public class Parser {
 } // end Parser

 

 } // end namespace

-$$$
\ No newline at end of file
+$$$

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 854ac558..c59772cd 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -953,17 +953,17 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 3 verified, 0 errors

 -------------------- fundef.bpl --------------------

 

-function {:inline true} foo(x: int) returns (bool)

+function {:inline true} foo(x: int) : bool

 {

   x > 0

 }

 

-function {:inline false} foo2(x: int) returns (bool);

+function {:inline false} foo2(x: int) : bool;

 

 // autogenerated definition axiom

 axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));

 

-function foo3(x: int) returns (bool);

+function foo3(x: int) : bool;

 

 // autogenerated definition axiom

 axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

diff --git a/Test/test0/Answer b/Test/test0/Answer
index e8ea231e..90721188 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -76,7 +76,7 @@ axiom P || Q || Q || R;
 

 axiom P && Q && Q && R;

 

-function f(int) returns (int);

+function f(int) : int;

 

 axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200);

 

@@ -87,10 +87,12 @@ Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in t
 Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

 2 type checking errors detected in Arrays1.bpl

 Types0.bpl(6,18): Error: expected identifier before ':'

-1 parse errors detected in Types0.bpl

+Types0.bpl(6,12): Error: expecting an identifier as parameter name

+2 parse errors detected in Types0.bpl

 Types1.bpl(6,11): Error: undeclared type: x

-Types1.bpl(7,18): Error: undeclared type: x

-2 name resolution errors detected in Types1.bpl

+Types1.bpl(7,11): Error: undeclared type: x

+Types1.bpl(7,14): Error: undeclared type: x

+3 name resolution errors detected in Types1.bpl

 WhereParsing.bpl(14,37): Error: where clause not allowed here

 WhereParsing.bpl(15,33): Error: where clause not allowed here

 2 parse errors detected in WhereParsing.bpl

@@ -153,7 +155,7 @@ AttributeParsingErr.bpl(20,26): Error: only attributes, not triggers, allowed he
 

 type {:sourcefile "test.ssc"} T;

 

-function {:source "test.scc"} f(int) returns (int);

+function {:source "test.scc"} f(int) : int;

 

 const {:description "The largest integer value"} unique MAXINT: int;

 

@@ -201,7 +203,7 @@ AttributeResolution.bpl(9,18): Error: undeclared identifier: mux
 AttributeResolution.bpl(11,29): Error: undeclared identifier: fux

 9 name resolution errors detected in AttributeResolution.bpl

 

-function \true() returns (bool);

+function \true() : bool;

 

 type \procedure;

 

diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl
index 09edbd12..cb69aa5f 100644
--- a/Test/test0/ModifiedBag.bpl
+++ b/Test/test0/ModifiedBag.bpl
@@ -41,19 +41,19 @@ function $RefArraySet(elements, int, ref) returns (elements);
 

 function $IntArrayGet(elements, int) returns (value: int);

 

-function $IntArraySet(elements, int, value: int) returns (elements);

+function $IntArraySet(elements, int, int) returns (elements);

 

 function $RealArrayGet(elements, int) returns (value: real);

 

-function $RealArraySet(elements, int, value: real) returns (elements);

+function $RealArraySet(elements, int, real) returns (elements);

 

 function $BoolArrayGet(elements, int) returns (value: bool);

 

-function $BoolArraySet(elements, int, value: bool) returns (elements);

+function $BoolArraySet(elements, int, bool) returns (elements);

 

 function $ArrayArrayGet(elements, int) returns (value: elements);

 

-function $ArrayArraySet(elements, int, value: elements) returns (elements);

+function $ArrayArraySet(elements, int, elements) returns (elements);

 

 axiom (forall A: elements, i: int, x: ref :: $RefArrayGet($RefArraySet(A, i, x), i) == x);

 

diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl
index f743be85..4c6e31ae 100644
--- a/Test/test0/Types1.bpl
+++ b/Test/test0/Types1.bpl
@@ -4,4 +4,4 @@ type V;
 function h(T) returns (int);

 function k(x:T) returns (int);

 function l(x) returns (int);  // resolve error

-function m(x:int, x) returns (bool);  // resolve error

+function m(x, x) returns (bool);  // resolve error

diff --git a/Test/test20/Answer b/Test/test20/Answer
index a4b991f7..efa5bced 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -87,7 +87,7 @@ type C _ _;
 

 type C2 b a = C a b;

 

-function f(C int bool) returns (int);

+function f(C int bool) : int;

 

 const x: C2 bool int;

 

@@ -108,7 +108,7 @@ type ref;
 

 type Set a = [a]bool;

 

-function union<a>(x: Set a, y: Set a) returns (Set a);

+function union<a>(x: Set a, y: Set a) : Set a;

 

 axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);

 

@@ -133,7 +133,7 @@ implementation P()
 

 type Set a = [a]bool;

 

-function union<a>(x: Set a, y: Set a) returns (Set a);

+function union<a>(x: Set a, y: Set a) : Set a;

 

 axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);

 

diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl
index 371724f5..67636af1 100644
--- a/Test/test21/InterestingExamples4.bpl
+++ b/Test/test21/InterestingExamples4.bpl
@@ -14,7 +14,7 @@ axiom (forall<a,b> x:a, y:b :: sameType(x,y) == (exists z:a :: y==z));
 // b = C^n(a)

 function rel<a,b>(x:a, y:b) returns (bool);

 

-function relHelp<a,b>(x:a, y:b, int) returns (bool);

+function relHelp<a,b>(x:a, y:b, z:int) returns (bool);

 

 axiom (forall<a, b> x:a, y:b :: relHelp(x, y, 0) == sameType(x, y));

 axiom (forall<a, b> n:int, x:a, y:b ::

diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl
index d5344449..a27f89c4 100644
--- a/Test/test21/MapAxiomsConsistency.bpl
+++ b/Test/test21/MapAxiomsConsistency.bpl
@@ -26,8 +26,8 @@ function Seq#Index<T>(Seq T, int) returns (T);
 function Seq#Contains<T>(Seq T, T) returns (bool);

 function Seq#Equal<T>(Seq T, Seq T) returns (bool);

 function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);

-function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);

-function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);

+function Seq#Take<T>(s:Seq T, howMany: int) returns (Seq T);

+function Seq#Drop<T>(s:Seq T, howMany: int) returns (Seq T);

 

 type Field _;

 type HeapType = <alpha>[ref,Field alpha]alpha;