Merge

2 files changed, 13 insertions, 13 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3d67ae0c..91028093 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -328,12 +328,12 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   .

 

 

-GIdentType<bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

-/* isGhost always returns as false if allowGhost is false */

+GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

+/* isGhost always returns as false if allowGhostKeyword is false */

 = (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

      Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

      isGhost = false; .)

-  [ "ghost"                    (. if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)

+  [ "ghost"                    (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)

   ]

   IdentType<out id, out ty>

   .

@@ -430,7 +430,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
   [ GenericParameters<typeArgs> ]

   Formals<true, !mmod.IsGhost, ins>

   [ "returns"

-    Formals<false, true, outs>

+    Formals<false, !mmod.IsGhost, outs>

   ]

 

   ( ";" { MethodSpec<req, mod, ens, dec> }

@@ -464,12 +464,12 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
   )

   .

 

-Formals<.bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals.> 

+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.> 

 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)

   "("

   [

-    GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

-    { "," GIdentType<allowGhosts, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

+    GIdentType<allowGhostKeyword, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

+    { "," GIdentType<allowGhostKeyword, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

     }

   ]

   ")"

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 4bbedb6e..100e34e1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -511,7 +511,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Formals(true, !mmod.IsGhost, ins);

 		if (la.kind == 26) {

 			Get();

-			Formals(false, true, outs);

+			Formals(false, !mmod.IsGhost, outs);

 		}

 		if (la.kind == 17) {

 			Get();

@@ -604,13 +604,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		EquivExpression(out e);

 	}

 

-	void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

+	void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

 		isGhost = false; 

 		if (la.kind == 11) {

 			Get();

-			if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 

+			if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 

 		}

 		IdentType(out id, out ty);

 	}

@@ -723,15 +723,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-	void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {

+	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 

 		Expect(32);

 		if (la.kind == 1 || la.kind == 11) {

-			GIdentType(allowGhosts, out id, out ty, out isGhost);

+			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			while (la.kind == 19) {

 				Get();

-				GIdentType(allowGhosts, out id, out ty, out isGhost);

+				GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			}

 		}