From 05bbbcc402870c5064df987d7f14c5b83cece22c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 27 Jun 2014 18:56:15 -0700 Subject: Added tuples and tuple types. Syntax is the expected one, namely parentheses around a comma-delimited list of expressions or types. Unit and the unit type are denoted (). --- Source/Dafny/Cloner.cs | 3 + Source/Dafny/Compiler.cs | 11 +++- Source/Dafny/Dafny.atg | 83 ++++++++++++++++++------- Source/Dafny/DafnyAst.cs | 98 ++++++++++++++++++++++++++--- Source/Dafny/Parser.cs | 107 ++++++++++++++++++++++++-------- Source/Dafny/Printer.cs | 13 +++- Source/Dafny/Resolver.cs | 4 ++ Test/dafny0/ResolutionErrors.dfy | 31 +++++++++ Test/dafny0/ResolutionErrors.dfy.expect | 8 ++- Test/dafny0/Tuples.dfy | 34 ++++++++++ Test/dafny0/Tuples.dfy.expect | 8 +++ 11 files changed, 342 insertions(+), 58 deletions(-) create mode 100644 Test/dafny0/Tuples.dfy create mode 100644 Test/dafny0/Tuples.dfy.expect diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 537dae1d..5b8f8cc5 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -30,6 +30,9 @@ namespace Microsoft.Dafny if (d is ArbitraryTypeDecl) { var dd = (ArbitraryTypeDecl)d; return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes)); + } else if (d is TupleTypeDecl) { + var dd = (TupleTypeDecl)d; + return new TupleTypeDecl(dd.Dims, dd.Module); } else if (d is IndDatatypeDecl) { var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 56c6edc2..fcf8a2ca 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -107,6 +107,10 @@ namespace Microsoft.Dafny { indent += IndentAmount; } foreach (TopLevelDecl d in m.TopLevelDecls) { + bool compileIt = true; + if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) { + continue; + } wr.WriteLine(); if (d is ArbitraryTypeDecl) { var at = (ArbitraryTypeDecl)d; @@ -411,7 +415,12 @@ namespace Microsoft.Dafny { if (dt is IndDatatypeDecl) { Indent(ind); wr.WriteLine("public override string ToString() {"); - string nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName; + string nm; + if (dt is TupleTypeDecl) { + nm = ""; + } else { + nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName; + } Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm); if (ctor.Formals.Count != 0) { Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";"); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2ab70c4f..5c1148c6 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -739,8 +739,9 @@ Type TypeAndToken . TypeAndToken -= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ - List/*!*/ gt; += (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); + tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ + List gt; .) ( "bool" (. tok = t; .) | "nat" (. tok = t; ty = new NatType(); .) @@ -774,6 +775,20 @@ TypeAndToken ty = new MapType(gt[0], gt[1]); } .) + | "(" (. tok = t; gt = new List(); .) + [ Type (. gt.Add(ty); .) + { "," Type (. gt.Add(ty); .) + } + ] + ")" (. if (gt.Count == 1) { + // just return the type 'ty' + } else { + // make sure the nullary tuple type exists + var dims = gt.Count; + var tmp = theBuiltIns.TupleType(tok, dims, true); + ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List()); + } + .) | ReferenceType ) . @@ -1876,25 +1891,51 @@ ConstAtomExpression | "|" (. x = t; .) Expression (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .) "|" - | "(" (. x = t; .) - Expression (. e = new ParensExpression(x, e); .) - ")" - | "real" (. x = t; .) - "(" (. IToken openParen = t; .) - Expression - ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); - e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); - .) - | "int" (. x = t; .) - "(" (. IToken openParen = t; .) - Expression - ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); - e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); - .) + | ParensExpression + | "real" (. x = t; .) + "(" (. IToken openParen = t; .) + Expression + ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); + e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); + .) + | "int" (. x = t; .) + "(" (. IToken openParen = t; .) + Expression + ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); + e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); + .) + ) + . +ParensExpression += (. IToken x; + List args = null; + .) + "(" (. x = t; e = null; .) + ( ")" (. // unit + // make sure the nullary tuple type exists + var tmp = theBuiltIns.TupleType(x, 0, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List()); + .) + | Expression + { "," (. if (args == null) { + args = new List(); + args.Add(e); // add the first argument, which was parsed above + } + .) + Expression (. args.Add(e); .) + } + ")" (. if (args == null) { + e = new ParensExpression(x, e); + } else { + // make sure the corresponding tuple type exists + var tmp = theBuiltIns.TupleType(x, args.Count, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args); + } + .) ) . DisplayExpr diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ad98a0c0..55dc973f 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -88,15 +88,17 @@ namespace Microsoft.Dafny { { public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true); Dictionary arrayTypeDecls = new Dictionary(); + Dictionary tupleTypeDecls = new Dictionary(); public readonly ClassDecl ObjectDecl; public readonly ClassDecl RealClass; //public readonly Function RealToInt; //public readonly Function IntToReal; public BuiltIns() { // create class 'object' - ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), null); + ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), DontCompile()); SystemModule.TopLevelDecls.Add(ObjectDecl); // add one-dimensional arrays, since they may arise during type checking + // Arrays of other dimensions may be added during parsing as the parser detects the need for these UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true); // add real number functions Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List(), Token.NoToken, @@ -108,12 +110,19 @@ namespace Microsoft.Dafny { new List(), new List(), new Specification(new List(), null), null, null, Token.NoToken); RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List(), - new List() { RealToInt, IntToReal }, null); + new List() { RealToInt, IntToReal }, DontCompile()); RealToInt.EnclosingClass = RealClass; IntToReal.EnclosingClass = RealClass; RealToInt.IsBuiltin = true; IntToReal.IsBuiltin = true; SystemModule.TopLevelDecls.Add(RealClass); + // Note, in addition to these types, the _System module contains tuple types. These tuple types are added to SystemModule + // by the parser as the parser detects the need for these. + } + + private Attributes DontCompile() { + var flse = new Attributes.Argument(Token.NoToken, Expression.CreateBoolLiteral(Token.NoToken, false)); + return new Attributes("compile", new List() { flse }, null); } public UserDefinedType ArrayType(int dims, Type arg) { @@ -129,7 +138,7 @@ namespace Microsoft.Dafny { typeArgs.Add(arg); UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null); if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) { - ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule); + ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile()); for (int d = 0; d < dims; d++) { string name = dims == 1 ? "Length" : "Length" + d; string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")"; @@ -152,6 +161,30 @@ namespace Microsoft.Dafny { return "array" + dims; } } + + public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType) { + Contract.Requires(tok != null); + Contract.Requires(0 <= dims); + Contract.Ensures(Contract.Result() != null); + + TupleTypeDecl tt; + if (!tupleTypeDecls.TryGetValue(dims, out tt)) { + Contract.Assume(allowCreationOfNewType); // the parser should ensure that all needed tuple types exist by the time of resolution + tt = new TupleTypeDecl(dims, SystemModule); + tupleTypeDecls.Add(dims, tt); + SystemModule.TopLevelDecls.Add(tt); + } + return tt; + } + public static string TupleTypeName(int dims) { + Contract.Requires(0 <= dims); + return "_tuple#" + dims; + } + public static bool IsTupleTypeName(string s) { + Contract.Requires(s != null); + return s.StartsWith("_tuple#"); + } + public const string TupleTypeCtorName = "_#Make"; // the printer wants this name to be uniquely recognizable } public class Attributes { @@ -714,6 +747,9 @@ namespace Microsoft.Dafny { [Pure] public override string TypeName(ModuleDefinition context) { Contract.Ensures(Contract.Result() != null); + if (BuiltIns.IsTupleTypeName(Name)) { + return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")"; + } string s = ""; foreach (var t in Path) { if (context != null && t == context.tok) { @@ -1355,10 +1391,10 @@ namespace Microsoft.Dafny { public class ArrayClassDecl : ClassDecl { public readonly int Dims; - public ArrayClassDecl(int dims, ModuleDefinition module) + public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs) : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module, new List(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}), - new List(), null) + new List(), attrs) { Contract.Requires(1 <= dims); Contract.Requires(module != null); @@ -1367,7 +1403,8 @@ namespace Microsoft.Dafny { } } - public abstract class DatatypeDecl : TopLevelDecl { + public abstract class DatatypeDecl : TopLevelDecl + { public readonly List Ctors; [ContractInvariantMethod] void ObjectInvariant() { @@ -1413,6 +1450,52 @@ namespace Microsoft.Dafny { } } + public class TupleTypeDecl : IndDatatypeDecl + { + public readonly int Dims; + /// + /// Construct a resolved built-in tuple type with "dim" arguments. "systemModule" is expected to be the _System module. + /// + public TupleTypeDecl(int dims, ModuleDefinition systemModule) + : this(systemModule, CreateTypeParameters(dims)) { + Contract.Requires(0 <= dims); + Contract.Requires(systemModule != null); + } + private TupleTypeDecl(ModuleDefinition systemModule, List typeArgs) + : base(Token.NoToken, BuiltIns.TupleTypeName(typeArgs.Count), systemModule, typeArgs, CreateConstructors(typeArgs), null) { + Contract.Requires(systemModule != null); + Contract.Requires(typeArgs != null); + Dims = typeArgs.Count; + foreach (var ctor in Ctors) { + ctor.EnclosingDatatype = this; // resolve here + DefaultCtor = ctor; + TypeParametersUsedInConstructionByDefaultCtor = new bool[typeArgs.Count]; + for (int i = 0; i < typeArgs.Count; i++) { + TypeParametersUsedInConstructionByDefaultCtor[i] = true; + } + } + } + private static List CreateTypeParameters(int dims) { + Contract.Requires(0 <= dims); + var ts = new List(); + for (int i = 0; i < dims; i++) { + ts.Add(new TypeParameter(Token.NoToken, "T" + i)); + } + return ts; + } + private static List CreateConstructors(List typeArgs) { + Contract.Requires(typeArgs != null); + var formals = new List(); + for (int i = 0; i < typeArgs.Count; i++) { + var tp = typeArgs[i]; + var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp.Name, tp), true, false); + formals.Add(f); + } + var ctor = new DatatypeCtor(Token.NoToken, BuiltIns.TupleTypeCtorName, formals, null); + return new List() { ctor }; + } + } + public class CoDatatypeDecl : DatatypeDecl { public CoDatatypeDecl SscRepr; // filled in during resolution @@ -1918,7 +2001,7 @@ namespace Microsoft.Dafny { } return UniqueName; } - static char[] specialChars = new char[] { '\'', '_', '?', '\\' }; + static char[] specialChars = new char[] { '\'', '_', '?', '\\', '#' }; public static string CompilerizeName(string nm) { if ('0' <= nm[0] && nm[0] <= '9') { // the identifier is one that consists of just digits @@ -1942,6 +2025,7 @@ namespace Microsoft.Dafny { case '_': name += "__"; break; case '?': name += "_q"; break; case '\\': name += "_b"; break; + case '#': name += "_h"; break; default: Contract.Assume(false); // unexpected character break; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 969774db..a7f058db 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1115,8 +1115,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } void TypeAndToken(out IToken/*!*/ tok, out Type/*!*/ ty) { - Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ - List/*!*/ gt; + Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); + tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ + List gt; switch (la.kind) { case 52: { @@ -1195,6 +1196,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break; } + case 11: { + Get(); + tok = t; gt = new List(); + if (StartOf(10)) { + Type(out ty); + gt.Add(ty); + while (la.kind == 31) { + Get(); + Type(out ty); + gt.Add(ty); + } + } + Expect(12); + if (gt.Count == 1) { + // just return the type 'ty' + } else { + // make sure the nullary tuple type exists + var dims = gt.Count; + var tmp = theBuiltIns.TupleType(tok, dims, true); + ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List()); + } + + break; + } case 1: case 5: case 60: { ReferenceType(out tok, out ty); break; @@ -3352,11 +3377,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } case 11: { - Get(); - x = t; - Expression(out e, true); - e = new ParensExpression(x, e); - Expect(12); + ParensExpression(out e); break; } case 55: { @@ -3427,6 +3448,41 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } + void ParensExpression(out Expression e) { + IToken x; + List args = null; + + Expect(11); + x = t; e = null; + if (la.kind == 12) { + Get(); + var tmp = theBuiltIns.TupleType(x, 0, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List()); + + } else if (StartOf(16)) { + Expression(out e, true); + while (la.kind == 31) { + Get(); + if (args == null) { + args = new List(); + args.Add(e); // add the first argument, which was parsed above + } + + Expression(out e, true); + args.Add(e); + } + Expect(12); + if (args == null) { + e = new ParensExpression(x, e); + } else { + // make sure the corresponding tuple type exists + var tmp = theBuiltIns.TupleType(x, args.Count, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args); + } + + } else SynErr(223); + } + void MapLiteralExpressions(out List elements) { Expression/*!*/ d, r; elements = new List(); @@ -3448,7 +3504,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 125) { Get(); - } else SynErr(223); + } else SynErr(224); } void MatchExpression(out Expression e, bool allowSemi) { @@ -3471,7 +3527,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(10); } else if (StartOf(31)) { if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } - } else SynErr(224); + } else SynErr(225); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -3489,7 +3545,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 122 || la.kind == 123) { Exists(); x = t; - } else SynErr(225); + } else SynErr(226); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi); @@ -3537,7 +3593,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 88) { CalcStmt(out s); - } else SynErr(226); + } else SynErr(227); } void LetExpr(out Expression e, bool allowSemi) { @@ -3577,7 +3633,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(227); + } else SynErr(228); Expression(out e, false); letRHSs.Add(e); while (la.kind == 31) { @@ -3628,7 +3684,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); pat = new CasePattern(bv.tok, bv); - } else SynErr(228); + } else SynErr(229); } void CaseExpression(out MatchCaseExpr c, bool allowSemi) { @@ -3661,7 +3717,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 121) { Get(); - } else SynErr(229); + } else SynErr(230); } void Exists() { @@ -3669,7 +3725,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 123) { Get(); - } else SynErr(230); + } else SynErr(231); } void AttributeBody(ref Attributes attrs) { @@ -3714,8 +3770,8 @@ List/*!*/ 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,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}, {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, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x, x,T,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, x,x,x,x, x,x,x,x, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x, x,T,x,x, x,x,x,T, 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, x,x,x,x, x,x,x,x, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x,x, x,x,x,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, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, 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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,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}, @@ -3986,14 +4042,15 @@ public class Errors { case 220: s = "invalid MultiSetExpr"; break; case 221: s = "invalid ConstAtomExpression"; break; case 222: s = "invalid Nat"; break; - case 223: s = "invalid QSep"; break; - case 224: s = "invalid MatchExpression"; break; - case 225: s = "invalid QuantifierGuts"; break; - case 226: s = "invalid StmtInExpr"; break; - case 227: s = "invalid LetExpr"; break; - case 228: s = "invalid CasePattern"; break; - case 229: s = "invalid Forall"; break; - case 230: s = "invalid Exists"; break; + case 223: s = "invalid ParensExpression"; break; + case 224: s = "invalid QSep"; break; + case 225: s = "invalid MatchExpression"; break; + case 226: s = "invalid QuantifierGuts"; break; + case 227: s = "invalid StmtInExpr"; break; + case 228: s = "invalid LetExpr"; break; + case 229: s = "invalid CasePattern"; break; + case 230: s = "invalid Forall"; break; + case 231: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 0a970498..5be5614d 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1191,9 +1191,16 @@ namespace Microsoft.Dafny { wr.Write(((IdentifierExpr)expr).Name); } else if (expr is DatatypeValue) { - DatatypeValue dtv = (DatatypeValue)expr; - wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName); - if (dtv.Arguments.Count != 0) { + var dtv = (DatatypeValue)expr; + bool printParens; + if (dtv.MemberName == BuiltIns.TupleTypeCtorName) { + // we're looking at a tuple, whose printed constructor name is essentially the empty string + printParens = true; + } else { + wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName); + printParens = dtv.Arguments.Count != 0; + } + if (printParens) { wr.Write("("); PrintExpressionList(dtv.Arguments, false); wr.Write(")"); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8de010fb..73925aef 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -197,6 +197,7 @@ namespace Microsoft.Dafny rewriters.Add(opaqueRewriter); systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); + prog.CompileModules.Add(prog.BuiltIns.SystemModule); foreach (var decl in sortedDecls) { if (decl is LiteralModuleDecl) { // The declaration is a literal module, so it has members and such that we need @@ -1019,6 +1020,9 @@ namespace Microsoft.Dafny if (d is ArbitraryTypeDecl) { var dd = (ArbitraryTypeDecl)d; return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null); + } else if (d is TupleTypeDecl) { + var dd = (TupleTypeDecl)d; + return new TupleTypeDecl(dd.Dims, dd.Module); } else if (d is IndDatatypeDecl) { var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f3297ed7..35c17112 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -912,3 +912,34 @@ method DirtyM(S: set) { forall s | s in S ensures s < 0; assert s < 0; // error: s is unresolved } + +// ------------------- tuples ------------------- + +method TupleResolution(x: int, y: int, r: real) +{ + var unit: () := (); + var expr: int := (x); + var pair: (int,int) := (x, x); + var triple: (int,int,int) := (y, x, x); + var badTriple: (int,real,int) := (y, x, r); // error: parameters 1 and 2 have the wrong types + var quadruple: (int,real,int,real) := (y, r, x); // error: trying to use a triple as a quadruple + + assert unit == (); + assert pair.0 == pair.1; + assert triple.2 == x; + + assert triple.2; // error: 2 has type int, not the expected bool + assert triple.3 == pair.x; // error(s): 3 and x are not destructors + + var k0 := (5, (true, 2, 3.14)); + var k1 := (((false, 10, 2.7)), 100, 120); + if k0.1 == k1.0 { + assert false; + } else if k0.1.1 < k1.0.1 { + assert k1.2 == 120; + } + + // int and (int) are the same type (i.e., there are no 1-tuples) + var pp: (int) := x; + var qq: int := pp; +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 2c0664d9..22f3274e 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -133,4 +133,10 @@ ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only i ResolutionErrors.dfy(546,18): Error: unresolved identifier: w ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses ResolutionErrors.dfy(913,9): Error: unresolved identifier: s -135 resolution/type errors detected in ResolutionErrors.dfy +ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int)) +ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real)) +ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int +ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3 +ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2 +ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int)) +141 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/Tuples.dfy b/Test/dafny0/Tuples.dfy new file mode 100644 index 00000000..81d054dd --- /dev/null +++ b/Test/dafny0/Tuples.dfy @@ -0,0 +1,34 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method M(x: int) +{ + var unit := (); + var expr := (x); + var pair := (x, x); + var triple := (x, x, x); +} + +method N(x: int, y: int) +{ + var unit: () := (); + var expr: int := (x); + var pair: (int,int) := (x, x); + var triple: (int,int,int) := (y, x, x); + + assert unit == (); + assert pair.0 == pair.1; + assert triple.2 == x; + assert triple.0 == triple.1; // error: they may be different + + var k := (24, 100 / y); // error: possible division by zero + assert 2 <= k.0 < 29; + + var k0 := (5, (true, 2, 3.14)); + var k1 := (((false, 10, 2.7)), 100, 120); + if k0.1 == k1.0 { + assert false; + } else if k0.1.1 < k1.0.1 { + assert k1.2 == 120; + } +} diff --git a/Test/dafny0/Tuples.dfy.expect b/Test/dafny0/Tuples.dfy.expect new file mode 100644 index 00000000..13c706d3 --- /dev/null +++ b/Test/dafny0/Tuples.dfy.expect @@ -0,0 +1,8 @@ +Tuples.dfy(22,19): Error: assertion violation +Execution trace: + (0,0): anon0 +Tuples.dfy(24,21): Error: possible division by zero +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 3 verified, 2 errors -- cgit v1.2.3 From b4e20b3397098b237b5b17b4b6a71d02a900a88d Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 28 Jun 2014 17:59:44 +0200 Subject: Minor change due to change in Boogie --- Source/DafnyDriver/DafnyDriver.csproj | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 631b0194..cf664364 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -20,7 +20,7 @@ 3.5 false - Client + publish\ true Disk -- cgit v1.2.3 From 62e76ea8117eb87571bf49588464540c8fa02357 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 28 Jun 2014 21:23:58 +0200 Subject: Minor change due to change in Boogie --- Source/DafnyExtension/DafnyDriver.cs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 36b07d60..ba01c04a 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -249,7 +249,8 @@ namespace DafnyLanguage resolver.ReInitializeVerificationErrors(requestId, boogieProgram.TopLevelDeclarations); - PipelineOutcome oc = BoogiePipeline(boogieProgram, requestId, er); + // TODO(wuestholz): Maybe we should use a fixed program ID to limit the memory overhead due to the program cache in Boogie. + PipelineOutcome oc = BoogiePipeline(boogieProgram, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? uniqueIdPrefix : null, requestId, er); switch (oc) { case PipelineOutcome.Done: case PipelineOutcome.VerificationCompleted: @@ -267,7 +268,7 @@ namespace DafnyLanguage /// else. Hence, any resolution errors and type checking errors are due to errors in /// the translation. /// - static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string requestId, ErrorReporterDelegate er) + static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string programId, string requestId, ErrorReporterDelegate er) { Contract.Requires(program != null); @@ -277,7 +278,7 @@ namespace DafnyLanguage ExecutionEngine.CollectModSets(program); ExecutionEngine.CoalesceBlocks(program); ExecutionEngine.Inline(program); - return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId); + return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), programId, er, requestId); } return oc; } -- cgit v1.2.3 From c5b2aec063fc1f3d5e61ff1b14983c5e4ba7c2ea Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 1 Jul 2014 00:55:31 +0200 Subject: Added support for verifying Dafny program snapshots from the command-line. --- Source/Dafny/Translator.cs | 3 ++- Source/DafnyDriver/DafnyDriver.cs | 20 +++++++++++++++++--- Test/dafny0/snapshots/Snapshots0.v0.dfy | 8 ++++++++ Test/dafny0/snapshots/Snapshots0.v1.dfy | 8 ++++++++ Test/dafny0/snapshots/lit.local.cfg | 5 +++++ Test/dafny0/snapshots/runtest.snapshot | 2 ++ Test/dafny0/snapshots/runtest.snapshot.expect | 7 +++++++ 7 files changed, 49 insertions(+), 4 deletions(-) create mode 100644 Test/dafny0/snapshots/Snapshots0.v0.dfy create mode 100644 Test/dafny0/snapshots/Snapshots0.v1.dfy create mode 100644 Test/dafny0/snapshots/lit.local.cfg create mode 100644 Test/dafny0/snapshots/runtest.snapshot create mode 100644 Test/dafny0/snapshots/runtest.snapshot.expect diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e64c0da6..39b1ea95 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -17,6 +17,7 @@ namespace Microsoft.Dafny { public class Translator { [NotDelayed] public Translator() { + InsertChecksums = 0 < CommandLineOptions.Clo.VerifySnapshots; Bpl.Program boogieProgram = ReadPrelude(); if (boogieProgram != null) { sink = boogieProgram; @@ -2507,7 +2508,7 @@ namespace Microsoft.Dafny { public void InsertUniqueIdForImplementation(Bpl.Declaration decl) { var impl = decl as Bpl.Implementation; - var prefix = UniqueIdPrefix ?? decl.tok.filename; + var prefix = UniqueIdPrefix ?? System.Text.RegularExpressions.Regex.Replace(decl.tok.filename, @".v\d+.dfy", ".dfy"); if (impl != null && !string.IsNullOrEmpty(prefix)) { decl.AddAttribute("id", prefix + ":" + impl.Name + ":0"); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 8f5b5300..01ee269e 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -99,7 +99,7 @@ namespace Microsoft.Dafny } - static ExitValue ProcessFiles(List/*!*/ fileNames) + static ExitValue ProcessFiles(List/*!*/ fileNames, bool lookForSnapshots = true) { Contract.Requires(cce.NonNullElements(fileNames)); @@ -110,7 +110,21 @@ namespace Microsoft.Dafny { Console.WriteLine(); Console.WriteLine("-------------------- {0} --------------------", f); - var ev = ProcessFiles(new List { f }); + var ev = ProcessFiles(new List { f }, lookForSnapshots); + if (exitValue != ev && ev != ExitValue.VERIFIED) + { + exitValue = ev; + } + } + return exitValue; + } + + if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots) + { + var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames); + foreach (var s in snapshotsByVersion) + { + var ev = ProcessFiles(new List(s), false); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -213,7 +227,7 @@ namespace Microsoft.Dafny ExecutionEngine.CollectModSets(program); ExecutionEngine.CoalesceBlocks(program); ExecutionEngine.Inline(program); - return ExecutionEngine.InferAndVerify(program, stats); + return ExecutionEngine.InferAndVerify(program, stats, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? "main_program_id" : null); default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy new file mode 100644 index 00000000..73db9f9c --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.v0.dfy @@ -0,0 +1,8 @@ +method foo() +{ + bar(); + assert false; +} + +method bar() + ensures false; diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy new file mode 100644 index 00000000..28f9f283 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy @@ -0,0 +1,8 @@ +method foo() +{ + bar(); + assert false; +} + +method bar() + ensures true; diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg new file mode 100644 index 00000000..07cb869f --- /dev/null +++ b/Test/dafny0/snapshots/lit.local.cfg @@ -0,0 +1,5 @@ +# This test is unusual in that we don't use the .bpl files +# directly on the command line. So instead we'll invoke +# files in this directory with extension '.snapshot'. There +# will only be one for now +config.suffixes = ['.snapshot'] diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot new file mode 100644 index 00000000..6d2f880f --- /dev/null +++ b/Test/dafny0/snapshots/runtest.snapshot @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect new file mode 100644 index 00000000..7906e7a5 --- /dev/null +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -0,0 +1,7 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Snapshots0.v1.dfy(4,10): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 2 verified, 1 error -- cgit v1.2.3 From 39a8abe0d2d6e4bda54fb3a481b049c19fe1dba9 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 1 Jul 2014 17:52:52 +0200 Subject: Removed the old test infrastructure. --- Test/Makefile | 17 - Test/VSComp2010/Answer | 20 - Test/VSComp2010/runtest.bat | 15 - Test/VSI-Benchmarks/Answer | 32 - Test/VSI-Benchmarks/runtest.bat | 13 - Test/alltests.txt | 10 - Test/cloudmake/Answer | 12 - Test/cloudmake/runtest.bat | 7 - Test/dafny0/Answer | 2616 ------------------------------------- Test/dafny0/runtest.bat | 61 - Test/dafny1/Answer | 124 -- Test/dafny1/runtest.bat | 26 - Test/dafny2/Answer | 60 - Test/dafny2/runtest.bat | 27 - Test/dafny3/Answer | 64 - Test/dafny3/runtest.bat | 19 - Test/dafny4/Answer | 43 - Test/dafny4/runtest.bat | 7 - Test/runtest.bat | 39 - Test/runtestall.bat | 24 - Test/vacid0/Answer | 12 - Test/vacid0/AnswerRuntimeChecking | 0 Test/vacid0/runtest.bat | 13 - Test/vstte2012/Answer | 24 - Test/vstte2012/runtest.bat | 23 - 25 files changed, 3308 deletions(-) delete mode 100644 Test/Makefile delete mode 100644 Test/VSComp2010/Answer delete mode 100644 Test/VSComp2010/runtest.bat delete mode 100644 Test/VSI-Benchmarks/Answer delete mode 100644 Test/VSI-Benchmarks/runtest.bat delete mode 100644 Test/alltests.txt delete mode 100644 Test/cloudmake/Answer delete mode 100644 Test/cloudmake/runtest.bat delete mode 100644 Test/dafny0/Answer delete mode 100644 Test/dafny0/runtest.bat delete mode 100644 Test/dafny1/Answer delete mode 100644 Test/dafny1/runtest.bat delete mode 100644 Test/dafny2/Answer delete mode 100644 Test/dafny2/runtest.bat delete mode 100644 Test/dafny3/Answer delete mode 100644 Test/dafny3/runtest.bat delete mode 100644 Test/dafny4/Answer delete mode 100644 Test/dafny4/runtest.bat delete mode 100644 Test/runtest.bat delete mode 100644 Test/runtestall.bat delete mode 100644 Test/vacid0/Answer delete mode 100644 Test/vacid0/AnswerRuntimeChecking delete mode 100644 Test/vacid0/runtest.bat delete mode 100644 Test/vstte2012/Answer delete mode 100644 Test/vstte2012/runtest.bat diff --git a/Test/Makefile b/Test/Makefile deleted file mode 100644 index 6e02aed0..00000000 --- a/Test/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -TESTS_FILE = alltests.txt -LONG = $(shell awk '{ if (tolower($$2) ~ /^long$$/) print $$1 }' $(TESTS_FILE)) -NORMAL = $(shell awk '{ if (tolower($$2) ~ /^use$$/) print $$1 }' $(TESTS_FILE)) -TESTS = $(NORMAL) - -all: dafny - -dafny: $(addprefix rundfy-, $(TESTS)) - -rundfy-%: - @cmd /c "runtest.bat $* $(FLAGS)" || : - -long: - $(MAKE) TESTS="$(NORMAL) $(LONG)" all - -show: - @echo $(TESTS) diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer deleted file mode 100644 index ff491aa5..00000000 --- a/Test/VSComp2010/Answer +++ /dev/null @@ -1,20 +0,0 @@ - --------------------- Problem1-SumMax.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Problem2-Invert.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- Problem3-FindZero.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- Problem4-Queens.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- Problem5-DoubleEndedQueue.dfy -------------------- - -Dafny program verifier finished with 21 verified, 0 errors diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat deleted file mode 100644 index 2cfcdafb..00000000 --- a/Test/VSComp2010/runtest.bat +++ /dev/null @@ -1,15 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy Problem5-DoubleEndedQueue.dfy - -rem for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy -rem Problem3-FindZero.dfy Problem4-Queens.dfy -rem Problem5-DoubleEndedQueue.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer deleted file mode 100644 index 2a4587f4..00000000 --- a/Test/VSI-Benchmarks/Answer +++ /dev/null @@ -1,32 +0,0 @@ - --------------------- b1.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- b2.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- b3.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- b4.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- b5.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- b6.dfy -------------------- - -Dafny program verifier finished with 21 verified, 0 errors - --------------------- b7.dfy -------------------- - -Dafny program verifier finished with 23 verified, 0 errors - --------------------- b8.dfy -------------------- - -Dafny program verifier finished with 42 verified, 0 errors diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat deleted file mode 100644 index f950cf2a..00000000 --- a/Test/VSI-Benchmarks/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy - -rem for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/alltests.txt b/Test/alltests.txt deleted file mode 100644 index c586a561..00000000 --- a/Test/alltests.txt +++ /dev/null @@ -1,10 +0,0 @@ -dafny0 Use Dafny functionality tests -dafny1 Use Various Dafny examples -dafny2 Use More Dafny examples -dafny3 Use And more Dafny examples -dafny4 Use More, more, more! -cloudmake Use CloudMake formalization and proofs -VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges -vacid0 Use Dafny attempts to VACID Edition 0 benchmarks -vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition -VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer deleted file mode 100644 index 3758853e..00000000 --- a/Test/cloudmake/Answer +++ /dev/null @@ -1,12 +0,0 @@ - --------------------- CloudMake-ParallelBuilds.dfy -------------------- - -Dafny program verifier finished with 244 verified, 0 errors - --------------------- CloudMake-CachedBuilds.dfy -------------------- - -Dafny program verifier finished with 104 verified, 0 errors - --------------------- CloudMake-ConsistentBuilds.dfy -------------------- - -Dafny program verifier finished with 59 verified, 0 errors diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat deleted file mode 100644 index 8fc7ccbb..00000000 --- a/Test/cloudmake/runtest.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer deleted file mode 100644 index dc3f1eda..00000000 --- a/Test/dafny0/Answer +++ /dev/null @@ -1,2616 +0,0 @@ - --------------------- Simple.dfy -------------------- -// Simple.dfy - -class MyClass { - var x: int; - - method M(s: bool, lotsaObjects: set) - returns (t: object, u: set, v: seq>) - requires s; - modifies this, lotsaObjects; - ensures t == t; - ensures old(null) != this; - { - x := 12; - while x < 100 - invariant x <= 100; - { - x := x + 17; - if x % 20 == 3 { - x := this.x + 1; - } else { - this.x := x + 0; - } - t, u, v := M(true, lotsaObjects); - var to: MyClass; - to, u, v := this.M(true, lotsaObjects); - to, u, v := to.M(true, lotsaObjects); - assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10]; - } - } - - function F(x: int, y: int, h: WildData, k: WildData): WildData - { - if x < 0 then - h - else if x == 0 then - if if h == k then true else false then - h - else if y == 0 then - k - else - h - else - k - } -} - -datatype List = Nil | Cons(T, List) - -datatype WildData = Something | JustAboutAnything(bool, myName: set, int, WildData) | More(List) - -class C { - var w: WildData; - var list: List; -} - -lemma M(x: int) - ensures x < 8; -{ -} - -colemma M'(x': int) - ensures true; -{ -} - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- TypeTests.dfy -------------------- -TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D) -TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C) -TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int) -TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int) -TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool) -TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C) -TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int) -TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -TypeTests.dfy(56,6): Error: Duplicate local-variable name: z -TypeTests.dfy(58,6): Error: Duplicate local-variable name: x -TypeTests.dfy(61,8): Error: Duplicate local-variable name: x -TypeTests.dfy(64,6): Error: Duplicate local-variable name: y -TypeTests.dfy(70,11): Error: unresolved identifier: x -TypeTests.dfy(72,28): Error: unresolved identifier: z -TypeTests.dfy(73,29): Error: unresolved identifier: w1 -TypeTests.dfy(73,47): Error: unresolved identifier: w0 -TypeTests.dfy(76,28): Error: unresolved identifier: e -TypeTests.dfy(91,17): Error: member F in type C does not refer to a method -TypeTests.dfy(92,17): Error: a method called as an initialization method must not have any result arguments -TypeTests.dfy(101,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(103,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(105,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type -TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts -TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed -33 resolution/type errors detected in TypeTests.dfy - --------------------- NatTypes.dfy -------------------- -NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 -NatTypes.dfy(34,10): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - NatTypes.dfy(22,3): anon10_LoopHead - (0,0): anon10_LoopBody - NatTypes.dfy(22,3): anon11_Else - (0,0): anon12_Then -NatTypes.dfy(41,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -NatTypes.dfy(43,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -NatTypes.dfy(60,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -NatTypes.dfy(74,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -NatTypes.dfy(107,45): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - -Dafny program verifier finished with 15 verified, 9 errors - --------------------- RealTypes.dfy -------------------- -RealTypes.dfy(8,23): Error: assertion violation -Execution trace: - (0,0): anon0 -RealTypes.dfy(14,12): Error: possible division by zero -Execution trace: - (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else - (0,0): anon2 -RealTypes.dfy(14,20): Error: assertion violation -Execution trace: - (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else - (0,0): anon2 -RealTypes.dfy(22,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 6 verified, 4 errors - --------------------- Definedness.dfy -------------------- -Definedness.dfy(11,7): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Definedness.dfy(18,16): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(27,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(28,21): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Definedness.dfy(29,17): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(36,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(45,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(53,18): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(54,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(53,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(60,18): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(61,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(60,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(68,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(67,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(88,7): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(89,5): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 -Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Definedness.dfy(89,10): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(90,10): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 -Definedness.dfy(95,14): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(95,23): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(96,15): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(101,12): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(108,15): Error: possible division by zero -Execution trace: - Definedness.dfy(108,5): anon7_LoopHead - (0,0): anon7_LoopBody - Definedness.dfy(108,5): anon8_Else -Definedness.dfy(117,23): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(116,5): anon12_LoopHead - (0,0): anon12_LoopBody - (0,0): anon13_Then -Definedness.dfy(123,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(116,5): anon12_LoopHead - (0,0): anon12_LoopBody - Definedness.dfy(116,5): anon13_Else - (0,0): anon14_Then - Definedness.dfy(122,5): anon15_LoopHead - (0,0): anon15_LoopBody - (0,0): anon16_Then -Definedness.dfy(133,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(132,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(133,22): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(134,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(132,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(143,15): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(143,5): anon8_LoopHead - (0,0): anon8_LoopBody - Definedness.dfy(143,5): anon9_Else -Definedness.dfy(162,15): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(156,5): anon16_LoopHead - (0,0): anon16_LoopBody - Definedness.dfy(156,5): anon17_Else - (0,0): anon18_Then - (0,0): anon5 - (0,0): anon19_Then - Definedness.dfy(162,5): anon20_LoopHead - (0,0): anon20_LoopBody - Definedness.dfy(162,5): anon21_Else -Definedness.dfy(175,28): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(181,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(173,5): anon18_LoopHead - (0,0): anon18_LoopBody - Definedness.dfy(173,5): anon19_Else - (0,0): anon20_Then - Definedness.dfy(180,5): anon21_LoopHead - (0,0): anon21_LoopBody - (0,0): anon22_Then - (0,0): anon23_Then - (0,0): anon11 -Definedness.dfy(196,19): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(194,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(196,23): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(196,28): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(194,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(217,46): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -Definedness.dfy(224,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(240,24): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon2 - (0,0): anon8_Else - -Dafny program verifier finished with 21 verified, 37 errors - --------------------- FunctionSpecifications.dfy -------------------- -FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else -FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon11_Else - (0,0): anon14_Else - (0,0): anon15_Then -FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon3 -FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -FunctionSpecifications.dfy(108,23): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(111,23): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(126,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -FunctionSpecifications.dfy(130,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(153,15): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(172,15): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Else -FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(160,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(188,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 19 verified, 17 errors - --------------------- ResolutionErrors.dfy -------------------- -ResolutionErrors.dfy(499,7): Error: RHS (of type List) not assignable to LHS (of type List) -ResolutionErrors.dfy(504,7): Error: RHS (of type List) not assignable to LHS (of type List) -ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>) -ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree -ResolutionErrors.dfy(565,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly -ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements -ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations -ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context -ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. -ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. -ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field 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(700,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field 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(732,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression -ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1) -ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object) -ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object) -ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object) -ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) -ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(429,2): Error: More than one default constructor -ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context -ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable -ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure -ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops -ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called -ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor -ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int) -ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3) -ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) -ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array) -ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name -ResolutionErrors.dfy(57,7): Error: unresolved identifier: F -ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name -ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance -ResolutionErrors.dfy(59,7): Error: unresolved identifier: G -ResolutionErrors.dfy(61,7): Error: unresolved identifier: M -ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance -ResolutionErrors.dfy(63,7): Error: unresolved identifier: N -ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters -ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global -ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') -ResolutionErrors.dfy(91,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(92,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(94,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(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1) -ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label -ResolutionErrors.dfy(263,2): Error: duplicate label -ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called -ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called -ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated -ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List) -ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int) -ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int) -ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts -ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass, got GenericClass) -ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) -ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool) -ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool) -ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(384,6): Error: print 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(406,6): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint -ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts -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 -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 -ParseErrors.dfy(9,37): error: this operator chain cannot continue with a descending operator -ParseErrors.dfy(10,38): error: this operator chain cannot continue with an ascending operator -ParseErrors.dfy(15,24): error: this operator chain cannot continue with a descending operator -ParseErrors.dfy(18,18): error: this operator cannot be part of a chain -ParseErrors.dfy(19,19): error: this operator cannot be part of a chain -ParseErrors.dfy(20,18): error: this operator cannot be part of a chain -ParseErrors.dfy(21,18): error: chaining not allowed from the previous operator -ParseErrors.dfy(49,8): error: the main operator of a calculation must be transitive -ParseErrors.dfy(65,2): error: this operator cannot continue this calculation -ParseErrors.dfy(66,2): error: this operator cannot continue this calculation -ParseErrors.dfy(71,2): error: this operator cannot continue this calculation -ParseErrors.dfy(72,2): error: this operator cannot continue this calculation -ParseErrors.dfy(78,2): error: this operator cannot continue this calculation -14 parse errors detected in ParseErrors.dfy - --------------------- Array.dfy -------------------- -Array.dfy(13,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(20,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Array.dfy(27,6): Error: index out of range -Execution trace: - (0,0): anon0 -Array.dfy(51,20): Error: assertion violation -Execution trace: - (0,0): anon0 -Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(66,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(110,21): Error: upper bound below lower bound or above length of array -Execution trace: - (0,0): anon0 - (0,0): anon14_Else - (0,0): anon18_Then - (0,0): anon19_Then - (0,0): anon20_Then - (0,0): anon11 -Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Then -Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(150,6): Error: insufficient reads clause to read array element -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Then -Array.dfy(158,6): Error: insufficient reads clause to read array element -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Then -Array.dfy(174,6): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Array.dfy(181,6): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Array.dfy(206,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(205,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(230,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(229,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(236,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(235,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(251,10): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(252,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then - -Dafny program verifier finished with 41 verified, 20 errors - --------------------- MultiDimArray.dfy -------------------- -MultiDimArray.dfy(56,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon12_Then -MultiDimArray.dfy(83,25): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - -Dafny program verifier finished with 8 verified, 2 errors - --------------------- NonGhostQuantifiers.dfy -------------------- -NonGhostQuantifiers.dfy(149,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(153,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(158,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(163,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(186,13): Error: 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 'c' -NonGhostQuantifiers.dfy(16,5): Error: 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 'n' -NonGhostQuantifiers.dfy(45,4): Error: 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 'n' -NonGhostQuantifiers.dfy(49,4): Error: 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 'd' -NonGhostQuantifiers.dfy(53,4): Error: 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 'n' -NonGhostQuantifiers.dfy(77,5): Error: 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 'i' -NonGhostQuantifiers.dfy(81,5): Error: 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 'j' -NonGhostQuantifiers.dfy(91,5): Error: 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 'j' -NonGhostQuantifiers.dfy(106,5): Error: 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 'j' -NonGhostQuantifiers.dfy(114,10): Error: 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 'y' -NonGhostQuantifiers.dfy(123,8): Error: 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 'x' -NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -20 resolution/type errors detected in NonGhostQuantifiers.dfy - --------------------- AdvancedLHS.dfy -------------------- -AdvancedLHS.dfy(34,23): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon15_Else - -Dafny program verifier finished with 7 verified, 1 error - --------------------- ModulesCycle.dfy -------------------- -ModulesCycle.dfy(5,9): Error: module T does not exist -ModulesCycle.dfy(8,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B -2 resolution/type errors detected in ModulesCycle.dfy - --------------------- Modules0.dfy -------------------- -Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(13,7): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(14,8): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(56,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) -Modules0.dfy(57,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(68,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(75,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) -Modules0.dfy(75,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?) -Modules0.dfy(78,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?) -Modules0.dfy(83,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) -Modules0.dfy(92,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?) -Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) -Modules0.dfy(224,8): Error: new can be applied only to reference types (got X) -Modules0.dfy(233,13): Error: Undeclared type X in module B -Modules0.dfy(243,13): Error: unresolved identifier: X -Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X -Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?) -Modules0.dfy(283,12): Error: new can be applied only to reference types (got D) -Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(287,6): Error: expected method call, found expression -Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(288,6): Error: expected method call, found expression -Modules0.dfy(310,24): Error: module Q_Imp does not exist -Modules0.dfy(100,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) -28 resolution/type errors detected in Modules0.dfy - --------------------- Modules1.dfy -------------------- -Modules1.dfy(79,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Modules1.dfy(92,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Modules1.dfy(94,18): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0 -Execution trace: - (0,0): anon0 -Modules1.dfy(62,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 26 verified, 5 errors - --------------------- Modules2.dfy -------------------- -Modules2.dfy(46,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name) -Modules2.dfy(46,10): Error: new can be applied only to reference types (got C) -Modules2.dfy(49,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E') -Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B -Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B -5 resolution/type errors detected in Modules2.dfy - --------------------- BadFunction.dfy -------------------- -BadFunction.dfy(9,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 2 verified, 1 error - --------------------- Comprehensions.dfy -------------------- -Comprehensions.dfy(12,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon10_Then - (0,0): anon4 - (0,0): anon11_Then - (0,0): anon12_Then - (0,0): anon8 - -Dafny program verifier finished with 6 verified, 1 error - --------------------- Basics.dfy -------------------- -Basics.dfy(45,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Basics.dfy(69,42): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Then - (0,0): anon15_Then - Basics.dfy(69,72): anon16_Else - Basics.dfy(69,82): anon17_Else - Basics.dfy(69,95): anon18_Else - (0,0): anon12 -Basics.dfy(113,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 - (0,0): anon10_Then - (0,0): anon3 - (0,0): anon11_Then - (0,0): anon6 - (0,0): anon12_Then - (0,0): anon9 -Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 -Basics.dfy(158,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then -Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3 -Basics.dfy(160,10): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon3 -Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Then -Basics.dfy(176,15): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Else - (0,0): anon6 - (0,0): anon13_Then - (0,0): anon8 - (0,0): anon14_Then -Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 -Basics.dfy(429,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Basics.dfy(440,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -Basics.dfy(442,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 - -Dafny program verifier finished with 61 verified, 14 errors - --------------------- ControlStructures.dfy -------------------- -ControlStructures.dfy(8,3): Error: missing case in case statement: Purple -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -ControlStructures.dfy(8,3): Error: missing case in case statement: Blue -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Else - (0,0): anon9_Then -ControlStructures.dfy(17,3): Error: missing case in case statement: Purple -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -ControlStructures.dfy(46,5): Error: missing case in case statement: Red -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Else - (0,0): anon10_Then -ControlStructures.dfy(54,3): Error: missing case in case statement: Red -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Else - (0,0): anon10_Else - (0,0): anon11_Else - (0,0): anon12_Then -ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -ControlStructures.dfy(218,18): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - (0,0): anon71_Then -ControlStructures.dfy(235,21): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - ControlStructures.dfy(213,9): anon71_Else - (0,0): anon72_Then - (0,0): after_4 - ControlStructures.dfy(224,7): anon74_LoopHead - (0,0): anon74_LoopBody - ControlStructures.dfy(224,7): anon75_Else - ControlStructures.dfy(224,7): anon76_Else - (0,0): anon78_Then - (0,0): anon38 - (0,0): anon83_Then - (0,0): anon52 -ControlStructures.dfy(238,30): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon65_Then - (0,0): anon84_Then - (0,0): anon85_Then - (0,0): anon56 -ControlStructures.dfy(241,17): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - ControlStructures.dfy(213,9): anon71_Else - (0,0): anon72_Then - (0,0): after_4 - ControlStructures.dfy(224,7): anon74_LoopHead - (0,0): anon74_LoopBody - ControlStructures.dfy(224,7): anon75_Else - ControlStructures.dfy(224,7): anon76_Else - (0,0): anon79_Then - (0,0): anon82_Then - (0,0): anon86_Then - (0,0): anon58 - -Dafny program verifier finished with 22 verified, 10 errors - --------------------- Termination.dfy -------------------- -Termination.dfy(359,47): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Else -Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop -Execution trace: - (0,0): anon0 - Termination.dfy(108,3): anon6_LoopHead - (0,0): anon6_LoopBody - Termination.dfy(108,3): anon7_Else - Termination.dfy(108,3): anon8_Else -Termination.dfy(116,3): Error: cannot prove termination; try supplying a decreases clause for the loop -Execution trace: - (0,0): anon0 - Termination.dfy(116,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(116,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(116,3): anon11_Else -Termination.dfy(125,3): Error: decreases expression might not decrease -Execution trace: - (0,0): anon0 - Termination.dfy(125,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(125,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(125,3): anon11_Else -Termination.dfy(126,17): Error: decreases expression must be bounded below by 0 at end of loop iteration -Execution trace: - (0,0): anon0 - Termination.dfy(125,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(125,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(125,3): anon11_Else -Termination.dfy(254,35): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -Termination.dfy(294,3): Error: decreases expression might not decrease -Execution trace: - Termination.dfy(294,3): anon9_LoopHead - (0,0): anon9_LoopBody - Termination.dfy(294,3): anon10_Else - Termination.dfy(294,3): anon11_Else - (0,0): anon12_Else - -Dafny program verifier finished with 59 verified, 7 errors - --------------------- DTypes.dfy -------------------- -DTypes.dfy(18,14): Error: assertion violation -Execution trace: - (0,0): anon0 -DTypes.dfy(56,18): Error: assertion violation -Execution trace: - (0,0): anon0 -DTypes.dfy(120,13): Error: assertion violation -DTypes.dfy(92,30): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(126,13): Error: assertion violation -DTypes.dfy(92,20): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(136,12): Error: assertion violation -DTypes.dfy(131,6): Related location -DTypes.dfy(92,20): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(157,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon4 - -Dafny program verifier finished with 27 verified, 6 errors - --------------------- ParallelResolveErrors.dfy -------------------- -ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable -ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements -ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods -ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement -ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations -ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -21 resolution/type errors detected in ParallelResolveErrors.dfy - --------------------- Parallel.dfy -------------------- -Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold. -Parallel.dfy(60,14): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Then - (0,0): anon34_Then - (0,0): anon35_Then - (0,0): anon14 -Parallel.dfy(38,5): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon38_Then - (0,0): anon20 -Parallel.dfy(42,18): Error: possible violation of postcondition of forall statement -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Else - (0,0): anon39_Then - (0,0): anon40_Then - (0,0): anon26 -Parallel.dfy(47,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Else - (0,0): anon39_Then - (0,0): anon40_Then -Parallel.dfy(93,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon10_Else - (0,0): anon11_Then -Parallel.dfy(99,20): Error: possible violation of postcondition of forall statement -Execution trace: - (0,0): anon0 - (0,0): anon10_Else - (0,0): anon11_Then - (0,0): anon12_Then -Parallel.dfy(122,12): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - (0,0): anon7_Then - (0,0): anon3 -Parallel.dfy(185,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon19_Then - (0,0): anon20_Then - (0,0): anon5 -Parallel.dfy(296,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - -Dafny program verifier finished with 43 verified, 9 errors - --------------------- TypeParameters.dfy -------------------- -TypeParameters.dfy(47,22): Error: assertion violation -Execution trace: - (0,0): anon0 -TypeParameters.dfy(69,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -TypeParameters.dfy(156,12): Error: assertion violation -TypeParameters.dfy(156,28): Related location -Execution trace: - (0,0): anon0 - (0,0): anon20_Then - TypeParameters.dfy(156,32): anon21_Else - (0,0): anon5 -TypeParameters.dfy(158,12): Error: assertion violation -TypeParameters.dfy(158,33): Related location -Execution trace: - (0,0): anon0 - (0,0): anon23_Then - TypeParameters.dfy(158,37): anon24_Else - (0,0): anon11 -TypeParameters.dfy(160,12): Error: assertion violation -TypeParameters.dfy(160,20): Related location -Execution trace: - (0,0): anon0 - (0,0): anon25_Then -TypeParameters.dfy(162,12): Error: assertion violation -TypeParameters.dfy(147,5): Related location -TypeParameters.dfy(162,21): Related location -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -TypeParameters.dfy(164,12): Error: assertion violation -TypeParameters.dfy(149,8): Related location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then -TypeParameters.dfy(178,15): Error BP5005: This loop invariant might not be maintained by the loop. -TypeParameters.dfy(178,38): Related location -Execution trace: - (0,0): anon0 - TypeParameters.dfy(171,3): anon16_LoopHead - (0,0): anon16_LoopBody - TypeParameters.dfy(171,3): anon17_Else - (0,0): anon19_Then - TypeParameters.dfy(177,3): anon20_LoopHead - (0,0): anon20_LoopBody - TypeParameters.dfy(177,3): anon21_Else - TypeParameters.dfy(177,3): anon23_Else - -Dafny program verifier finished with 58 verified, 8 errors - --------------------- Datatypes.dfy -------------------- -Datatypes.dfy(297,10): Error BP5003: A postcondition might not hold on this return path. -Datatypes.dfy(295,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Else - (0,0): anon15_Then - (0,0): anon6 -Datatypes.dfy(298,12): Error: missing case in case statement: Appendix -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Else - (0,0): anon15_Else - (0,0): anon16_Then -Datatypes.dfy(349,5): Error: missing case in case statement: Cons -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then -Datatypes.dfy(349,5): Error: missing case in case statement: Nil -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -Datatypes.dfy(356,8): Error: missing case in case statement: Cons -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then -Datatypes.dfy(356,8): Error: missing case in case statement: Nil -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else - (0,0): anon12_Then -Datatypes.dfy(82,20): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon20_Else - (0,0): anon21_Then - (0,0): anon4 - (0,0): anon22_Else - (0,0): anon23_Then - (0,0): anon24_Else - (0,0): anon25_Then -Datatypes.dfy(170,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -Datatypes.dfy(172,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon5_Then -Datatypes.dfy(201,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons' -Execution trace: - (0,0): anon0 -Datatypes.dfy(204,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons' -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -Datatypes.dfy(225,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T'' -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - -Dafny program verifier finished with 44 verified, 12 errors - --------------------- StatementExpressions.dfy -------------------- -StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - (0,0): anon8_Then -StatementExpressions.dfy(59,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - StatementExpressions.dfy(53,7): anon8_Else -StatementExpressions.dfy(77,6): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - -Dafny program verifier finished with 17 verified, 5 errors - --------------------- Coinductive.dfy -------------------- -Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed -Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed -Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed -Coinductive.dfy(64,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed -Coinductive.dfy(93,8): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(94,8): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(95,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(95,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(101,5): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(104,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(105,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates -16 resolution/type errors detected in Coinductive.dfy - --------------------- Corecursion.dfy -------------------- -Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 20 verified, 8 errors - --------------------- CoResolution.dfy -------------------- -CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default -CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared# -CoResolution.dfy(21,7): Error: unresolved identifier: _k -CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) -CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause -CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause -CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -21 resolution/type errors detected in CoResolution.dfy - --------------------- CoPrefix.dfy -------------------- -CoPrefix.dfy(164,3): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(163,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -CoPrefix.dfy(169,3): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(168,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoPrefix.dfy(63,7): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Else - (0,0): anon9_Then -CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Else - (0,0): anon9_Then -CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold. -CoPrefix.dfy(101,17): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoPrefix.dfy(138,25): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon10_Then -CoPrefix.dfy(142,25): Error: assertion violation -CoPrefix.dfy(117,23): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon12_Then -CoPrefix.dfy(151,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(150,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 41 verified, 9 errors - --------------------- CoinductiveProofs.dfy -------------------- -CoinductiveProofs.dfy(29,12): Error: assertion violation -CoinductiveProofs.dfy(13,17): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(54,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(74,12): Error: assertion violation -CoinductiveProofs.dfy(54,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(80,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(100,12): Error: assertion violation -CoinductiveProofs.dfy(80,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(106,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - -Dafny program verifier finished with 35 verified, 8 errors - --------------------- TypeAntecedents.dfy -------------------- -TypeAntecedents.dfy(35,13): Error: assertion violation -Execution trace: - (0,0): anon0 -TypeAntecedents.dfy(58,1): Error BP5003: A postcondition might not hold on this return path. -TypeAntecedents.dfy(57,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon25_Then - (0,0): anon6 - (0,0): anon28_Then - (0,0): anon8 - (0,0): anon29_Else - (0,0): anon31_Else - (0,0): anon33_Then - (0,0): anon20 - (0,0): anon34_Then - (0,0): anon35_Then - (0,0): anon24 -TypeAntecedents.dfy(66,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon25_Else - (0,0): anon26_Then - (0,0): anon27_Else - -Dafny program verifier finished with 12 verified, 3 errors - --------------------- NoTypeArgs.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- EqualityTypes.dfy -------------------- -EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype -EqualityTypes.dfy(35,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality -EqualityTypes.dfy(40,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes a different number of type parameters -EqualityTypes.dfy(41,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters -EqualityTypes.dfy(45,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality -EqualityTypes.dfy(46,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality -EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) -EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) -EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) -EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D) -EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D) -11 resolution/type errors detected in EqualityTypes.dfy - --------------------- SplitExpr.dfy -------------------- -SplitExpr.dfy(92,15): Error: loop invariant violation -SplitExpr.dfy(86,44): Related location -Execution trace: - SplitExpr.dfy(91,3): anon7_LoopHead - -Dafny program verifier finished with 10 verified, 1 error - --------------------- LoopModifies.dfy -------------------- -LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(16,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(16,4): anon9_Else - LoopModifies.dfy(16,4): anon11_Else -LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(44,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(44,4): anon9_Else - LoopModifies.dfy(44,4): anon11_Else -LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(59,4): anon9_LoopHead - (0,0): anon9_LoopBody - LoopModifies.dfy(59,4): anon10_Else - LoopModifies.dfy(59,4): anon12_Else -LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause -Execution trace: - (0,0): anon0 -LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(92,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(92,4): anon9_Else - LoopModifies.dfy(92,4): anon11_Else -LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(136,4): anon17_LoopHead - (0,0): anon17_LoopBody - LoopModifies.dfy(136,4): anon18_Else - LoopModifies.dfy(136,4): anon20_Else - LoopModifies.dfy(141,7): anon21_LoopHead - (0,0): anon21_LoopBody - LoopModifies.dfy(141,7): anon22_Else - LoopModifies.dfy(141,7): anon24_Else -LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(195,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(195,4): anon9_Else - LoopModifies.dfy(195,4): anon11_Else -LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(275,4): anon16_LoopHead - (0,0): anon16_LoopBody - LoopModifies.dfy(275,4): anon17_Else - LoopModifies.dfy(275,4): anon19_Else - LoopModifies.dfy(283,7): anon20_LoopHead - (0,0): anon20_LoopBody - LoopModifies.dfy(283,7): anon21_Else - LoopModifies.dfy(283,7): anon23_Else - -Dafny program verifier finished with 23 verified, 9 errors - --------------------- Refinement.dfy -------------------- -Refinement.dfy(15,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(14,17): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(33,20): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy(64,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Refinement.dfy(74,17): Error: assertion violation -Execution trace: - (0,0): anon0 -Refinement.dfy(93,12): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(72,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Refinement.dfy(96,3): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(77,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy[IncorrectConcrete](115,15): Related location: This is the postcondition that might not hold. -Refinement.dfy(180,9): Related location -Execution trace: - (0,0): anon0 -Refinement.dfy(187,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy[IncorrectConcrete](123,15): Related location: This is the postcondition that might not hold. -Refinement.dfy(180,9): Related location -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Refinement.dfy(193,7): Error: assertion violation -Refinement.dfy[IncorrectConcrete](131,24): Related location -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 48 verified, 9 errors - --------------------- RefinementErrors.dfy -------------------- -RefinementErrors.dfy(30,17): Error: a refining method is not allowed to add preconditions -RefinementErrors.dfy(31,15): Error: a refining method is not allowed to extend the modifies clause -RefinementErrors.dfy(34,14): Error: a predicate declaration (abc) can only refine a predicate -RefinementErrors.dfy(35,8): Error: a field re-declaration (xyz) must be to ghostify the field -RefinementErrors.dfy(37,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F -RefinementErrors.dfy(38,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C') -RefinementErrors.dfy(38,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A') -RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B') -RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq' instead of 'set') -RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines -RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G -11 resolution/type errors detected in RefinementErrors.dfy - --------------------- ReturnErrors.dfy -------------------- -ReturnErrors.dfy(32,10): Error: cannot have method call in return statement. -ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement. -ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'. -3 resolution/type errors detected in ReturnErrors.dfy - --------------------- ReturnTests.dfy -------------------- - -Dafny program verifier finished with 20 verified, 0 errors - --------------------- ChainingDisjointTests.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- CallStmtTests.dfy -------------------- -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable -CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable -2 resolution/type errors detected in CallStmtTests.dfy - --------------------- MultiSets.dfy -------------------- -MultiSets.dfy(159,3): Error BP5003: A postcondition might not hold on this return path. -MultiSets.dfy(158,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MultiSets.dfy(165,3): Error BP5003: A postcondition might not hold on this return path. -MultiSets.dfy(164,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MultiSets.dfy(178,11): Error: new number of occurrences might be negative -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -MultiSets.dfy(269,24): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Then - (0,0): anon14_Else - -Dafny program verifier finished with 54 verified, 4 errors - --------------------- PredExpr.dfy -------------------- -PredExpr.dfy(7,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -PredExpr.dfy(52,17): Error: assertion violation -Execution trace: - (0,0): anon0 -PredExpr.dfy(77,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon3 - PredExpr.dfy(76,20): anon10_Else - (0,0): anon6 - -Dafny program verifier finished with 11 verified, 4 errors - --------------------- Predicates.dfy -------------------- -Predicates.dfy[B](21,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[B](20,15): Related location: This is the postcondition that might not hold. -Predicates.dfy(31,9): Related location -Execution trace: - (0,0): anon0 -Predicates.dfy(88,16): Error: assertion violation -Execution trace: - (0,0): anon0 -Predicates.dfy(92,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Predicates.dfy[Tricky_Full](126,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[Tricky_Full](125,15): Related location: This is the postcondition that might not hold. -Predicates.dfy(136,7): Related location -Predicates.dfy[Tricky_Full](116,9): Related location -Execution trace: - (0,0): anon0 -Predicates.dfy(164,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy(163,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Predicates.dfy[Q1](154,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[Q1](153,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 52 verified, 6 errors - --------------------- Skeletons.dfy -------------------- -Skeletons.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. -Skeletons.dfy(44,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - Skeletons.dfy[C0](32,5): anon11_LoopHead - (0,0): anon11_LoopBody - Skeletons.dfy[C0](32,5): anon12_Else - (0,0): anon13_Then - Skeletons.dfy[C0](37,19): anon15_Else - (0,0): anon10 - -Dafny program verifier finished with 9 verified, 1 error - --------------------- OpaqueFunctions.dfy -------------------- -OpaqueFunctions.dfy(27,16): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(58,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(60,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(63,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(66,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(77,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -OpaqueFunctions.dfy(86,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(88,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(91,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(94,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(105,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -OpaqueFunctions.dfy(114,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(116,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(119,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(122,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(138,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 43 verified, 19 errors - --------------------- Maps.dfy -------------------- -Maps.dfy(78,8): Error: element may not be in domain -Execution trace: - (0,0): anon0 -Maps.dfy(128,13): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 32 verified, 2 errors - --------------------- LiberalEquality.dfy -------------------- -LiberalEquality.dfy(20,14): Error: arguments must have the same type (got T and U) -LiberalEquality.dfy(39,14): Error: arguments must have the same type (got Weird and Weird) -LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array and array) -3 resolution/type errors detected in LiberalEquality.dfy - --------------------- RefinementModificationChecking.dfy -------------------- -RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously -RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously -2 resolution/type errors detected in RefinementModificationChecking.dfy - --------------------- TailCalls.dfy -------------------- -TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code -TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods -5 resolution/type errors detected in TailCalls.dfy - --------------------- IteratorResolution.dfy -------------------- -IteratorResolution.dfy(62,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(67,18): Error: arguments must have the same type (got _T0 and int) -IteratorResolution.dfy(79,19): Error: RHS (of type bool) not assignable to LHS (of type int) -IteratorResolution.dfy(82,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called -IteratorResolution.dfy(86,15): Error: logical negation expects a boolean argument (instead got int) -IteratorResolution.dfy(20,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(126,9): Error: unresolved identifier: _decreases3 -IteratorResolution.dfy(127,21): Error: arguments must have the same type (got int and ?) -IteratorResolution.dfy(128,2): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(135,9): Error: unresolved identifier: _decreases1 -IteratorResolution.dfy(140,9): Error: unresolved identifier: _decreases0 -12 resolution/type errors detected in IteratorResolution.dfy - --------------------- Iterators.dfy -------------------- -Iterators.dfy(251,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(274,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(284,24): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 -Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 -Iterators.dfy(343,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 -Iterators.dfy(370,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(103,22): Error: assertion violation -Execution trace: - (0,0): anon0 -Iterators.dfy(106,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Iterators.dfy(177,28): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon15_Then -Iterators.dfy(208,7): Error: an assignment to _new is only allowed to shrink the set -Execution trace: - (0,0): anon0 - Iterators.dfy(197,3): anon16_LoopHead - (0,0): anon16_LoopBody - Iterators.dfy(197,3): anon17_Else - Iterators.dfy(197,3): anon19_Else - (0,0): anon20_Then -Iterators.dfy(212,21): Error: assertion violation -Execution trace: - (0,0): anon0 - Iterators.dfy(197,3): anon16_LoopHead - (0,0): anon16_LoopBody - Iterators.dfy(197,3): anon17_Else - Iterators.dfy(197,3): anon19_Else - (0,0): anon21_Then -Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold. -Iterators.dfy(4,10): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon35_Then - (0,0): anon2 - (0,0): anon36_Then - (0,0): anon5 - (0,0): anon37_Then -Iterators.dfy(89,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Iterators.dfy(119,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Iterators.dfy(150,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold. -Iterators.dfy(125,10): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Iterators.dfy(234,14): Error: assertion violation -Execution trace: - (0,0): anon0 - Iterators.dfy(225,3): anon14_LoopHead - (0,0): anon14_LoopBody - Iterators.dfy(225,3): anon15_Else - Iterators.dfy(225,3): anon18_Else - (0,0): anon19_Else - -Dafny program verifier finished with 65 verified, 20 errors - --------------------- RankPos.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- RankNeg.dfy -------------------- -RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then - -Dafny program verifier finished with 1 verified, 4 errors - --------------------- Computations.dfy -------------------- - -Dafny program verifier finished with 58 verified, 0 errors - --------------------- ComputationsNeg.dfy -------------------- -ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path. -ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(23,1): Error BP5003: A postcondition might not hold on this return path. -ComputationsNeg.dfy(22,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(36,13): Error: assertion violation -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(45,13): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 7 verified, 5 errors - --------------------- Include.dfy -------------------- -Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(17,20): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Includee.dfy[Concrete](22,16): Error: assertion violation -Execution trace: - (0,0): anon0 -Include.dfy(27,7): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy[Concrete](20,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - -Dafny program verifier finished with 4 verified, 3 errors - --------------------- Includee.dfy -------------------- -Includee.dfy(21,3): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(20,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Includee.dfy(24,18): Error: assertion violation -Execution trace: - (0,0): anon0 -Includee.dfy(6,1): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(5,13): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 5 verified, 3 errors - --------------------- AutoReq.dfy -------------------- -AutoReq.dfy(247,3): Error: possible violation of function precondition -AutoReq.dfy(239,12): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(13,3): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(25,3): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(38,12): Error: assertion violation -AutoReq.dfy(31,13): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then -AutoReq.dfy(38,12): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then -AutoReq.dfy(40,12): Error: assertion violation -AutoReq.dfy(31,27): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -AutoReq.dfy(40,12): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -AutoReq.dfy(45,12): Error: assertion violation -AutoReq.dfy(31,13): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - -Dafny program verifier finished with 52 verified, 8 errors - --------------------- DatatypeUpdate.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ModifyStmt.dfy -------------------- -ModifyStmt.dfy(27,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(42,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(48,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(61,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(70,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(89,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - ModifyStmt.dfy(81,7): anon10_LoopHead - (0,0): anon10_LoopBody - ModifyStmt.dfy(81,7): anon11_Else - (0,0): anon12_Then - (0,0): anon8 -ModifyStmt.dfy(99,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(110,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(122,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -ModifyStmt.dfy(134,7): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(172,15): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 25 verified, 11 errors - --------------------- SeqSlice.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- RealCompare.dfy -------------------- -RealCompare.dfy(35,5): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0 -Execution trace: - (0,0): anon0 -RealCompare.dfy(141,12): Error: assertion violation -Execution trace: - (0,0): anon0 - RealCompare.dfy(133,3): anon7_LoopHead - (0,0): anon7_LoopBody - RealCompare.dfy(133,3): anon8_Else - (0,0): anon9_Then -RealCompare.dfy(156,12): Error: assertion violation -Execution trace: - (0,0): anon0 - RealCompare.dfy(147,3): anon9_LoopHead - (0,0): anon9_LoopBody - RealCompare.dfy(147,3): anon10_Else - (0,0): anon12_Then - -Dafny program verifier finished with 24 verified, 4 errors - --------------------- AssumptionVariables0.dfy -------------------- -AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && " -AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost -AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool' -AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " -AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " -AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost -AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool' -AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -13 resolution/type errors detected in AssumptionVariables0.dfy - --------------------- AssumptionVariables1.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Superposition.dfy -------------------- - -Verifying CheckWellformed$$_0_M0.C.M ... - [0 proof obligations] verified - -Verifying Impl$$_0_M0.C.M ... - [4 proof obligations] verified - -Verifying CheckWellformed$$_0_M0.C.P ... - [4 proof obligations] verified - -Verifying CheckWellformed$$_0_M0.C.Q ... - [3 proof obligations] error -Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy(28,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - -Verifying CheckWellformed$$_0_M0.C.R ... - [3 proof obligations] error -Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy(34,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - -Verifying CheckWellformed$$_1_M1.C.M ... - [0 proof obligations] verified - -Verifying Impl$$_1_M1.C.M ... - [1 proof obligation] verified - -Verifying CheckWellformed$$_1_M1.C.P ... - [1 proof obligation] error -Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon9_Then - (0,0): anon6 - -Verifying CheckWellformed$$_1_M1.C.Q ... - [0 proof obligations] verified - -Verifying CheckWellformed$$_1_M1.C.R ... - [0 proof obligations] verified - -Dafny program verifier finished with 7 verified, 3 errors - --------------------- SmallTests.dfy -------------------- -SmallTests.dfy(33,11): Error: index out of range -Execution trace: - (0,0): anon0 -SmallTests.dfy(64,36): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -SmallTests.dfy(65,51): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Else - (0,0): anon3 - (0,0): anon13_Else -SmallTests.dfy(66,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - (0,0): anon3 - (0,0): anon13_Then - (0,0): anon6 -SmallTests.dfy(85,24): Error: target object may be null -Execution trace: - (0,0): anon0 - SmallTests.dfy(84,5): anon8_LoopHead - (0,0): anon8_LoopBody - (0,0): anon9_Then -SmallTests.dfy(119,5): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon3 -SmallTests.dfy(132,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -SmallTests.dfy(134,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(174,9): Error: assignment may update an object field not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon22_Else - (0,0): anon24_Else - (0,0): anon26_Else - (0,0): anon28_Then - (0,0): anon29_Then - (0,0): anon19 -SmallTests.dfy(198,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -SmallTests.dfy(205,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Then -SmallTests.dfy(207,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Else -SmallTests.dfy(253,24): Error BP5002: A precondition for this call might not hold. -SmallTests.dfy(231,30): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - SmallTests.dfy(248,19): anon3_Else - (0,0): anon2 -SmallTests.dfy(358,12): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(368,12): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(378,6): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(682,14): Error: assertion violation -Execution trace: - (0,0): anon0 - SmallTests.dfy(679,5): anon7_LoopHead - (0,0): anon7_LoopBody - SmallTests.dfy(679,5): anon8_Else - (0,0): anon9_Then -SmallTests.dfy(703,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Then - (0,0): anon3 -SmallTests.dfy(288,3): Error BP5003: A postcondition might not hold on this return path. -SmallTests.dfy(282,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon18_Else - (0,0): anon23_Then - (0,0): anon24_Then - (0,0): anon15 - (0,0): anon25_Else -SmallTests.dfy(329,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon7 -SmallTests.dfy(336,10): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(346,4): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(390,10): Error BP5003: A postcondition might not hold on this return path. -SmallTests.dfy(393,41): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -SmallTests.dfy(553,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -SmallTests.dfy(567,20): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - (0,0): anon28_Then - (0,0): anon4 - (0,0): anon29_Then - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Then - (0,0): anon32_Then - (0,0): anon12 -SmallTests.dfy(569,15): Error: left-hand sides 1 and 2 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - SmallTests.dfy(562,18): anon28_Else - (0,0): anon4 - (0,0): anon29_Else - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Else - (0,0): anon35_Then - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon22 - (0,0): anon38_Then -SmallTests.dfy(576,25): Error: target object may be null -Execution trace: - (0,0): anon0 -SmallTests.dfy(589,10): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(613,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 -SmallTests.dfy(636,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Then - (0,0): anon4 - (0,0): anon10_Then - (0,0): anon7 -SmallTests.dfy(650,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon3 -SmallTests.dfy(652,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -SmallTests.dfy(665,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 87 verified, 33 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- LetExpr.dfy -------------------- -LetExpr.dfy(8,12): Error: assertion violation -Execution trace: - (0,0): anon0 -LetExpr.dfy(107,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then -LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -LetExpr.dfy(256,24): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -LetExpr.dfy(285,14): Error: RHS is not certain to look like the pattern 'Agnes' -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -LetExpr.dfy(302,42): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -LetExpr.dfy(304,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - -Dafny program verifier finished with 38 verified, 8 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- Calculations.dfy -------------------- -Calculations.dfy(6,6): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon24_Then -Calculations.dfy(11,15): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(11,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(55,12): Error: assertion violation -Execution trace: - (0,0): anon0 - Calculations.dfy(50,3): anon5_Else -Calculations.dfy(78,15): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -Calculations.dfy(78,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - -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 - -Dafny program verifier finished with 15 verified, 0 errors -Compilation error: Arbitrary type ('_module.MyType') cannot be compiled -Compilation error: Iterator _module.Iter has no body -Compilation error: Method _module._default.M has no body -Compilation error: Method _module._default.P has no body -Compilation error: an assume statement cannot be compiled (line 11) -Compilation error: Function _module._default.F has no body -Compilation error: Function _module._default.H has no body -Compilation error: an assume statement cannot be compiled (line 20) -Compilation error: an assume statement cannot be compiled (line 23) -Compilation error: an assume statement cannot be compiled (line 28) -Compilation error: an assume statement cannot be compiled (line 37) diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat deleted file mode 100644 index 1a371ba3..00000000 --- a/Test/dafny0/runtest.bat +++ /dev/null @@ -1,61 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -for %%f in (Simple.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f -) - -for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy - FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy - Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy - ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy - Comprehensions.dfy Basics.dfy ControlStructures.dfy - Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy - TypeParameters.dfy Datatypes.dfy StatementExpressions.dfy - Coinductive.dfy Corecursion.dfy CoResolution.dfy - CoPrefix.dfy CoinductiveProofs.dfy - TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy - LoopModifies.dfy Refinement.dfy RefinementErrors.dfy - ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy - CallStmtTests.dfy MultiSets.dfy PredExpr.dfy - Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy - Maps.dfy LiberalEquality.dfy - RefinementModificationChecking.dfy TailCalls.dfy - IteratorResolution.dfy Iterators.dfy - RankPos.dfy RankNeg.dfy - Computations.dfy ComputationsNeg.dfy - Include.dfy Includee.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy - RealCompare.dfy - AssumptionVariables0.dfy AssumptionVariables1.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f -) - -for %%f in (Superposition.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f -) - -for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f - %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 diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer deleted file mode 100644 index e60451c2..00000000 --- a/Test/dafny1/Answer +++ /dev/null @@ -1,124 +0,0 @@ - --------------------- Queue.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- PriorityQueue.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- ExtensibleArray.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- ExtensibleArrayAuto.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- BinaryTree.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- UnboundedStack.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SeparationLogicList.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- ListCopy.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- ListReverse.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ListContents.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- MatrixFun.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- pow2.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- SchorrWaite.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- SchorrWaite-stages.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- Cubes.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- SumOfCubes.dfy -------------------- - -Dafny program verifier finished with 17 verified, 0 errors - --------------------- FindZero.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- TerminationDemos.dfy -------------------- - -Dafny program verifier finished with 14 verified, 0 errors - --------------------- Substitution.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- TreeDatatype.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- KatzManna.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Induction.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- Rippling.dfy -------------------- - -Dafny program verifier finished with 141 verified, 0 errors - --------------------- MoreInduction.dfy -------------------- -MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 15 verified, 4 errors - --------------------- Celebrity.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- BDD.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- UltraFilter.dfy -------------------- - -Dafny program verifier finished with 19 verified, 0 errors diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat deleted file mode 100644 index f02a7965..00000000 --- a/Test/dafny1/runtest.bat +++ /dev/null @@ -1,26 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy - -rem for %%f in (Queue.dfy PriorityQueue.dfy -rem ExtensibleArray.dfy ExtensibleArrayAuto.dfy -rem BinaryTree.dfy -rem UnboundedStack.dfy -rem SeparationLogicList.dfy -rem ListCopy.dfy ListReverse.dfy ListContents.dfy -rem MatrixFun.dfy pow2.dfy -rem SchorrWaite.dfy SchorrWaite-stages.dfy -rem Cubes.dfy SumOfCubes.dfy FindZero.dfy -rem TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy -rem Induction.dfy Rippling.dfy MoreInduction.dfy -rem Celebrity.dfy BDD.dfy -rem UltraFilter.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer deleted file mode 100644 index 9fa6f4ef..00000000 --- a/Test/dafny2/Answer +++ /dev/null @@ -1,60 +0,0 @@ - --------------------- Classics.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- TreeBarrier.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- COST-verif-comp-2011-1-MaxArray.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- COST-verif-comp-2011-2-MaxTree-class.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- COST-verif-comp-2011-2-MaxTree-datatype.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- COST-verif-comp-2011-3-TwoDuplicates.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy -------------------- - -Dafny program verifier finished with 25 verified, 0 errors - --------------------- StoreAndRetrieve.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- Intervals.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- TreeFill.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- TuringFactorial.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- MajorityVote.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- SegmentSum.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- MonotonicHeapstate.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors - --------------------- Calculations.dfy -------------------- - -Dafny program verifier finished with 31 verified, 0 errors diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat deleted file mode 100644 index d038acce..00000000 --- a/Test/dafny2/runtest.bat +++ /dev/null @@ -1,27 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -REM soon again: SnapshotableTrees.dfy - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Classics.dfy TreeBarrier.dfy COST-verif-comp-2011-1-MaxArray.dfy COST-verif-comp-2011-2-MaxTree-class.dfy COST-verif-comp-2011-2-MaxTree-datatype.dfy COST-verif-comp-2011-3-TwoDuplicates.dfy COST-verif-comp-2011-4-FloydCycleDetect.dfy StoreAndRetrieve.dfy Intervals.dfy TreeFill.dfy TuringFactorial.dfy MajorityVote.dfy SegmentSum.dfy MonotonicHeapstate.dfy Calculations.dfy - -rem for %%f in ( -rem Classics.dfy -rem TreeBarrier.dfy -rem COST-verif-comp-2011-1-MaxArray.dfy -rem COST-verif-comp-2011-2-MaxTree-class.dfy -rem COST-verif-comp-2011-2-MaxTree-datatype.dfy -rem COST-verif-comp-2011-3-TwoDuplicates.dfy -rem COST-verif-comp-2011-4-FloydCycleDetect.dfy -rem StoreAndRetrieve.dfy -rem Intervals.dfy TreeFill.dfy TuringFactorial.dfy -rem MajorityVote.dfy SegmentSum.dfy -rem MonotonicHeapstate.dfy Calculations.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer deleted file mode 100644 index 9e8ac835..00000000 --- a/Test/dafny3/Answer +++ /dev/null @@ -1,64 +0,0 @@ - --------------------- Iter.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- Streams.dfy -------------------- - -Dafny program verifier finished with 52 verified, 0 errors - --------------------- Dijkstra.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- CachedContainer.dfy -------------------- - -Dafny program verifier finished with 47 verified, 0 errors - --------------------- SimpleInduction.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SimpleCoinduction.dfy -------------------- - -Dafny program verifier finished with 31 verified, 0 errors - --------------------- CalcExample.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- InductionVsCoinduction.dfy -------------------- - -Dafny program verifier finished with 20 verified, 0 errors - --------------------- Zip.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- SetIterations.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- Paulson.dfy -------------------- - -Dafny program verifier finished with 28 verified, 0 errors - --------------------- Filter.dfy -------------------- - -Dafny program verifier finished with 43 verified, 0 errors - --------------------- WideTrees.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- InfiniteTrees.dfy -------------------- - -Dafny program verifier finished with 88 verified, 0 errors - --------------------- OpaqueTrees.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- GenericSort.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat deleted file mode 100644 index 41971d4e..00000000 --- a/Test/dafny3/runtest.bat +++ /dev/null @@ -1,19 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy GenericSort.dfy - -rem for %%f in ( -rem Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy -rem SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy -rem InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy -rem Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy -rem OpaqueTrees.dfy GenericSort.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer deleted file mode 100644 index 14986a59..00000000 --- a/Test/dafny4/Answer +++ /dev/null @@ -1,43 +0,0 @@ - --------------------- CoqArt-InsertionSort.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors - --------------------- GHC-MergeSort.dfy -------------------- - -Dafny program verifier finished with 83 verified, 0 errors - --------------------- Fstar-QuickSort.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Primes.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- KozenSilva.dfy -------------------- - -Dafny program verifier finished with 47 verified, 0 errors - --------------------- SoftwareFoundations-Basics.dfy -------------------- -SoftwareFoundations-Basics.dfy(41,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 82 verified, 1 error - --------------------- NumberRepresentations.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- Circ.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- ACL2-extractor.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- ClassRefinement.dfy -------------------- - -Dafny program verifier finished with 18 verified, 0 errors diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat deleted file mode 100644 index cec5d271..00000000 --- a/Test/dafny4/runtest.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy ACL2-extractor.dfy ClassRefinement.dfy diff --git a/Test/runtest.bat b/Test/runtest.bat deleted file mode 100644 index dfc3ae00..00000000 --- a/Test/runtest.bat +++ /dev/null @@ -1,39 +0,0 @@ -@echo off -rem Usage: runtest.bat -if "%1" == "" goto noDirSpecified -if not exist %1\nul goto noDirExists -echo ----- Running regression test %1 -pushd %1 -if not exist runtest.bat goto noRunTest -call runtest.bat -nologo -logPrefix:%* > Output -rem There seem to be some race between finishing writing to the Output file, and running fc. -rem Calling fc twice seems to fix (or at least alleviate) the problem. -fc /W Answer Output > nul -fc /W Answer Output > nul -if not errorlevel 1 goto passTest -echo ============ %1 FAILED ==================================== -goto errorEnd - -:passTest -echo Success: %1 -goto end - -:noDirSpecified -echo runtest: Error: Syntax: runtest testDirectory [ additionalTestArguments ... ] -goto errorEnd - -:noDirExists -echo runtest: Error: There is no test directory %1 -goto errorEnd - -:noRunTest -echo runtest: Error: no runtest.bat found in test directory %1 -goto errorEnd - -:errorEnd -popd -exit /b 1 - -:end -popd -exit /b 0 diff --git a/Test/runtestall.bat b/Test/runtestall.bat deleted file mode 100644 index 207bb030..00000000 --- a/Test/runtestall.bat +++ /dev/null @@ -1,24 +0,0 @@ -@echo off -setlocal - -set errors=0 - -if "%1" == "short" goto UseShort - -set IncludeLong=True -goto Loop - -:UseShort -set IncludeLong=False -shift -goto Loop - -:Loop -for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1 - -if not %IncludeLong%==True goto End - -for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Long call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1 - -:End -exit /b %errors% \ No newline at end of file diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer deleted file mode 100644 index 90bbcc78..00000000 --- a/Test/vacid0/Answer +++ /dev/null @@ -1,12 +0,0 @@ - --------------------- LazyInitArray.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- SparseArray.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- Composite.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking deleted file mode 100644 index e69de29b..00000000 diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat deleted file mode 100644 index d7f31c3b..00000000 --- a/Test/vacid0/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* LazyInitArray.dfy SparseArray.dfy Composite.dfy - -rem for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer deleted file mode 100644 index 43eddcb1..00000000 --- a/Test/vstte2012/Answer +++ /dev/null @@ -1,24 +0,0 @@ - --------------------- Two-Way-Sort.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Combinators.dfy -------------------- - -Dafny program verifier finished with 25 verified, 0 errors - --------------------- RingBuffer.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- RingBufferAuto.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- Tree.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- BreadthFirstSearch.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat deleted file mode 100644 index 7e597fd4..00000000 --- a/Test/vstte2012/runtest.bat +++ /dev/null @@ -1,23 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy - -echo. -echo -------------------- BreadthFirstSearch.dfy -------------------- -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /vcsMaxKeepGoingSplits:10 %* BreadthFirstSearch.dfy - -rem for %%f in ( -rem Two-Way-Sort.dfy -rem Combinators.dfy -rem RingBuffer.dfy RingBufferAuto.dfy -rem Tree.dfy -rem BreadthFirstSearch.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) -- cgit v1.2.3 From d8ed73e962c5e7120497cbbdd25e30ac84df49d1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 1 Jul 2014 14:55:45 -0700 Subject: Color nested comments correctly in the Dafny IDE --- Source/DafnyExtension/TokenTagger.cs | 68 ++++++++++++++++++++++++------------ 1 file changed, 45 insertions(+), 23 deletions(-) diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 48f5d1b4..8a01c22f 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -5,6 +5,7 @@ using System.Linq; using Microsoft.VisualStudio.Text; using Microsoft.VisualStudio.Text.Tagging; using Microsoft.VisualStudio.Utilities; +using System.Diagnostics.Contracts; namespace DafnyLanguage @@ -148,20 +149,24 @@ namespace DafnyLanguage private static List Rescan(ITextSnapshot newSnapshot) { List newRegions = new List(); - bool stillScanningLongComment = false; - SnapshotPoint commentStart = new SnapshotPoint(); // used only when stillScanningLongComment - SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when stillScanningLongComment + int longCommentDepth = 0; + SnapshotPoint commentStart = new SnapshotPoint(); // used only when longCommentDepth != 0 + SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when longCommentDepth != 0 foreach (ITextSnapshotLine line in newSnapshot.Lines) { string txt = line.GetText(); // the current line (without linebreak characters) int N = txt.Length; // length of the current line int cur = 0; // offset into the current line - if (stillScanningLongComment) { - if (ScanForEndOfComment(txt, ref cur)) { + if (longCommentDepth != 0) { + ScanForEndOfComment(txt, ref longCommentDepth, ref cur); + if (longCommentDepth == 0) { + // we just finished parsing a long comment newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment)); - stillScanningLongComment = false; } else { + // we're still parsing the long comment + Contract.Assert(cur == txt.Length); commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur); + goto OUTER_CONTINUE; } } @@ -179,9 +184,9 @@ namespace DafnyLanguage if ('a' <= ch && ch <= 'z') break; if ('A' <= ch && ch <= 'Z') break; if ('0' <= ch && ch <= '9') { ty = DafnyTokenKind.Number; break; } + if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break; // parts of identifiers if (ch == '"') { ty = DafnyTokenKind.String; break; } if (ch == '/') { ty = DafnyTokenKind.Comment; break; } - if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break; // parts of identifiers } // advance to the end of the token @@ -211,7 +216,7 @@ namespace DafnyLanguage } } } else if (ty == DafnyTokenKind.Comment) { - if (end == N) continue; // this was not the start of a comment + if (end == N) continue; // this was not the start of a comment; it was just a single "/" and we don't care to color it char ch = txt[end]; if (ch == '/') { // a short comment @@ -220,15 +225,18 @@ namespace DafnyLanguage // a long comment; find the matching "*/" end++; commentStart = new SnapshotPoint(newSnapshot, line.Start + cur); - if (ScanForEndOfComment(txt, ref end)) { + Contract.Assert(longCommentDepth == 0); + longCommentDepth = 1; + ScanForEndOfComment(txt, ref longCommentDepth, ref end); + if (longCommentDepth == 0) { + // we finished scanning a long comment, and "end" is set to right after it newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment)); } else { - stillScanningLongComment = true; commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end); } continue; } else { - // not a comment + // not a comment; it was just a single "/" and we don't care to color it continue; } } else { @@ -322,7 +330,7 @@ namespace DafnyLanguage #endregion break; default: - continue; // it was an identifier + continue; // it was an identifier, so we don't color it } } } @@ -332,26 +340,40 @@ namespace DafnyLanguage OUTER_CONTINUE: ; } - if (stillScanningLongComment) { + if (longCommentDepth != 0) { + // This was a malformed comment, running to the end of the buffer. Above, we let "commentEndAsWeKnowIt" be the end of the + // last line, so we can use it here. newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment)); } return newRegions; } - private static bool ScanForEndOfComment(string txt, ref int end) { - int N = txt.Length; - for (; end < N; end++) { + /// + /// Scans "txt" beginning with depth "depth", which is assumed to be non-0. Any occurrences of "/*" or "*/" + /// increment or decrement "depth". If "depth" ever reaches 0, then "end" returns as the number of characters + /// consumed from "txt" (including the last "*/"). If "depth" is still non-0 when the entire "txt" has + /// been consumed, then "end" returns as the length of "txt". (Note, "end" may return as the length of "txt" + /// if "depth" is still non-0 or if "depth" became 0 from reading the last characters of "txt".) + /// + private static void ScanForEndOfComment(string txt, ref int depth, ref int end) { + Contract.Requires(depth > 0); + + int Nminus1 = txt.Length - 1; // no reason ever to look at the last character of the line, unless the second-to-last character is '*' or '/' + for (; end < Nminus1; ) { char ch = txt[end]; - if (ch == '*' && end + 1 < N) { - ch = txt[end + 1]; - if (ch == '/') { - end += 2; - return true; - } + if (ch == '*' && txt[end + 1] == '/') { + end += 2; + depth--; + if (depth == 0) { return; } + } else if (ch == '/' && txt[end + 1] == '*') { + end += 2; + depth++; + } else { + end++; } } - return false; // hit end-of-line without finding end-of-comment + end = txt.Length; // we didn't look at the last character, but we still consumed all the output } } -- cgit v1.2.3 From 3f3f4a4d42cb0926acd6606b537b8a1a743e138e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 1 Jul 2014 15:35:13 -0700 Subject: Dispose DafnyTokenTagger --- Source/DafnyExtension/TokenTagger.cs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 8a01c22f..5068354a 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -70,11 +70,12 @@ namespace DafnyLanguage } } - internal sealed class DafnyTokenTagger : ITagger + internal sealed class DafnyTokenTagger : ITagger, IDisposable { ITextBuffer _buffer; ITextSnapshot _snapshot; List _regions; + bool _disposed; internal DafnyTokenTagger(ITextBuffer buffer) { _buffer = buffer; @@ -84,6 +85,19 @@ namespace DafnyLanguage _buffer.Changed += new EventHandler(ReparseFile); } + public void Dispose() { + lock (this) { + if (!_disposed) { + _buffer.Changed -= ReparseFile; + _buffer = null; + _snapshot = null; + _regions = null; + _disposed = true; + } + } + GC.SuppressFinalize(this); + } + public event EventHandler TagsChanged; public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { -- cgit v1.2.3