diff options
-rw-r--r-- | Source/Dafny/Compiler.cs | 35 | ||||
-rw-r--r-- | Source/Dafny/Dafny.atg | 18 | ||||
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 49 | ||||
-rw-r--r-- | Source/Dafny/Parser.cs | 131 | ||||
-rw-r--r-- | Source/Dafny/Printer.cs | 21 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 120 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 13 | ||||
-rw-r--r-- | Test/dafny0/Answer | 136 | ||||
-rw-r--r-- | Test/dafny0/ControlStructures.dfy | 105 | ||||
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 167 | ||||
-rw-r--r-- | Test/dafny1/Substitution.dfy | 2 |
11 files changed, 638 insertions, 159 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index fdab9ab9..82604794 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -609,14 +609,9 @@ namespace Microsoft.Dafny { wr.WriteLine(");");
}
} else if (stmt is BreakStmt) {
- BreakStmt s = (BreakStmt)stmt;
+ var s = (BreakStmt)stmt;
Indent(indent);
- if (s.TargetLabel == null) {
- // use the scoping rules of C#
- wr.WriteLine("break;");
- } else {
- wr.WriteLine("goto after_{0};", s.TargetLabel);
- }
+ wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);
} else if (stmt is ReturnStmt) {
Indent(indent);
wr.WriteLine("return;");
@@ -927,29 +922,11 @@ namespace Microsoft.Dafny { }
void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));
- List<string/*!*/> currentLabels = null;
foreach (Statement ss in stmts) {
- if (ss is LabelStmt) {
- LabelStmt s = (LabelStmt)ss;
- if (currentLabels == null) {
- currentLabels = new List<string>();
- }
- currentLabels.Add(s.Label);
- } else {
- TrStmt(ss, indent + IndentAmount);
- SpillLabels(currentLabels, indent);
- currentLabels = null;
- }
- }
- SpillLabels(currentLabels, indent);
- }
-
- void SpillLabels(List<string> labels, int indent) {
- Contract.Requires(cce.NonNullElements(labels));
- if (labels != null) {
- foreach (string label in labels) {
- Indent(indent);
- wr.WriteLine("after_{0}: ;", label);
+ TrStmt(ss, indent + IndentAmount);
+ if (ss.Labels != null) {
+ Indent(indent); // labels are not indented as much as the statements
+ wr.WriteLine("after_{0}: ;", ss.Labels.UniqueId);
}
}
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index b7b81d44..e3761d57 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -434,7 +434,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m> { Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
- Formals<true, true, ins>
+ Formals<true, !mmod.IsGhost, ins>
[ "returns"
Formals<false, true, outs>
]
@@ -579,7 +579,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> { Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
- Formals<true, false, formals>
+ Formals<true, isFunctionMethod, formals>
":"
Type<out returnType>
( ";"
@@ -710,6 +710,7 @@ OneStmt<out Statement/*!*/ s> = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
IToken bodyStart, bodyEnd;
+ int breakCount;
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
( BlockStmt<out s, out bodyStart, out bodyEnd>
@@ -725,10 +726,14 @@ OneStmt<out Statement/*!*/ s> | MatchStmt<out s>
| ForeachStmt<out s>
| "label" (. x = t; .)
- Ident<out id> ":" (. s = new LabelStmt(x, id.val); .)
- | "break" (. x = t; .)
- [ Ident<out id> (. label = id.val; .)
- ] ";" (. s = new BreakStmt(x, label); .)
+ Ident<out id> ":"
+ OneStmt<out s> (. s.Labels = new LabelNode(x, id.val, s.Labels); .)
+ | "break" (. x = t; breakCount = 1; label = null; .)
+ ( Ident<out id> (. label = id.val; .)
+ | { "break" (. breakCount++; .)
+ }
+ )
+ ";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
| "return" (. x = t; .)
";" (. s = new ReturnStmt(x); .)
)
@@ -751,6 +756,7 @@ UpdateStmt<out Statement/*!*/ s> { "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
";"
+ | ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
(. s = new UpdateStmt(x, lhss, rhss); .)
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8d1143af..bb5f4f67 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1141,6 +1141,8 @@ namespace Microsoft.Dafny { public abstract class Statement {
public readonly IToken Tok;
+ public LabelNode Labels; // mutable during resolution
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Tok != null);
@@ -1153,7 +1155,25 @@ namespace Microsoft.Dafny { }
}
- public abstract class PredicateStmt : Statement {
+ public class LabelNode
+ {
+ public readonly IToken Tok;
+ public readonly string Label;
+ public readonly int UniqueId;
+ public readonly LabelNode Next;
+ static int nodes = 0;
+
+ public LabelNode(IToken tok, string label, LabelNode next) {
+ Contract.Requires(tok != null);
+ Tok = tok;
+ Label = label;
+ Next = next;
+ UniqueId = nodes++;
+ }
+ }
+
+ public abstract class PredicateStmt : Statement
+ {
[Peer]
public readonly Expression Expr;
[ContractInvariantMethod]
@@ -1255,31 +1275,25 @@ namespace Microsoft.Dafny { }
}
- public class LabelStmt : Statement {
- public readonly string Label;
+ public class BreakStmt : Statement {
+ public readonly string TargetLabel;
+ public readonly int BreakCount;
+ public Statement TargetStmt; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Label != null);
+ Contract.Invariant(TargetLabel == null || 1 <= BreakCount);
}
- public LabelStmt(IToken/*!*/ tok, string/*!*/ label)
+ public BreakStmt(IToken tok, string targetLabel)
: base(tok) {
Contract.Requires(tok != null);
- Contract.Requires(label != null);
- this.Label = label;
-
+ this.TargetLabel = targetLabel;
}
- }
-
- public class BreakStmt : Statement {
- public readonly string TargetLabel;
- public Statement TargetStmt; // filled in during resolution
-
- public BreakStmt(IToken tok, string targetLabel)
+ public BreakStmt(IToken tok, int breakCount)
: base(tok) {
Contract.Requires(tok != null);
- this.TargetLabel = targetLabel;
-
+ Contract.Requires(1 <= breakCount);
+ this.BreakCount = breakCount;
}
}
@@ -1287,7 +1301,6 @@ namespace Microsoft.Dafny { public ReturnStmt(IToken tok)
: base(tok) {
Contract.Requires(tok != null);
-
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 2fa88a69..1d7eb3e6 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -466,7 +466,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 23) {
GenericParameters(typeArgs);
}
- Formals(true, false, formals);
+ Formals(true, isFunctionMethod, formals);
Expect(22);
Type(out returnType);
if (la.kind == 15) {
@@ -518,7 +518,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 23) {
GenericParameters(typeArgs);
}
- Formals(true, true, ins);
+ Formals(true, !mmod.IsGhost, ins);
if (la.kind == 26) {
Get();
Formals(false, true, outs);
@@ -996,6 +996,7 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
IToken bodyStart, bodyEnd;
+ int breakCount;
if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
@@ -1026,22 +1027,28 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
Ident(out id);
Expect(22);
- s = new LabelStmt(x, id.val);
+ OneStmt(out s);
+ s.Labels = new LabelNode(x, id.val, s.Labels);
} else if (la.kind == 48) {
Get();
- x = t;
+ x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- }
+ } else if (la.kind == 15 || la.kind == 48) {
+ while (la.kind == 48) {
+ Get();
+ breakCount++;
+ }
+ } else SynErr(120);
Expect(15);
- s = new BreakStmt(x, label);
+ s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
} else if (la.kind == 49) {
Get();
x = t;
Expect(15);
s = new ReturnStmt(x);
- } else SynErr(120);
+ } else SynErr(121);
}
void AssertStmt(out Statement/*!*/ s) {
@@ -1117,7 +1124,10 @@ List<Expression/*!*/>/*!*/ decreases) { rhss.Add(r);
}
Expect(15);
- } else SynErr(121);
+ } else if (la.kind == 22) {
+ Get();
+ SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
+ } else SynErr(122);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1199,13 +1209,13 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(122);
+ } else SynErr(123);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(123);
+ } else SynErr(124);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1230,7 +1240,7 @@ List<Expression/*!*/>/*!*/ decreases) { LoopSpec(out invariants, out decreases);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
- } else SynErr(124);
+ } else SynErr(125);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1295,7 +1305,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 56) {
HavocStmt(out s);
bodyAssign = s;
- } else SynErr(125);
+ } else SynErr(126);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1319,7 +1329,7 @@ List<Expression/*!*/>/*!*/ decreases) { while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
- } else SynErr(126);
+ } else SynErr(127);
}
void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {
@@ -1369,7 +1379,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(127);
+ } else SynErr(128);
}
void Guard(out Expression e) {
@@ -1381,7 +1391,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(128);
+ } else SynErr(129);
Expect(33);
}
@@ -1471,7 +1481,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(129);
+ } else SynErr(130);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1501,7 +1511,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 68) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1539,7 +1549,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 70) {
Get();
- } else SynErr(131);
+ } else SynErr(132);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1557,7 +1567,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 72) {
Get();
- } else SynErr(132);
+ } else SynErr(133);
}
void OrOp() {
@@ -1565,7 +1575,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 74) {
Get();
- } else SynErr(133);
+ } else SynErr(134);
}
void Term(out Expression/*!*/ e0) {
@@ -1641,7 +1651,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(134); break;
+ default: SynErr(135); break;
}
}
@@ -1663,7 +1673,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(135);
+ } else SynErr(136);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1690,7 +1700,7 @@ List<Expression/*!*/>/*!*/ decreases) { while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
- } else SynErr(136);
+ } else SynErr(137);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1704,7 +1714,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(137);
+ } else SynErr(138);
}
void NegOp() {
@@ -1712,7 +1722,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 89) {
Get();
- } else SynErr(138);
+ } else SynErr(139);
}
void EndlessExpression(out Expression e) {
@@ -1733,7 +1743,7 @@ List<Expression/*!*/>/*!*/ decreases) { QuantifierGuts(out e);
} else if (la.kind == 37) {
ComprehensionExpr(out e);
- } else SynErr(139);
+ } else SynErr(140);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1806,12 +1816,12 @@ List<Expression/*!*/>/*!*/ decreases) { multipleIndices.Add(ee);
}
- } else SynErr(140);
+ } else SynErr(141);
} else if (la.kind == 98) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(141);
+ } else SynErr(142);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1835,7 +1845,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(53);
- } else SynErr(142);
+ } else SynErr(143);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1932,7 +1942,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(33);
break;
}
- default: SynErr(143); break;
+ default: SynErr(144); break;
}
}
@@ -1963,7 +1973,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 101 || la.kind == 102) {
Exists();
x = t;
- } else SynErr(144);
+ } else SynErr(145);
IdentTypeOptional(out bv);
bvars.Add(bv);
while (la.kind == 19) {
@@ -2021,7 +2031,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 100) {
Get();
- } else SynErr(145);
+ } else SynErr(146);
}
void Exists() {
@@ -2029,7 +2039,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(146);
+ } else SynErr(147);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2042,7 +2052,7 @@ List<Expression/*!*/>/*!*/ decreases) { es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(147);
+ } else SynErr(148);
Expect(8);
}
@@ -2051,7 +2061,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 104) {
Get();
- } else SynErr(148);
+ } else SynErr(149);
}
void AttributeBody(ref Attributes attrs) {
@@ -2250,34 +2260,35 @@ public class Errors { case 118: s = "invalid PossiblyWildExpression"; break;
case 119: s = "invalid MatchOrExpr"; break;
case 120: s = "invalid OneStmt"; break;
- case 121: s = "invalid UpdateStmt"; break;
- case 122: s = "invalid IfStmt"; break;
+ case 121: s = "invalid OneStmt"; break;
+ case 122: s = "invalid UpdateStmt"; break;
case 123: s = "invalid IfStmt"; break;
- case 124: s = "invalid WhileStmt"; break;
- case 125: s = "invalid ForeachStmt"; break;
- case 126: s = "invalid Lhs"; break;
- case 127: s = "invalid Rhs"; break;
- case 128: s = "invalid Guard"; break;
- case 129: s = "invalid AttributeArg"; break;
- case 130: s = "invalid EquivOp"; break;
- case 131: s = "invalid ImpliesOp"; break;
- case 132: s = "invalid AndOp"; break;
- case 133: s = "invalid OrOp"; break;
- case 134: s = "invalid RelOp"; break;
- case 135: s = "invalid AddOp"; break;
- case 136: s = "invalid UnaryExpression"; break;
- case 137: s = "invalid MulOp"; break;
- case 138: s = "invalid NegOp"; break;
- case 139: s = "invalid EndlessExpression"; break;
- case 140: s = "invalid Suffix"; break;
+ case 124: s = "invalid IfStmt"; break;
+ case 125: s = "invalid WhileStmt"; break;
+ case 126: s = "invalid ForeachStmt"; break;
+ case 127: s = "invalid Lhs"; break;
+ case 128: s = "invalid Rhs"; break;
+ case 129: s = "invalid Guard"; break;
+ case 130: s = "invalid AttributeArg"; break;
+ case 131: s = "invalid EquivOp"; break;
+ case 132: s = "invalid ImpliesOp"; break;
+ case 133: s = "invalid AndOp"; break;
+ case 134: s = "invalid OrOp"; break;
+ case 135: s = "invalid RelOp"; break;
+ case 136: s = "invalid AddOp"; break;
+ case 137: s = "invalid UnaryExpression"; break;
+ case 138: s = "invalid MulOp"; break;
+ case 139: s = "invalid NegOp"; break;
+ case 140: s = "invalid EndlessExpression"; break;
case 141: s = "invalid Suffix"; break;
case 142: s = "invalid Suffix"; break;
- case 143: s = "invalid ConstAtomExpression"; break;
- case 144: s = "invalid QuantifierGuts"; break;
- case 145: s = "invalid Forall"; break;
- case 146: s = "invalid Exists"; break;
- case 147: s = "invalid AttributeOrTrigger"; break;
- case 148: s = "invalid QSep"; break;
+ case 143: s = "invalid Suffix"; break;
+ case 144: s = "invalid ConstAtomExpression"; break;
+ case 145: s = "invalid QuantifierGuts"; break;
+ case 146: s = "invalid Forall"; break;
+ case 147: s = "invalid Exists"; break;
+ case 148: s = "invalid AttributeOrTrigger"; break;
+ case 149: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index f5fba723..c92b477a 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -396,6 +396,13 @@ namespace Microsoft.Dafny { /// </summary>
public void PrintStatement(Statement stmt, int indent) {
Contract.Requires(stmt != null);
+ for (LabelNode label = stmt.Labels; label != null; label = label.Next) {
+ if (label.Label != null) {
+ wr.WriteLine("label {0}:", label.Label);
+ Indent(indent);
+ }
+ }
+
if (stmt is AssertStmt) {
wr.Write("assert ");
PrintExpression(((AssertStmt)stmt).Expr);
@@ -417,15 +424,17 @@ namespace Microsoft.Dafny { PrintAttributeArgs(s.Args);
wr.Write(";");
- } else if (stmt is LabelStmt) {
- wr.Write("label {0}:", ((LabelStmt)stmt).Label);
-
} else if (stmt is BreakStmt) {
BreakStmt s = (BreakStmt)stmt;
- if (s.TargetLabel == null) {
- wr.Write("break;");
- } else {
+ if (s.TargetLabel != null) {
wr.Write("break {0};", s.TargetLabel);
+ } else {
+ string sep = "";
+ for (int i = 0; i < s.BreakCount; i++) {
+ wr.Write("{0}break", sep);
+ sep = " ";
+ }
+ wr.Write(";");
}
} else if (stmt is ReturnStmt) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a7fe06ec..3eb3bd34 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -277,6 +277,8 @@ namespace Microsoft.Dafny { readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
+ readonly List<Statement> loopStack = new List<Statement>(); // the enclosing loops (from which it is possible to break out)
+ readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
/// <summary>
/// Assumes type parameters have already been pushed
@@ -1118,11 +1120,14 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
}
-
+
+ /// <summary>
+ /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
+ /// at run time. That means it must not have any side effects on non-ghost variables, for example.
+ /// </summary>
public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {
Contract.Requires(stmt != null);
Contract.Requires(method != null);
- Contract.Requires(!(stmt is LabelStmt)); // these should be handled inside lists of statements
if (stmt is UseStmt) {
UseStmt s = (UseStmt)stmt;
s.IsGhost = true;
@@ -1153,21 +1158,36 @@ namespace Microsoft.Dafny { }
} else if (stmt is BreakStmt) {
- BreakStmt s = (BreakStmt)stmt;
+ var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
Statement target = labeledStatements.Find(s.TargetLabel);
if (target == null) {
Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel);
} else {
s.TargetStmt = target;
+ bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;
+ if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {
+ Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
+ }
+ }
+ } else {
+ if (loopStack.Count < s.BreakCount) {
+ Error(s, "trying to break out of more loop levels than there are enclosing loops");
+ } else {
+ Statement target = loopStack[loopStack.Count - s.BreakCount];
+ if (target.Labels == null) {
+ // make sure there is a label, because the compiler and translator will want to see a unique ID
+ target.Labels = new LabelNode(target.Tok, null, null);
+ }
+ s.TargetStmt = target;
+ if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {
+ Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost loop");
+ }
}
- }
- if (specContextOnly) {
- Error(stmt, "break statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
} else if (stmt is ReturnStmt) {
- if (specContextOnly) {
+ if (specContextOnly && !method.IsGhost) {
Error(stmt, "return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
@@ -1301,7 +1321,7 @@ namespace Microsoft.Dafny { if (var == null) {
// the LHS didn't resolve correctly; some error would already have been reported
} else {
- lvalueIsGhost = var.IsGhost;
+ lvalueIsGhost = var.IsGhost || method.IsGhost;
if (!var.IsMutable) {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
@@ -1441,7 +1461,7 @@ namespace Microsoft.Dafny { } else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
- s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, method);
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
@@ -1473,11 +1493,16 @@ namespace Microsoft.Dafny { // any type is fine
}
s.IsGhost = bodyMustBeSpecOnly;
+ loopStack.Add(s); // push
+ if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
+ inSpecOnlyContext.Add(s, specContextOnly);
+ }
ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
+ loopStack.RemoveAt(loopStack.Count-1); // pop
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
- s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, method);
foreach (MaybeFreeExpression inv in s.Invariants) {
ResolveExpression(inv.E, true);
Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
@@ -1643,7 +1668,7 @@ namespace Microsoft.Dafny { }
}
- bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, Method method) {
+ bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {
Contract.Requires(alternatives != null);
Contract.Requires(method != null);
@@ -1661,6 +1686,13 @@ namespace Microsoft.Dafny { isGhost = isGhost || UsesSpecFeatures(alternative.Guard);
}
}
+
+ if (loopToCatchBreaks != null) {
+ loopStack.Add(loopToCatchBreaks); // push
+ if (loopToCatchBreaks.Labels == null) { // otherwise, "loopToCatchBreak" is already in "inSpecOnlyContext" map
+ inSpecOnlyContext.Add(loopToCatchBreaks, specContextOnly);
+ }
+ }
foreach (var alternative in alternatives) {
scope.PushMarker();
foreach (Statement ss in alternative.Body) {
@@ -1668,6 +1700,10 @@ namespace Microsoft.Dafny { }
scope.PopMarker();
}
+ if (loopToCatchBreaks != null) {
+ loopStack.RemoveAt(loopStack.Count - 1); // pop
+ }
+
return isGhost;
}
@@ -1795,25 +1831,33 @@ namespace Microsoft.Dafny { }
}
}
-
+
void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method)
{
Contract.Requires(blockStmt != null);
Contract.Requires(method != null);
- int labelsToPop = 0;
+
foreach (Statement ss in blockStmt.Body) {
- if (ss is LabelStmt) {
- LabelStmt ls = (LabelStmt)ss;
- labeledStatements.PushMarker();
- bool b = labeledStatements.Push(ls.Label, ls);
- Contract.Assert(b); // since we just pushed a marker, we expect the Push to succeed
- labelsToPop++;
- } else {
- ResolveStatement(ss, specContextOnly, method);
- for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
+ labeledStatements.PushMarker();
+ // push labels
+ for (var lnode = ss.Labels; lnode != null; lnode = lnode.Next) {
+ Contract.Assert(lnode.Label != null); // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet
+ var prev = labeledStatements.Find(lnode.Label);
+ if (prev == ss) {
+ Error(lnode.Tok, "duplicate label");
+ } else if (prev != null) {
+ Error(lnode.Tok, "label shadows an enclosing label");
+ } else {
+ bool b = labeledStatements.Push(lnode.Label, ss);
+ Contract.Assert(b); // since we just checked for duplicates, we expect the Push to succeed
+ if (lnode == ss.Labels) { // add it only once
+ inSpecOnlyContext.Add(ss, specContextOnly);
+ }
+ }
}
+ ResolveStatement(ss, specContextOnly, method);
+ labeledStatements.PopMarker();
}
- for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
}
Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, Method method) {
@@ -2544,25 +2588,43 @@ namespace Microsoft.Dafny { Contract.Requires(expr.Type != null); // this check approximates the requirement that "expr" be resolved
if (expr is IdentifierExpr) {
- IdentifierExpr e = (IdentifierExpr)expr;
+ var e = (IdentifierExpr)expr;
if (e.Var != null && e.Var.IsGhost) {
Error(expr, "ghost variables are allowed only in specification contexts");
return;
}
} else if (expr is FieldSelectExpr) {
- FieldSelectExpr e = (FieldSelectExpr)expr;
+ var e = (FieldSelectExpr)expr;
if (e.Field != null && e.Field.IsGhost) {
Error(expr, "ghost fields are allowed only in specification contexts");
return;
}
} else if (expr is FunctionCallExpr) {
- FunctionCallExpr e = (FunctionCallExpr)expr;
+ var e = (FunctionCallExpr)expr;
if (e.Function != null && e.Function.IsGhost) {
Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");
return;
}
+ // function is okay, so check all NON-ghost arguments
+ CheckIsNonGhost(e.Receiver);
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ if (!e.Function.Formals[i].IsGhost) {
+ CheckIsNonGhost(e.Args[i]);
+ }
+ }
+ return;
+
+ } else if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ // check all NON-ghost arguments
+ for (int i = 0; i < e.Ctor.Formals.Count; i++) {
+ if (!e.Ctor.Formals[i].IsGhost) {
+ CheckIsNonGhost(e.Arguments[i]);
+ }
+ }
+ return;
} else if (expr is OldExpr) {
Error(expr, "old expressions are allowed only in specification and ghost contexts");
@@ -2577,7 +2639,7 @@ namespace Microsoft.Dafny { return;
} else if (expr is BinaryExpr) {
- BinaryExpr e = (BinaryExpr)expr;
+ var e = (BinaryExpr)expr;
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.RankGt:
case BinaryExpr.ResolvedOpcode.RankLt:
@@ -2588,7 +2650,7 @@ namespace Microsoft.Dafny { }
} else if (expr is QuantifierExpr) {
- QuantifierExpr e = (QuantifierExpr)expr;
+ var e = (QuantifierExpr)expr;
if (e.MissingBounds != null) {
foreach (var bv in e.MissingBounds) {
Error(expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
@@ -3454,7 +3516,7 @@ namespace Microsoft.Dafny { return Contract.Exists( me.Cases,mc=> UsesSpecFeatures(mc.Body));
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
- return UsesSpecFeatures(e.ResolvedExpression);
+ return e.ResolvedExpression != null && UsesSpecFeatures(e.ResolvedExpression);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index eb1d1cca..50e7965c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2899,7 +2899,6 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-
return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
}
@@ -2912,7 +2911,6 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-
TrStmt(block, builder, locals, etran);
return builder.Collect(block.Tok); // TODO: would be nice to have an end-curly location for "block"
@@ -2961,12 +2959,10 @@ namespace Microsoft.Dafny { }
}
- } else if (stmt is LabelStmt) {
- AddComment(builder, stmt, "label statement"); // TODO: ouch, comments probably mess up what the label labels in the Boogie program
- builder.AddLabelCmd(((LabelStmt)stmt).Label);
} else if (stmt is BreakStmt) {
AddComment(builder, stmt, "break statement");
- builder.Add(new Bpl.BreakCmd(stmt.Tok, ((BreakStmt)stmt).TargetLabel)); // TODO: handle name clashes of labels
+ var s = (BreakStmt)stmt;
+ builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));
} else if (stmt is ReturnStmt) {
AddComment(builder, stmt, "return statement");
builder.Add(new Bpl.ReturnCmd(stmt.Tok));
@@ -2988,6 +2984,9 @@ namespace Microsoft.Dafny { } else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
TrStmt(ss, builder, locals, etran);
+ if (ss.Labels != null) {
+ builder.AddLabelCmd("after_" + ss.Labels.UniqueId);
+ }
}
} else if (stmt is IfStmt) {
AddComment(builder, stmt, "if statement");
@@ -3259,7 +3258,7 @@ namespace Microsoft.Dafny { locals.Add(preLoopHeapVar);
Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
- builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr)); // TODO: does this screw up labeled breaks for this loop?
+ builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
List<Bpl.Expr> initDecr = null;
if (!Contract.Exists(theDecreases, e => e is WildcardExpr)) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index efcfa8bb..d997cba1 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -403,6 +403,22 @@ Dafny program verifier finished with 3 verified, 3 errors -------------------- ResolutionErrors.dfy --------------------
ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(100,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(144,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
@@ -422,7 +438,9 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-20 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(252,2): Error: duplicate label
+38 resolution/type errors detected in ResolutionErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -597,8 +615,120 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil Execution trace:
(0,0): anon0
(0,0): anon5_Else
-
-Dafny program verifier finished with 15 verified, 6 errors
+ControlStructures.dfy(218,18): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ (0,0): anon74_Then
+ (0,0): anon29
+ControlStructures.dfy(235,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ ControlStructures.dfy(213,9): anon74_Else
+ (0,0): anon22
+ (0,0): anon75_Then
+ (0,0): after_4
+ ControlStructures.dfy(224,7): anon77_LoopHead
+ (0,0): anon77_LoopBody
+ ControlStructures.dfy(224,7): anon78_Else
+ (0,0): anon33
+ ControlStructures.dfy(224,7): anon79_Else
+ (0,0): anon35
+ (0,0): anon81_Then
+ (0,0): anon38
+ (0,0): after_9
+ (0,0): anon86_Then
+ (0,0): anon53
+ControlStructures.dfy(238,30): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon68_Then
+ (0,0): after_5
+ (0,0): anon87_Then
+ (0,0): anon88_Then
+ (0,0): anon58
+ControlStructures.dfy(241,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ ControlStructures.dfy(213,9): anon74_Else
+ (0,0): anon22
+ (0,0): anon75_Then
+ (0,0): after_4
+ ControlStructures.dfy(224,7): anon77_LoopHead
+ (0,0): anon77_LoopBody
+ ControlStructures.dfy(224,7): anon78_Else
+ (0,0): anon33
+ ControlStructures.dfy(224,7): anon79_Else
+ (0,0): anon35
+ (0,0): anon82_Then
+ (0,0): anon85_Then
+ (0,0): after_8
+ (0,0): anon89_Then
+ (0,0): anon61
+
+Dafny program verifier finished with 18 verified, 10 errors
-------------------- Termination.dfy --------------------
Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index 2c9b3a35..5012e003 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -135,3 +135,108 @@ method B(x: int) returns (r: int) r := r - 1;
}
}
+
+// --------------- breaks ---------------
+
+method TheBreaker_AllGood(M: int, N: int, O: int)
+{
+ var a, b, c, d, e;
+ var i := 0;
+ while (i < M)
+ {
+ var j := 0;
+ label InnerHasLabel:
+ while (j < N)
+ {
+ var u := 2000;
+ label MyLabelBlock:
+ label MyLabelBlockAgain:
+ if (*) {
+ a := 15; break;
+ } else if (*) {
+ b := 12; break break;
+ } else if (*) {
+ c := 21; break InnerHasLabel;
+ } else if (*) {
+ while (u < 10000) {
+ u := u + 3;
+ if (*) { u := 1998; break MyLabelBlock; }
+ if (*) { u := 1998; break MyLabelBlockAgain; }
+ }
+ assert 10000 <= u;
+ u := 1998;
+ } else {
+ u := u - 2;
+ }
+ assert u == 1998;
+ var k := 0;
+ while
+ decreases O - k;
+ {
+ case k < O && k % 2 == 0 =>
+ d := 187; break;
+ case k < O =>
+ if (*) { e := 4; break InnerHasLabel; }
+ if (*) { e := 7; break; }
+ if (*) { e := 37; break break break; }
+ k := k + 1;
+ }
+ assert O <= k || d == 187 || e == 7;
+ j := j + 1;
+ }
+ assert N <= j || a == 15 || c == 21 || e == 4;
+ i := i + 1;
+ }
+ assert M <= i || b == 12 || e == 37;
+}
+
+method TheBreaker_SomeBad(M: int, N: int, O: int)
+{
+ var a, b, c, d, e;
+ var i := 0;
+ while (i < M)
+ {
+ var j := 0;
+ label InnerHasLabel:
+ while (j < N)
+ {
+ var u := 2000;
+ label MyLabelBlock:
+ label MyLabelBlockAgain:
+ if (*) {
+ a := 15; break;
+ } else if (*) {
+ b := 12; break break;
+ } else if (*) {
+ c := 21; break InnerHasLabel;
+ } else if (*) {
+ while (u < 10000) {
+ u := u + 3;
+ if (*) { u := 1998; break MyLabelBlock; }
+ if (*) { u := 1998; break MyLabelBlockAgain; }
+ }
+ assert u < 2000; // error (and no way to get past this assert statement)
+ } else {
+ u := u - 2;
+ }
+ assert u == 1998;
+ var k := 0;
+ while
+ decreases O - k;
+ {
+ case k < O && k % 2 == 0 =>
+ d := 187; break;
+ case k < O =>
+ if (*) { e := 4; break InnerHasLabel; }
+ if (*) { e := 7; break; }
+ if (*) { e := 37; break break break; }
+ k := k + 1;
+ }
+ assert O <= k || e == 7; // error: d == 187
+ j := j + 1;
+ }
+ assert N <= j || c == 21 || e == 4; // error: a == 15
+ i := i + 1;
+ }
+ assert M <= i || b == 12; // error: e == 37
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 56d7575f..09307b2b 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -87,3 +87,170 @@ method TestNameResolution1() { var e := Eleanor;
assert Tuv(e, this.Eleanor) == 10;
}
+
+// --------------- ghost tests -------------------------------------
+
+datatype GhostDt =
+ Nil(ghost extraInfo: int) |
+ Cons(data: int, tail: GhostDt, ghost moreInfo: int);
+
+class GhostTests {
+ method M(dt: GhostDt) returns (r: int) {
+ ghost var g := 5;
+ r := g; // error: RHS is ghost, LHS is not
+ r := F(18, g); // error: RHS is a ghost and will not be available at run time
+ r := G(20, g); // it's fine to pass a ghost as a parameter to a non-ghost, because
+ // only the ghost goes away during compilation
+ r := N(22, g); // ditto
+ r := N(g, 22); // error: passing in 'g' as non-ghost parameter
+ r := P(24, 22); // error: 'P' is ghost, but its result is assigned to a non-ghost
+
+ match (dt) {
+ case Nil(gg) =>
+ case Cons(dd, tt, gg) =>
+ r := G(dd, dd); // fine
+ r := G(dd, gg); // fine
+ r := G(gg, gg); // error: cannot pass ghost 'gg' as non-ghost parameter to 'G'
+ }
+ var dd;
+ dd := GhostDt.Nil(g); // fine
+ dd := GhostDt.Cons(g, dt, 2); // error: cannot pass 'g' as non-ghost parameter
+ ghost var dtg := GhostDt.Cons(g, dt, 2); // fine, since result is ghost
+ }
+ function F(x: int, y: int): int {
+ y
+ }
+ function method G(x: int, ghost y: int): int {
+ y // error: cannot return a ghost from a non-ghost function
+ }
+ function method H(dt: GhostDt): int {
+ match dt
+ case Nil(gg) => gg // error: cannot return a ghost from a non-ghost function
+ case Cons(dd, tt, gg) => dd + gg // error: ditto
+ }
+ method N(x: int, ghost y: int) returns (r: int) {
+ r := x;
+ }
+ ghost method P(x: int, y: int) returns (r: int) {
+ ghost var g := 5;
+ r := y; // allowed, since the entire method is ghost
+ r := r + g; // fine, for the same reason
+ r := N(20, 20); // error: call to non-ghost method from ghost method is not okay
+ }
+ ghost method NiceTry()
+ ensures false;
+ {
+ while (true)
+ decreases *; // error: not allowed in ghost context
+ {
+ }
+ }
+ ghost method BreaksAreFineHere(t: int)
+ {
+ var n := 0;
+ ghost var k := 0;
+ while (true)
+ invariant n <= 112;
+ decreases 112 - n;
+ {
+ label MyStructure: {
+ if (k % 17 == 0) { break MyStructure; } // this is fine, because it's a ghost method
+ k := k + 1;
+ }
+ label MyOtherStructure:
+ if (k % 17 == 0) {
+ break MyOtherStructure;
+ } else {
+ k := k + 1;
+ }
+
+ if (n == 112) {
+ break;
+ } else if (n == t) {
+ return;
+ }
+ n := n + 1;
+ }
+ }
+ method BreakMayNotBeFineHere(ghost t: int)
+ {
+ var n := 0;
+ ghost var k := 0;
+ var p := 0;
+ while (true)
+ invariant n <= 112;
+ decreases 112 - n;
+ {
+ label MyStructure: {
+ if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
+ k := k + 1;
+ }
+ label MyOtherStructure:
+ if (k % 17 == 0) {
+ break MyOtherStructure; // this break is fine
+ } else {
+ k := k + 1;
+ }
+
+ var dontKnow;
+ if (n == 112) {
+ ghost var m := 0;
+ label LoopLabel0:
+ label LoopLabel1:
+ while (m < 200) {
+ if (m % 103 == 0) {
+ if {
+ case true => break; // fine, since this breaks out of the enclosing ghost loop
+ case true => break LoopLabel0; // fine
+ case true => break LoopLabel1; // fine
+ }
+ } else if (m % 101 == 0) {
+ break break; // error: break out of non-ghost loop from ghost context
+ }
+ m := m + 3;
+ }
+ break;
+ } else if (dontKnow == 708) {
+ var q := 0;
+ while (q < 1) {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
+ } else if (*) {
+ break break break; // error: tries to break out of more loop levels than there are
+ } else if (*) {
+ break break; // fine, since this is not a ghost context
+ } else if (k == 67) {
+ break break; // error, because this is a ghost context
+ }
+ q := q + 1;
+ }
+ } else if (n == t) {
+ return; // error: this is a ghost context trying to return from a non-ghost method
+ }
+ n := n + 1;
+ p := p + 1;
+ }
+ }
+}
+
+method DuplicateLabels(n: int) {
+ var x;
+ if (n < 7) {
+ label DuplicateLabel: x := x + 1;
+ } else {
+ label DuplicateLabel: x := x + 1;
+ }
+ label DuplicateLabel: x := x + 1;
+ label DuplicateLabel: {
+ label AnotherLabel:
+ label DuplicateLabel: // error: duplicate label
+ label OneMoreTime:
+ x := x + 1;
+ }
+ label DuplicateLabel:
+ label DuplicateLabel: // error: duplicate label
+ x := x + 1;
+ label DuplicateLabel: x := x + 1;
+
+}
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index d3e0e82e..11c8c878 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -99,7 +99,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) }
}
-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)
+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
|