diff options
| -rw-r--r-- | Source/Dafny.sln | 12 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 97 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 56 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 89 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 16 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 63 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 93 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 9 | ||||
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 7 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 3 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 7 |
14 files changed, 278 insertions, 199 deletions
diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 034dfd7b..40e71952 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -1,6 +1,6 @@
-Microsoft Visual Studio Solution File, Format Version 11.00
-# Visual Studio 2010
+Microsoft Visual Studio Solution File, Format Version 12.00
+# Visual Studio 2012
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver", "DafnyDriver\DafnyDriver.csproj", "{63400D1F-05B2-453E-9592-1EAB74B2C9CC}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline", "Dafny\DafnyPipeline.csproj", "{FE44674A-1633-4917-99F4-57635E6FA740}"
@@ -28,8 +28,8 @@ Global {63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|.NET.Build.0 = Debug|Any CPU
{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Mixed Platforms.Build.0 = Checked|Any CPU
{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|.NET.ActiveCfg = Release|Any CPU
{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Any CPU.ActiveCfg = Release|Any CPU
{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Any CPU.Build.0 = Release|Any CPU
@@ -45,8 +45,8 @@ Global {FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.Build.0 = Debug|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Mixed Platforms.Build.0 = Checked|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Release|.NET.ActiveCfg = Release|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Release|Any CPU.ActiveCfg = Release|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Release|Any CPU.Build.0 = Release|Any CPU
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index f5e8ff30..56c6edc2 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -130,16 +130,16 @@ namespace Microsoft.Dafny { // public T x; // yield-parameter
// public int y; // yield-parameter
// IEnumerator<object> _iter;
- //
+ //
// public void _MyIteratorExample(T q) {
// this.q = q;
// _iter = TheIterator();
// }
- //
+ //
// public void MoveNext(out bool more) {
// more =_iter.MoveNext();
// }
- //
+ //
// private IEnumerator<object> TheIterator() {
// // the translation of the body of the iterator, with each "yield" turning into a "yield return null;"
// yield break;
@@ -538,7 +538,7 @@ namespace Microsoft.Dafny { }
}
wr.Write(")");
-
+
wr.WriteLine(";");
Indent(ind + 2 * IndentAmount);
wr.WriteLine("}");
@@ -584,7 +584,7 @@ namespace Microsoft.Dafny { Indent(ind);
wr.WriteLine("}");
}
-
+
// destructors
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
@@ -1019,6 +1019,11 @@ namespace Microsoft.Dafny { if (s.AssumeToken != null) {
compiler.Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
}
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ if (s.Body == null) {
+ compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line);
+ }
}
}
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 74aa4abd..dd3ab8fe 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -81,7 +81,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, parser.Parse();
return parser.errors.count;
}
-public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
: this(scanner, errors) // the real work
{
// initialize readonly fields
@@ -197,9 +197,9 @@ Dafny includedFile = Path.Combine(basePath, includedFile);
fullPath = Path.GetFullPath(includedFile);
}
- defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
+ defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
}
- .)
+ .)
}
{ SubModuleDecl<defaultModule, out submodule> (. defaultModule.TopLevelDecls.Add(submodule); .)
| ClassDecl<defaultModule, out c> (. defaultModule.TopLevelDecls.Add(c); .)
@@ -226,7 +226,7 @@ Dafny .
SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;
- Attributes attrs = null; IToken/*!*/ id;
+ Attributes attrs = null; IToken/*!*/ id;
List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
List<IToken> idRefined = null, idPath = null, idAssignment = null;
ModuleDefinition module;
@@ -238,8 +238,8 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule> ( [ "abstract" (. isAbstract = true; .) ]
"module"
{ Attribute<ref attrs> }
- NoUSIdent<out id>
-
+ NoUSIdent<out id>
+
[ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)
"{" (. module.BodyStartTok = t; .)
{ SubModuleDecl<module, out sm> (. module.TopLevelDecls.Add(sm); .)
@@ -252,15 +252,15 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule> "}" (. module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent); .)
- |
+ |
"import" ["opened" (.opened = true;.)]
- NoUSIdent<out id>
+ NoUSIdent<out id>
[ "=" QualifiedName<out idPath>
(. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
| "as" QualifiedName<out idPath> ["default" QualifiedName<out idAssignment> ]
(. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .)
]
- [ SYNC ";"
+ [ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
@@ -342,7 +342,7 @@ DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt> "=" (. bodyStart = t; .)
DatatypeMemberDecl<ctors>
{ "|" DatatypeMemberDecl<ctors> }
- [ SYNC ";"
+ [ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
@@ -394,7 +394,7 @@ ArbitraryTypeDecl<ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at> NoUSIdent<out id>
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)
- [ SYNC ";"
+ [ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
@@ -618,7 +618,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> { MethodSpec<req, mod, ens, dec, ref decAttrs, ref modAttrs> }
[ BlockStmt<out body, out bodyStart, out bodyEnd>
]
- (.
+ (.
if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {
SemErr(t, "only ghost methods can have the :axiom attribute");
}
@@ -788,7 +788,7 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty> | Ident<out tok> (. gt = new List<Type/*!*/>();
path = new List<IToken>(); .)
{ (. path.Add(tok); .)
- "." Ident<out tok>
+ "." Ident<out tok>
}
[ GenericInstantiation<gt> ] (. ty = (tok.val == "real") ? (Type)Microsoft.Dafny.Type.Real : new UserDefinedType(tok, tok.val, gt, path); .)
)
@@ -1009,7 +1009,7 @@ OneStmt<out Statement/*!*/ s> SYNC
";" (. s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); .)
| ReturnStmt<out s>
- | SkeletonStmt<out s>
+ | SkeletonStmt<out s>
)
.
@@ -1023,7 +1023,7 @@ SkeletonStmt<out Statement s> Ident<out tok> (. names.Add(tok); .)
{"," Ident<out tok> (. names.Add(tok); .)
}
- ":="
+ ":="
Expression<out e, false> (. exprs.Add(e); .)
{"," Expression<out e, false> (. exprs.Add(e); .)
}
@@ -1031,7 +1031,7 @@ SkeletonStmt<out Statement s> SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");
names = null; exprs = null;
}
- .)
+ .)
]
";"
(. s = new SkeletonStatement(dotdotdot, t, names, exprs); .)
@@ -1417,10 +1417,11 @@ ForallStmt<out Statement/*!*/ s> var ens = new List<MaybeFreeExpression/*!*/>();
bool isFree;
Expression/*!*/ e;
- BlockStmt/*!*/ block;
+ BlockStmt block = null;
IToken bodyStart, bodyEnd;
+ IToken tok = Token.NoToken;
.)
- ( "forall" (. x = t; .)
+ ( "forall" (. x = t; tok = x; .)
| "parallel" (. x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
.)
@@ -1441,10 +1442,20 @@ ForallStmt<out Statement/*!*/ s> { (. isFree = false; .)
[ "free" (. isFree = true; .)
]
- "ensures" Expression<out e, false> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
+ "ensures" Expression<out e, false> (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
+ ";" (. tok = t; .)
}
- BlockStmt<out block, out bodyStart, out bodyEnd>
- (. s = new ForallStmt(x, block.EndTok, bvars, attrs, range, ens, block); .)
+ [ BlockStmt<out block, out bodyStart, out bodyEnd>
+ ]
+ (. if (DafnyOptions.O.DisallowSoundnessCheating && block == null && 0 < ens.Count) {
+ SemErr(t, "a forall statement with an ensures clause must have a body");
+ }
+
+ if (block != null) {
+ tok = block.EndTok;
+ }
+ s = new ForallStmt(x, tok, bvars, attrs, range, ens, block);
+ .)
.
ModifyStmt<out Statement s>
@@ -1478,9 +1489,9 @@ ModifyStmt<out Statement s> CalcStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
- CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
+ CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
var lines = new List<Expression/*!*/>();
- var hints = new List<BlockStmt/*!*/>();
+ var hints = new List<BlockStmt/*!*/>();
CalcStmt.CalcOp stepOp;
var stepOps = new List<CalcStmt.CalcOp>();
CalcStmt.CalcOp maybeOp;
@@ -1494,7 +1505,7 @@ CalcStmt<out Statement/*!*/ s> if (maybeOp == null) {
SemErr(opTok, "the main operator of a calculation must be transitive");
}
- resOp = calcOp;
+ resOp = calcOp;
.)
]
"{"
@@ -1522,8 +1533,8 @@ CalcStmt<out Statement/*!*/ s> if (lines.Count > 0) {
// Repeat the last line to create a dummy line for the dangling hint
lines.Add(lines[lines.Count - 1]);
- }
- s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);
+ }
+ s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);
.)
.
CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
@@ -1543,9 +1554,9 @@ CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op> | '\u2265' (. x = t; binOp = BinaryExpr.Opcode.Ge; .)
| EquivOp (. x = t; binOp = BinaryExpr.Opcode.Iff; .)
| ImpliesOp (. x = t; binOp = BinaryExpr.Opcode.Imp; .)
- | ExpliesOp (. x = t; binOp = BinaryExpr.Opcode.Exp; .)
+ | ExpliesOp (. x = t; binOp = BinaryExpr.Opcode.Exp; .)
)
- (.
+ (.
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
} else {
@@ -1555,7 +1566,7 @@ CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op> .
Hint<out BlockStmt s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
- var subhints = new List<Statement/*!*/>();
+ var subhints = new List<Statement/*!*/>();
IToken bodyStart, bodyEnd;
BlockStmt/*!*/ block;
Statement/*!*/ calc;
@@ -1565,7 +1576,7 @@ Hint<out BlockStmt s> { BlockStmt<out block, out bodyStart, out bodyEnd> (. endTok = block.EndTok; subhints.Add(block); .)
| CalcStmt<out calc> (. endTok = calc.EndTok; subhints.Add(calc); .)
}
- (. s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
+ (. s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
.)
.
/*------------------------------------------------------------------------*/
@@ -1745,7 +1756,7 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k> [ "#" "[" Expression<out k, true> "]" ]
| "in" (. x = t; op = BinaryExpr.Opcode.In; .)
| notIn (. x = t; op = BinaryExpr.Opcode.NotIn; .)
- | /* The next operator is "!!", but we have to scan it as two "!", since the scanner is gready
+ | /* The next operator is "!!", but we have to scan it as two "!", since the scanner is gready
so if "!!" is a valid token, we won't be able to scan it as two "!" when needed: */
"!" (. x = t; y = Token.NoToken; .)
[ "!" (. y = t; .)
@@ -1854,18 +1865,18 @@ ConstAtomExpression<out Expression e> ")"
| "real" (. x = t; .)
"(" (. IToken openParen = t; .)
- Expression<out e, true>
+ Expression<out e, true>
")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
.)
| "int" (. x = t; .)
"(" (. IToken openParen = t; .)
- Expression<out e, true>
+ Expression<out e, true>
")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
.)
)
@@ -2051,10 +2062,10 @@ CasePattern<out CasePattern pat> // later if resolution finds the CasePattern to denote a parameter-less constructor), because this
// (in particular, bv.IsGhost) is the place where a LetExpr records whether or not the "ghost"
// keyword was used in the declaration.
- pat = new CasePattern(bv.tok, bv);
+ pat = new CasePattern(bv.tok, bv);
.)
)
-
+
.
/*------------------------------------------------------------------------*/
DottedIdentifiersAndFunction<out Expression e>
@@ -2108,9 +2119,9 @@ Suffix<ref Expression e> multipleLengths = new List<Expression>();
multipleLengths.Add(e0);
}
- takeRest = true;
+ takeRest = true;
.)
- [Expression<out ee, true> (. multipleLengths.Add(ee);
+ [Expression<out ee, true> (. multipleLengths.Add(ee);
takeRest = false;
.)
]
@@ -2310,7 +2321,7 @@ IdentOrDigitsSuffix<out IToken x, out IToken y> // Identifier, disallowing leading underscores
NoUSIdent<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
- ident (. x = t;
+ ident (. x = t;
if (x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
@@ -2320,7 +2331,7 @@ NoUSIdent<out IToken/*!*/ x> // Identifier, disallowing leading underscores, except possibly the "wildcard" identifier "_"
WildIdent<out IToken/*!*/ x, bool allowWildcardId>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
- ident (. x = t;
+ ident (. x = t;
if (x.val.StartsWith("_")) {
if (allowWildcardId && x.val.Length == 1) {
t.val = "_v" + anonymousIds++;
@@ -2341,7 +2352,7 @@ Nat<out BigInteger n> n = BigInteger.Zero;
}
.)
- |hexdigits
+ |hexdigits
(. try {
// note: leading 0 required when parsing positive hex numbers
n = BigInteger.Parse("0" + t.val.Substring(2), System.Globalization.NumberStyles.HexNumber);
@@ -2361,7 +2372,7 @@ Dec<out Basetypes.BigDec d> SemErr("incorrectly formatted number");
d = Basetypes.BigDec.ZERO;
}
- .)
+ .)
)
.
END Dafny.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0ffb8410..e7b36227 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -648,7 +648,7 @@ namespace Microsoft.Dafny { else
this.Path = new List<IToken>();
}
-
+
/// <summary>
/// This constructor constructs a resolved type parameter
/// </summary>
@@ -882,7 +882,7 @@ namespace Microsoft.Dafny { /// Domain and Range refer to the types of the indexing operation. That is, in A[i],
/// i is of type Domain and A[i] is of type Range.
/// Arg is either Domain or Range, depending on what type it is. Arg is the type
- /// one would use in an expression "x in C", whereas
+ /// one would use in an expression "x in C", whereas
/// This proxy stands for one of:
/// seq(T) Domain,Range,Arg := int,T,T
/// multiset(T) Domain,Range,Arg := T,int,T
@@ -1051,7 +1051,7 @@ namespace Microsoft.Dafny { public ModuleDecl CompileRoot;
public readonly List<IToken> CompilePath;
public ModuleSignature OriginalSignature;
-
+
public ModuleFacadeDecl(List<IToken> path, IToken name, ModuleDefinition parent, List<IToken> compilePath, bool opened)
: base(name, name.val, parent, opened) {
Path = path;
@@ -1061,7 +1061,7 @@ namespace Microsoft.Dafny { }
public class ModuleSignature {
-
+
public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();
public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();
public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();
@@ -1082,15 +1082,15 @@ namespace Microsoft.Dafny { } else return false;
} else return false;
}
-
-
+
+
}
public class ModuleDefinition : TopLevelDecl {
public readonly List<IToken> RefinementBaseName; // null if no refinement base
public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0]
public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base)
public List<Include> Includes;
-
+
public readonly List<TopLevelDecl> TopLevelDecls = new List<TopLevelDecl>(); // filled in by the parser; readonly after that
public readonly Graph<ICallable> CallGraph = new Graph<ICallable>(); // filled in during resolution
public int Height; // height in the topological sorting of modules; filled in during resolution
@@ -1505,9 +1505,9 @@ namespace Microsoft.Dafny { public class NoContext : ICodeContext
{
public readonly ModuleDefinition Module;
- public NoContext(ModuleDefinition module)
+ public NoContext(ModuleDefinition module)
{
- this.Module = module;
+ this.Module = module;
}
bool ICodeContext.IsGhost { get { return true; } }
bool ICodeContext.IsStatic { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
@@ -3490,7 +3490,6 @@ namespace Microsoft.Dafny { Contract.Invariant(Range != null);
Contract.Invariant(BoundVars.Count != 0 || LiteralExpr.IsTrue(Range));
Contract.Invariant(Ens != null);
- Contract.Invariant(Body != null);
}
public ForallStmt(IToken tok, IToken endTok, List<BoundVar> boundVars, Attributes attrs, Expression range, List<MaybeFreeExpression> ens, Statement body)
@@ -3501,7 +3500,6 @@ namespace Microsoft.Dafny { Contract.Requires(range != null);
Contract.Requires(boundVars.Count != 0 || LiteralExpr.IsTrue(range));
Contract.Requires(cce.NonNullElements(ens));
- Contract.Requires(body != null);
this.BoundVars = boundVars;
this.Attributes = attrs;
this.Range = range;
@@ -3535,7 +3533,9 @@ namespace Microsoft.Dafny { public override IEnumerable<Statement> SubStatements {
get {
- yield return Body;
+ if (Body != null) {
+ yield return Body;
+ }
}
}
public override IEnumerable<Expression> SubExpressions {
@@ -3641,7 +3641,7 @@ namespace Microsoft.Dafny { var op2 = other.Op;
if (op1 == BinaryExpr.Opcode.Neq || op2 == BinaryExpr.Opcode.Neq)
return op2 == BinaryExpr.Opcode.Eq;
- if (op1 == op2)
+ if (op1 == op2)
return true;
if (LogicOp(op1) || LogicOp(op2))
return op2 == BinaryExpr.Opcode.Eq ||
@@ -3733,7 +3733,7 @@ namespace Microsoft.Dafny { public readonly List<Expression> Steps; // expressions li op l<i + 1>, filled in during resolution (last step is dummy)
public Expression Result; // expression l0 ResultOp ln, filled in during resolution
- public static readonly CalcOp DefaultOp = new BinaryCalcOp(BinaryExpr.Opcode.Eq);
+ public static readonly CalcOp DefaultOp = new BinaryCalcOp(BinaryExpr.Opcode.Eq);
[ContractInvariantMethod]
void ObjectInvariant()
@@ -3775,7 +3775,7 @@ namespace Microsoft.Dafny { } else {
this.ResultOp = resultOp;
}
- this.Steps = new List<Expression>();
+ this.Steps = new List<Expression>();
this.Result = null;
}
@@ -3942,7 +3942,7 @@ namespace Microsoft.Dafny { Contract.Requires(endTok != null);
NameReplacements = nameReplacements;
ExprReplacements = exprReplacements;
-
+
}
public override IEnumerable<Statement> SubStatements {
get {
@@ -4180,7 +4180,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Create a resolved expression for a bool b
- /// </summary>
+ /// </summary>
public static Expression CreateBoolLiteral(IToken tok, bool b) {
Contract.Requires(tok != null);
var lit = new LiteralExpr(tok, b);
@@ -4285,7 +4285,7 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result<MatchCaseExpr>() != null);
ResolvedCloner cloner = new ResolvedCloner();
- var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);
+ var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);
new_body = VarSubstituter(old_case.Arguments.ConvertAll<NonglobalVariable>(x=>(NonglobalVariable)x), newVars, new_body);
var new_case = new MatchCaseExpr(old_case.tok, old_case.Id, newVars, new_body);
@@ -4295,7 +4295,7 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// Create a match expression with a resolved type
+ /// Create a match expression with a resolved type
/// </summary>
public static Expression CreateMatch(IToken tok, Expression src, List<MatchCaseExpr> cases, Type type) {
MatchExpr e = new MatchExpr(tok, src, cases);
@@ -4303,7 +4303,7 @@ namespace Microsoft.Dafny { return e;
}
-
+
/// <summary>
/// Create a let expression with a resolved type and fresh variables
/// </summary>
@@ -4343,22 +4343,22 @@ namespace Microsoft.Dafny { }
body = VarSubstituter(expr.BoundVars.ConvertAll<NonglobalVariable>(x=>(NonglobalVariable)x), newVars, body);
-
+
QuantifierExpr q;
if (forall) {
q = new ForallExpr(expr.tok, newVars, expr.Range, body, expr.Attributes);
} else {
q = new ExistsExpr(expr.tok, newVars, expr.Range, body, expr.Attributes);
- }
+ }
q.Type = Type.Bool;
- return q;
+ return q;
}
public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e) {
Contract.Requires(oldVars != null && newVars != null);
Contract.Requires(oldVars.Count == newVars.Count);
-
+
Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
@@ -4383,7 +4383,7 @@ namespace Microsoft.Dafny { {
public readonly Type UnresolvedType;
- public StaticReceiverExpr(IToken tok, Type t)
+ public StaticReceiverExpr(IToken tok, Type t)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(t != null);
@@ -4453,7 +4453,7 @@ namespace Microsoft.Dafny { this.Value = b;
}
}
-
+
public class DatatypeValue : Expression {
public readonly string DatatypeName;
public readonly string MemberName;
@@ -4563,7 +4563,7 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(elements));
}
}
-
+
public class MultiSetDisplayExpr : DisplayExpression {
public MultiSetDisplayExpr(IToken tok, List<Expression> elements) : base(tok, elements) {
Contract.Requires(tok != null);
@@ -5694,7 +5694,7 @@ namespace Microsoft.Dafny { public class MaybeFreeExpression {
public readonly Expression E;
public readonly bool IsFree;
-
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(E != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index bc89b6f1..d0a205df 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -107,7 +107,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, parser.Parse();
return parser.errors.count;
}
-public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
: this(scanner, errors) // the real work
{
// initialize readonly fields
@@ -248,7 +248,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { includedFile = Path.Combine(basePath, includedFile);
fullPath = Path.GetFullPath(includedFile);
}
- defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
+ defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
}
}
@@ -302,7 +302,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { void SubModuleDecl(ModuleDefinition parent, out ModuleDecl submodule) {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;
- Attributes attrs = null; IToken/*!*/ id;
+ Attributes attrs = null; IToken/*!*/ id;
List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
List<IToken> idRefined = null, idPath = null, idAssignment = null;
ModuleDefinition module;
@@ -598,7 +598,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { void NoUSIdent(out IToken/*!*/ x) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
- x = t;
+ x = t;
if (x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
@@ -1028,7 +1028,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { void WildIdent(out IToken/*!*/ x, bool allowWildcardId) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
- x = t;
+ x = t;
if (x.val.StartsWith("_")) {
if (allowWildcardId && x.val.Length == 1) {
t.val = "_v" + anonymousIds++;
@@ -1977,12 +1977,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo var ens = new List<MaybeFreeExpression/*!*/>();
bool isFree;
Expression/*!*/ e;
- BlockStmt/*!*/ block;
+ BlockStmt block = null;
IToken bodyStart, bodyEnd;
+ IToken tok = Token.NoToken;
if (la.kind == 85) {
Get();
- x = t;
+ x = t; tok = x;
} else if (la.kind == 86) {
Get();
x = t;
@@ -2005,7 +2006,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 33) {
Get();
if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); }
- } else if (la.kind == 9 || la.kind == 46 || la.kind == 48) {
+ } else if (StartOf(21)) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
} else SynErr(188);
while (la.kind == 46 || la.kind == 48) {
@@ -2016,19 +2017,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(48);
Expression(out e, false);
- Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree));
+ Expect(8);
+ tok = t;
+ }
+ if (la.kind == 9) {
+ BlockStmt(out block, out bodyStart, out bodyEnd);
+ }
+ if (DafnyOptions.O.DisallowSoundnessCheating && block == null && 0 < ens.Count) {
+ SemErr(t, "a forall statement with an ensures clause must have a body");
+ }
+
+ if (block != null) {
+ tok = block.EndTok;
}
- BlockStmt(out block, out bodyStart, out bodyEnd);
- s = new ForallStmt(x, block.EndTok, bvars, attrs, range, ens, block);
+ s = new ForallStmt(x, tok, bvars, attrs, range, ens, block);
+
}
void CalcStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
- CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
+ CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
var lines = new List<Expression/*!*/>();
- var hints = new List<BlockStmt/*!*/>();
+ var hints = new List<BlockStmt/*!*/>();
CalcStmt.CalcOp stepOp;
var stepOps = new List<CalcStmt.CalcOp>();
CalcStmt.CalcOp maybeOp;
@@ -2039,13 +2051,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(88);
x = t;
- if (StartOf(21)) {
+ if (StartOf(22)) {
CalcOp(out opTok, out calcOp);
maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)
if (maybeOp == null) {
SemErr(opTok, "the main operator of a calculation must be transitive");
}
- resOp = calcOp;
+ resOp = calcOp;
}
Expect(9);
@@ -2053,7 +2065,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false);
lines.Add(e); stepOp = calcOp; danglingOperator = null;
Expect(8);
- if (StartOf(21)) {
+ if (StartOf(22)) {
CalcOp(out opTok, out op);
maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
@@ -2078,8 +2090,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (lines.Count > 0) {
// Repeat the last line to create a dummy line for the dangling hint
lines.Add(lines[lines.Count - 1]);
- }
- s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);
+ }
+ s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);
}
@@ -2095,7 +2107,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) {
Attribute(ref attrs);
}
- if (StartOf(22)) {
+ if (StartOf(23)) {
if (StartOf(12)) {
FrameExpression(out fe);
mod.Add(fe);
@@ -2136,7 +2148,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
returnTok = t; isYield = true;
} else SynErr(191);
- if (StartOf(23)) {
+ if (StartOf(24)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 30) {
@@ -2252,7 +2264,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
- } else if (StartOf(24)) {
+ } else if (StartOf(25)) {
ConstAtomExpression(out e);
Suffix(ref e);
while (la.kind == 61 || la.kind == 74) {
@@ -2317,7 +2329,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(25)) {
+ while (StartOf(26)) {
if (la.kind == 46 || la.kind == 81) {
Invariant(out invariant);
while (!(la.kind == 0 || la.kind == 8)) {SynErr(195); Get();}
@@ -2514,7 +2526,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Hint(out BlockStmt s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
- var subhints = new List<Statement/*!*/>();
+ var subhints = new List<Statement/*!*/>();
IToken bodyStart, bodyEnd;
BlockStmt/*!*/ block;
Statement/*!*/ calc;
@@ -2530,7 +2542,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo endTok = calc.EndTok; subhints.Add(calc);
}
}
- s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
+ s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
}
@@ -2572,7 +2584,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpliesExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
- if (StartOf(26)) {
+ if (StartOf(27)) {
if (la.kind == 98 || la.kind == 99) {
ImpliesOp();
x = t;
@@ -2596,7 +2608,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void LogicalExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0, allowSemi);
- if (StartOf(27)) {
+ if (StartOf(28)) {
if (la.kind == 102 || la.kind == 103) {
AndOp();
x = t;
@@ -2650,7 +2662,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Term(out e0, allowSemi);
e = e0;
- if (StartOf(28)) {
+ if (StartOf(29)) {
RelOp(out x, out op, out k);
firstOpTok = x;
Term(out e1, allowSemi);
@@ -2663,7 +2675,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
}
- while (StartOf(28)) {
+ while (StartOf(29)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -2930,7 +2942,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e, allowSemi);
- } else if (StartOf(29)) {
+ } else if (StartOf(30)) {
SemErr("map must be followed by literal in brackets or comprehension.");
} else SynErr(210);
break;
@@ -3106,11 +3118,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleLengths = new List<Expression>();
multipleLengths.Add(e0);
}
- takeRest = true;
+ takeRest = true;
if (StartOf(16)) {
Expression(out ee, true);
- multipleLengths.Add(ee);
+ multipleLengths.Add(ee);
takeRest = false;
}
@@ -3223,7 +3235,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true);
e = new MultiSetFormingExpr(x, e);
Expect(33);
- } else if (StartOf(30)) {
+ } else if (StartOf(31)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
} else SynErr(219);
}
@@ -3339,7 +3351,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(33);
IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
break;
@@ -3353,7 +3365,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(33);
IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
break;
@@ -3587,7 +3599,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo pat = new CasePattern(id, id.val, arguments);
} else if (la.kind == 1) {
IdentTypeOptional(out bv);
- pat = new CasePattern(bv.tok, bv);
+ pat = new CasePattern(bv.tok, bv);
} else SynErr(226);
}
@@ -3641,7 +3653,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(7);
Expect(1);
aName = t.val;
- if (StartOf(31)) {
+ if (StartOf(32)) {
AttributeArg(out aArg, true);
aArgs.Add(aArg);
while (la.kind == 30) {
@@ -3687,6 +3699,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {T,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
{x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,T,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
{x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
@@ -3695,8 +3708,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,T, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,T, x,T,T,T, x,T,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, T,T,x,x},
- {x,x,x,x, x,x,x,T, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,x,x, x,x,T,T, x,T,T,T, x,T,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, T,T,x,x},
+ {x,T,T,T, T,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,T,T,x, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x},
+ {x,T,T,T, T,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,T,x,x, x,T,T,T, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x},
{x,T,T,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}
};
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index bf9214b9..8239fb75 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -48,7 +48,7 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null);
using (var wr = new System.IO.StringWriter()) {
var pr = new Printer(wr);
- pr.PrintExtendedExpr(expr, 0, true, false);
+ pr.PrintExtendedExpr(expr, 0, true, false);
return wr.ToString();
}
}
@@ -560,7 +560,7 @@ namespace Microsoft.Dafny { }
}
- internal void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent) {
+ internal void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent, bool newLine = true) {
Contract.Requires(kind != null);
Contract.Requires(ee != null);
foreach (MaybeFreeExpression e in ee)
@@ -577,7 +577,11 @@ namespace Microsoft.Dafny { wr.Write(" ");
PrintExpression(e.E, true);
- wr.WriteLine(";");
+ if (newLine) {
+ wr.WriteLine(";");
+ } else {
+ wr.Write(";");
+ }
}
}
@@ -730,10 +734,12 @@ namespace Microsoft.Dafny { wr.Write(" ");
} else {
wr.WriteLine();
- PrintSpec("ensures", s.Ens, indent + IndentAmount);
+ PrintSpec("ensures", s.Ens, indent + IndentAmount, s.Body != null);
Indent(indent);
}
- PrintStatement(s.Body, indent);
+ if (s.Body != null) {
+ PrintStatement(s.Body, indent);
+ }
} else if (stmt is ModifyStmt) {
var s = (ModifyStmt)stmt;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9d1e96ce..a194390c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -192,7 +192,7 @@ namespace Microsoft.Dafny var refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, prog);
rewriters.Add(refinementTransformer);
rewriters.Add(new AutoContractsRewriter());
- var opaqueRewriter = new OpaqueFunctionRewriter();
+ var opaqueRewriter = new OpaqueFunctionRewriter();
rewriters.Add(new AutoReqFunctionRewriter(this, opaqueRewriter));
rewriters.Add(opaqueRewriter);
@@ -201,7 +201,7 @@ namespace Microsoft.Dafny if (decl is LiteralModuleDecl) {
// The declaration is a literal module, so it has members and such that we need
// to resolve. First we do refinement transformation. Then we construct the signature
- // of the module. This is the public, externally visible signature. Then we add in
+ // of the module. This is the public, externally visible signature. Then we add in
// everything that the system defines, as well as any "import" (i.e. "opened" modules)
// directives (currently not supported, but this is where we would do it.) This signature,
// which is only used while resolving the members of the module is stored in the (basically)
@@ -1953,7 +1953,7 @@ namespace Microsoft.Dafny /// Note, the current implementation is rather conservative in its analysis; upon need, the
/// algorithm could be improved.
/// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
- ///
+ ///
/// The incoming value of "tailCall" is not used, but it's nevertheless a 'ref' parameter to allow the
/// body to return the incoming value or to omit assignments to it.
/// If the return value is CanBeFollowedByAnything, "tailCall" is unchanged.
@@ -2083,7 +2083,10 @@ namespace Microsoft.Dafny }
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
- var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
+ var status = TailRecursionStatus.NotTailRecursive;
+ if (s.Body != null) {
+ status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
+ }
if (status != TailRecursionStatus.CanBeFollowedByAnything) {
if (status == TailRecursionStatus.NotTailRecursive) {
// an error has already been reported
@@ -2790,13 +2793,13 @@ namespace Microsoft.Dafny /// datatype has some value that can be constructed from datatypes in lower stratospheres only.
/// The algorithm used here is quadratic in the number of datatypes in the SCC. Since that number is
/// deemed to be rather small, this seems okay.
- ///
+ ///
/// As a side effect of this checking, the DefaultCtor field is filled in (for every inductive datatype
/// that passes the check). It may be that several constructors could be used as the default, but
/// only the first one encountered as recorded. This particular choice is slightly more than an
/// implementation detail, because it affects how certain cycles among inductive datatypes (having
/// to do with the types used to instantiate type parameters of datatypes) are used.
- ///
+ ///
/// The role of the SCC here is simply to speed up this method. It would still be correct if the
/// equivalence classes in the given SCC were unions of actual SCC's. In particular, this method
/// would still work if "dependencies" consisted of one large SCC containing all the inductive
@@ -3984,7 +3987,7 @@ namespace Microsoft.Dafny // set(Arg) or multiset(Arg) or seq(Arg) or map(Arg, anyRange)
// pb is:
// seq(Arg) or multiset(Arg) or map(Domain, Arg), or
- // if AllowArray, array(Arg)
+ // if AllowArray, array(Arg)
// Their intersection is:
if (ib.AllowArray) {
var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, false);
@@ -4497,14 +4500,16 @@ namespace Microsoft.Dafny }
s.IsGhost = bodyMustBeSpecOnly;
- // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
- var prevLblStmts = labeledStatements;
- var prevLoopStack = loopStack;
- labeledStatements = new Scope<Statement>();
- loopStack = new List<Statement>();
- ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
- labeledStatements = prevLblStmts;
- loopStack = prevLoopStack;
+ if (s.Body != null) {
+ // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
+ var prevLblStmts = labeledStatements;
+ var prevLoopStack = loopStack;
+ labeledStatements = new Scope<Statement>();
+ loopStack = new List<Statement>();
+ ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+ labeledStatements = prevLblStmts;
+ loopStack = prevLoopStack;
+ }
scope.PopMarker();
if (prevErrorCount == ErrorCount) {
@@ -4541,9 +4546,11 @@ namespace Microsoft.Dafny }
}
}
- CheckForallStatementBodyRestrictions(s.Body, s.Kind);
+ if (s.Body != null) {
+ CheckForallStatementBodyRestrictions(s.Body, s.Kind);
+ }
}
-
+
} else if (stmt is ModifyStmt) {
var s = (ModifyStmt)stmt;
ResolveAttributes(s.Mod.Attributes, true, codeContext);
@@ -4572,14 +4579,14 @@ namespace Microsoft.Dafny if (!UnifyTypes(e0.Type, e1.Type)) {
Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
} else {
- var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
+ var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
ResolveExpression(step, true, codeContext);
- s.Steps.Add(step);
+ s.Steps.Add(step);
}
e0 = e1;
}
}
-
+
// clear the labels for the duration of checking the hints, because break statements are not allowed to leave a forall statement
var prevLblStmts = labeledStatements;
var prevLoopStack = loopStack;
@@ -4590,7 +4597,7 @@ namespace Microsoft.Dafny CheckHintRestrictions(h);
}
labeledStatements = prevLblStmts;
- loopStack = prevLoopStack;
+ loopStack = prevLoopStack;
}
if (prevErrorCount == ErrorCount && s.Lines.Count > 0) {
@@ -4600,8 +4607,8 @@ namespace Microsoft.Dafny s.Result = CalcStmt.DefaultOp.StepExpr(Expression.CreateIntLiteral(s.Tok, 0), Expression.CreateIntLiteral(s.Tok, 0));
}
ResolveExpression(s.Result, true, codeContext);
- Contract.Assert(s.Result != null);
- Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
+ Contract.Assert(s.Result != null);
+ Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
@@ -5327,7 +5334,7 @@ namespace Microsoft.Dafny Contract.Assert(false); // unexpected kind
break;
}
-
+
} else if (stmt is CalcStmt) {
// cool
@@ -5446,7 +5453,7 @@ namespace Microsoft.Dafny Contract.Assert(false); // unexpected kind
break;
}
-
+
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
foreach (var h in s.Hints) {
@@ -5990,10 +5997,10 @@ namespace Microsoft.Dafny }
else if (e.Seq.Type is UserDefinedType && ((UserDefinedType)e.Seq.Type).IsDatatype)
- {
+ {
DatatypeDecl dt = ((UserDefinedType)e.Seq.Type).AsDatatype;
- if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger)))
+ if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger)))
{
Error(expr, "datatype updates must be to datatype destructors");
} else {
@@ -7219,7 +7226,7 @@ namespace Microsoft.Dafny if (p < e.Tokens.Count) {
Contract.Assert(e.Arguments != null);
-
+
bool itIsAMethod = false;
if (allowMethodCall) {
var udt = r.Type.Normalize() as UserDefinedType;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b1622efd..c441a8b6 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -327,9 +327,9 @@ namespace Microsoft.Dafny { public Bpl.Program Translate(Program p) {
Contract.Requires(p != null);
Contract.Ensures(Contract.Result<Bpl.Program>() != null);
-
+
program = p;
-
+
if (sink == null || predef == null) {
// something went wrong during construction, which reads the prelude; an error has
// already been printed, so just return an empty program here (which is non-null)
@@ -579,7 +579,7 @@ namespace Microsoft.Dafny { rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));
- sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
} else if (arg.Type is SetType) {
// axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
// that is:
@@ -626,7 +626,7 @@ namespace Microsoft.Dafny { {
InsertChecksum(dt, cases_fn);
}
-
+
sink.TopLevelDeclarations.Add(cases_fn);
// and here comes the actual axiom:
{
@@ -717,7 +717,7 @@ namespace Microsoft.Dafny { {
InsertChecksum(dt, fn);
}
-
+
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall d0, d1: DatatypeType :: { $Eq#Dt(d0, d1) } $Eq#Dt(d0, d1) <==>
@@ -845,7 +845,7 @@ namespace Microsoft.Dafny { {
InsertChecksum(dt, fn);
}
-
+
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall k: int, d0, d1: DatatypeType :: { $PrefixEqual#Dt(k, d0, d1) } $PrefixEqual#Dt(k, d0, d1) <==>
@@ -896,7 +896,7 @@ namespace Microsoft.Dafny { {
InsertChecksum(dt, fn);
}
-
+
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall k: int, d0: DatatypeType, d1: DatatypeType :: { $PrefixEqual#Dt(k,d0,d1) }
@@ -1131,7 +1131,7 @@ namespace Microsoft.Dafny { }
private bool IsOpaqueFunction(Function f) {
- return Attributes.Contains(f.Attributes, "opaque") &&
+ return Attributes.Contains(f.Attributes, "opaque") &&
!Attributes.Contains(f.Attributes, "opaque_full"); // The full version has both attributes
}
@@ -2223,7 +2223,7 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
List<Variable> localVariables = new List<Variable>();
GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables);
-
+
Bpl.StmtList stmts;
if (!wellformednessProc) {
if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoLemma)) {
@@ -3501,7 +3501,7 @@ namespace Microsoft.Dafny { builder.Add(Assert(expr.tok, inDomain, "element may not be in domain", options.AssertKv));
} else if (e.Seq.Type is MultiSetType) {
// cool
-
+
} else {
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
@@ -4182,7 +4182,7 @@ namespace Microsoft.Dafny { /// method.
/// If the method has no body, there is no reason to include this kind
/// of procedure.
- ///
+ ///
/// Note that SpecWellformedness and Implementation have procedure implementations
/// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall.
/// </summary>
@@ -4318,9 +4318,9 @@ namespace Microsoft.Dafny { var req = new List<Bpl.Requires>();
List<Bpl.IdentifierExpr> mod = new List<Bpl.IdentifierExpr>();
var ens = new List<Bpl.Ensures>();
-
+
req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null));
-
+
mod.Add((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr);
mod.Add(etran.Tick());
@@ -4435,7 +4435,7 @@ namespace Microsoft.Dafny { }
var stmts = builder.Collect(method.tok); // this token is for the implict return, which should be for the refining method,
// as this is where the error is.
-
+
var impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams, inParams, outParams,
localVariables, stmts, etran.TrAttributes(m.Attributes, null));
@@ -4499,7 +4499,7 @@ namespace Microsoft.Dafny { foreach (Expression p in f.Req) {
req.Add(Requires(p.tok, true, etran.TrExpr(p), null, null));
}
-
+
// check that postconditions hold
var ens = new List<Bpl.Ensures>();
foreach (Expression p in f.Ens) {
@@ -4517,7 +4517,7 @@ namespace Microsoft.Dafny { List<Variable> implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);
List<Variable> locals = new List<Variable>();
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
-
+
Bpl.FunctionCall funcOriginal = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
Bpl.FunctionCall funcRefining = new Bpl.FunctionCall(new Bpl.IdentifierExpr(functionCheck.Refining.tok, functionCheck.Refining.FullSanitizedName, TrType(f.ResultType)));
List<Bpl.Expr> args = new List<Bpl.Expr>();
@@ -4546,7 +4546,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(Token.NoToken, function.FullSanitizedName + "#canCall", Bpl.Type.Bool);
Bpl.Expr canCall = new Bpl.NAryExpr(Token.NoToken, new Bpl.FunctionCall(canCallFuncID), argsCanCall);
builder.Add(new AssumeCmd(function.tok, canCall));
-
+
// check that the preconditions for the call hold
foreach (Expression p in function.Req) {
Expression precond = Substitute(p, new ThisExpr(Token.NoToken), substMap);
@@ -5337,18 +5337,18 @@ namespace Microsoft.Dafny { assert line<n-1> op line<n>;
assume false;
}
- assume line<0> op line<n>;
+ assume line<0> op line<n>;
*/
var s = (CalcStmt)stmt;
Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver
AddComment(builder, stmt, "calc statement");
- if (s.Lines.Count > 0) {
+ if (s.Lines.Count > 0) {
Bpl.IfCmd ifCmd = null;
Bpl.StmtListBuilder b;
// if the dangling hint is empty, do not generate anything for the dummy step
- var stepCount = s.Hints.Last().Body.Count == 0 ? s.Steps.Count - 1 : s.Steps.Count;
+ var stepCount = s.Hints.Last().Body.Count == 0 ? s.Steps.Count - 1 : s.Steps.Count;
// check steps:
- for (int i = stepCount; 0 <= --i; ) {
+ for (int i = stepCount; 0 <= --i; ) {
b = new Bpl.StmtListBuilder();
// assume wf[line<i>]:
AddComment(b, stmt, "assume wf[lhs]");
@@ -5358,7 +5358,7 @@ namespace Microsoft.Dafny { if (s.Steps[i] is BinaryExpr && (((BinaryExpr)s.Steps[i]).ResolvedOp == BinaryExpr.ResolvedOpcode.Imp)) {
// assume line<i>:
AddComment(b, stmt, "assume lhs");
- b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i]))));
+ b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i]))));
}
// hint:
AddComment(b, stmt, "Hint" + i.ToString());
@@ -5398,7 +5398,7 @@ namespace Microsoft.Dafny { ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);
builder.Add(ifCmd);
// assume result:
- if (s.Steps.Count > 1) {
+ if (s.Steps.Count > 1) {
builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));
}
}
@@ -6009,16 +6009,21 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));
- TrStmt(s.Body, definedness, locals, etran);
-
- // check that postconditions hold
foreach (var ens in s.Ens) {
TrStmt_CheckWellformed(ens.E, definedness, locals, etran, false);
- if (!ens.IsFree) {
- bool splitHappened; // we actually don't care
- foreach (var split in TrSplitExpr(ens.E, etran, out splitHappened)) {
- if (split.IsChecked) {
- definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of forall statement"));
+ }
+
+ if (s.Body != null) {
+ TrStmt(s.Body, definedness, locals, etran);
+
+ // check that postconditions hold
+ foreach (var ens in s.Ens) {
+ if (!ens.IsFree) {
+ bool splitHappened; // we actually don't care
+ foreach (var split in TrSplitExpr(ens.E, etran, out splitHappened)) {
+ if (split.IsChecked) {
+ definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of forall statement"));
+ }
}
}
}
@@ -7145,7 +7150,7 @@ namespace Microsoft.Dafny { Contract.Requires(builder != null);
Contract.Requires(etran != null);
Contract.Requires(predef != null);
-
+
for (int i = 0; i < lhss.Count; i++) {
var lhs = lhss[i];
Contract.Assume(!(lhs is ConcreteSyntaxExpression));
@@ -7189,7 +7194,7 @@ namespace Microsoft.Dafny { string.Format("when left-hand sides {0} and {1} refer to the same location, they must be assigned the same value", j, i)));
}
}
-
+
}
}
}
@@ -7226,7 +7231,7 @@ namespace Microsoft.Dafny { int i = 0;
var lhsNameSet = new Dictionary<string, object>();
-
+
foreach (var lhs in lhss) {
Contract.Assume(!(lhs is ConcreteSyntaxExpression));
IToken tok = lhs.tok;
@@ -8541,7 +8546,7 @@ namespace Microsoft.Dafny { BoxIfNecessary(expr.tok, e0, e.E0.Type)));
case BinaryExpr.ResolvedOpcode.MapDisjoint:
return translator.FunctionCall(expr.tok, BuiltinFunction.MapDisjoint, null, e0, e1);
-
+
case BinaryExpr.ResolvedOpcode.RankLt:
return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Lt,
translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),
@@ -8648,7 +8653,7 @@ namespace Microsoft.Dafny { List<Variable> bvars = new List<Variable>();
var bv = e.BoundVars[0];
TrBoundVariables(e.BoundVars, bvars);
-
+
Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);
var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));
@@ -8657,7 +8662,7 @@ namespace Microsoft.Dafny { Bpl.Expr unboxy = !ModeledAsBoxType(bv.Type) ? translator.FunctionCall(e.tok, BuiltinFunction.Unbox, translator.TrType(bv.Type), new Bpl.IdentifierExpr(expr.tok, yVar))
: (Bpl.Expr)(new Bpl.IdentifierExpr(expr.tok, yVar));
Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, unboxy, bv.Type, this);
-
+
Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();
subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));
@@ -8667,7 +8672,7 @@ namespace Microsoft.Dafny { ebody = TrExpr(translator.Substitute(e.Term, null, subst));
Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type));
-
+
return translator.FunctionCall(e.tok, BuiltinFunction.MapGlue, null, l1, l2);
} else if (expr is StmtExpr) {
@@ -8974,9 +8979,9 @@ namespace Microsoft.Dafny { public Bpl.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {
Bpl.QKeyValue kv = null;
for ( ; attrs != null; attrs = attrs.Prev) {
- if (attrs.Name == skipThisAttribute
+ if (attrs.Name == skipThisAttribute
|| attrs.Name == "axiom") { // Dafny's axiom attribute clashes with Boogie's axiom keyword
- continue;
+ continue;
}
List<object> parms = new List<object>();
foreach (Attributes.Argument arg in attrs.Args) {
@@ -9123,7 +9128,7 @@ namespace Microsoft.Dafny { MultiSetSubset,
MultiSetDisjoint,
MultiSetFromSet,
- MultiSetFromSeq,
+ MultiSetFromSeq,
IsGoodMultiSet,
IsGoodMultiSet_Extended,
@@ -9200,7 +9205,7 @@ namespace Microsoft.Dafny { Bpl.Expr RemoveLit(Bpl.Expr expr) {
var e = GetLit(expr);
if (e == null) {
- e = expr;
+ e = expr;
}
return e;
}
@@ -9745,7 +9750,7 @@ namespace Microsoft.Dafny { splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, op, negatedTest, s.E)));
}
- return true;
+ return true;
} else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
// For an expression S;E in split position, the conclusion of S can be used as an assumption. Unfortunately,
@@ -10685,7 +10690,7 @@ namespace Microsoft.Dafny { var info = translator.letSuchThatExprInfo[e];
translator.letSuchThatExprInfo.Add(newLet, new LetSuchThatExprInfo(info, translator, substMap));
}
- newExpr = newLet;
+ newExpr = newLet;
}
} else if (expr is MatchExpr) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c15049ba..dc3f1eda 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -563,7 +563,8 @@ ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
-134 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
+135 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(7,19): error: a chain cannot have more than one != operator
@@ -2592,6 +2593,12 @@ Dafny program verifier finished with 9 verified, 6 errors Dafny program verifier finished with 0 verified, 0 errors
+-------------------- DirtyLoops.dfy --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
+
Dafny program verifier finished with 44 verified, 0 errors
Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy new file mode 100644 index 00000000..6a49e733 --- /dev/null +++ b/Test/dafny0/DirtyLoops.dfy @@ -0,0 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M(S: set<int>) {
+ forall s | s in S ensures s < 0;
+}
diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect new file mode 100644 index 00000000..5c12e1ef --- /dev/null +++ b/Test/dafny0/DirtyLoops.dfy.expect @@ -0,0 +1,4 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index e49f9823..f3297ed7 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -905,3 +905,10 @@ module LhsLvalue { method MyLemma() returns (w: int)
}
+
+// ------------------- dirty loops -------------------
+
+method DirtyM(S: set<int>) {
+ forall s | s in S ensures s < 0;
+ assert s < 0; // error: s is unresolved
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index eb9b244b..2c0664d9 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -132,4 +132,5 @@ ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
-134 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\ResolutionErrors.dfy
+ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
+135 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index fe3a29e1..1a371ba3 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -50,5 +50,12 @@ for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do ( %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy
)
+for %%f in (DirtyLoops.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
+ %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy
+)
+
%DAFNY_EXE% %* Compilation.dfy
%DAFNY_EXE% %* CompilationErrors.dfy
|