summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg14
-rw-r--r--Source/Dafny/Parser.cs12
-rw-r--r--Test/dafny0/Answer6
-rw-r--r--Test/dafny0/Basics.dfy10
4 files changed, 23 insertions, 19 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));
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b8d94b06..05250fa8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -579,6 +579,10 @@ Execution trace:
Dafny program verifier finished with 6 verified, 1 error
-------------------- Basics.dfy --------------------
+Basics.dfy(42,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
Basics.dfy(66,42): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -592,7 +596,7 @@ Execution trace:
Basics.dfy(66,95): anon18_Else
(0,0): anon12
-Dafny program verifier finished with 8 verified, 1 error
+Dafny program verifier finished with 7 verified, 2 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index c02f2c45..16fd7d87 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -1,6 +1,6 @@
class Global {
static function G(x: int): int { x+x }
- static method N(x: int) returns (ghost r: int)
+ static method N(ghost x: int) returns (ghost r: int)
ensures r == Global.G(x);
{
if {
@@ -23,8 +23,8 @@ method TestCalls(k: nat) {
ghost var r: int;
ghost var s := Global.G(k);
-// r := Global.N(k);
-// assert r == s;
+ r := Global.N(k);
+ assert r == s;
r := g.N(k);
assert r == s;
@@ -35,11 +35,11 @@ method TestCalls(k: nat) {
r := g.N(k);
assert r == s;
-// r := Global.N(r);
+ r := Global.N(r);
if (k == 0) {
assert r == s;
} else {
-// assert r == s; // error: G(k) and G(k+k) are different
+ assert r == s; // error: G(k) and G(k+k) are different
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 07:02:01 +0000