From ed46d78f54da4cb22539adc995ed85bdda0538fb Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 12 Jan 2017 08:48:42 -0800 Subject: [PATCH] Report errors originating from included files when verifying including file Closes #16 --- Source/Dafny/DafnyAst.cs | 13 ++++++- Source/Dafny/DafnyMain.cs | 9 +++-- Source/Dafny/Parser.cs | 38 ++++++++++--------- Source/Dafny/Reporting.cs | 12 +++++- Source/DafnyServer/DafnyHelper.cs | 2 +- .../dafny0/AssumptionVariables0.dfy.expect | 3 +- .../dafny0/BindingGuardsResolution.dfy.expect | 3 +- .../dafny0/BitvectorResolution.dfy.expect | 3 +- .../dafny0/CallStmtTests.dfy.expect | 3 +- .../allocated1/dafny0/CoResolution.dfy.expect | 3 +- Test/allocated1/dafny0/Coinductive.dfy.expect | 3 +- .../DatatypeUpdateResolution.dfy.expect | 3 +- .../dafny0/DiscoverBoundsErrors.dfy.expect | 3 +- .../dafny0/DisplayExpressions.dfy.expect | 3 +- .../dafny0/EqualityTypes.dfy.expect | 3 +- .../dafny0/ErrorsInRelatedModules.dfy.expect | 3 +- Test/allocated1/dafny0/Fuel.dfy.expect | 1 + Test/allocated1/dafny0/IMaps2.dfy.expect | 3 +- .../dafny0/LiberalEquality.dfy.expect | 3 +- Test/allocated1/dafny0/Modules0.dfy.expect | 3 +- Test/allocated1/dafny0/Modules2.dfy.expect | 3 +- .../allocated1/dafny0/ModulesCycle.dfy.expect | 3 +- .../dafny0/NestedPatterns.dfy.expect | 3 +- .../dafny0/NonGhostQuantifiers.dfy.expect | 3 +- .../dafny0/ParallelResolveErrors.dfy.expect | 3 +- Test/allocated1/dafny0/ParseErrors.dfy.expect | 1 + .../RefinementModificationChecking.dfy.expect | 3 +- .../allocated1/dafny0/ReturnErrors.dfy.expect | 3 +- Test/allocated1/dafny0/Shadows.dfy.expect | 3 +- .../dafny0/TypeConstraints.dfy.expect | 3 +- .../dafny0/TypeInstantiations.dfy.expect | 3 +- Test/allocated1/dafny0/TypeTests.dfy.expect | 3 +- .../UserSpecifiedTypeParameters.dfy.expect | 3 +- Test/dafny4/git-issue16.dfy | 9 +++++ Test/dafny4/git-issue16.dfy.expect | 3 ++ Test/dafny4/git-issue16.dfyi | 3 ++ 36 files changed, 117 insertions(+), 52 deletions(-) create mode 100644 Test/dafny4/git-issue16.dfy create mode 100644 Test/dafny4/git-issue16.dfy.expect create mode 100644 Test/dafny4/git-issue16.dfyi diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 802b5c27848..e0ff84ef16d 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -85,12 +85,14 @@ public class Include : IComparable public readonly string includerFilename; public readonly string includedFilename; public readonly string includedFullPath; + public bool ErrorReported; public Include(IToken tok, string includer, string theFilename, string fullPath) { this.tok = tok; this.includerFilename = includer; this.includedFilename = theFilename; this.includedFullPath = fullPath; + this.ErrorReported = false; } public int CompareTo(object obj) { @@ -6755,7 +6757,7 @@ public int pos { get { return WrappedToken.pos; } set { throw new NotSupportedException(); } } - public string val { + public virtual string val { get { return WrappedToken.val; } set { throw new NotSupportedException(); } } @@ -6781,9 +6783,16 @@ public NestedToken(IToken outer, IToken inner) /// public class IncludeToken : TokenWrapper { - public IncludeToken(IToken wrappedToken) + public Include Include; + public IncludeToken(Include include, IToken wrappedToken) : base(wrappedToken) { Contract.Requires(wrappedToken != null); + this.Include = include; + } + + public override string val { + get { return WrappedToken.val; } + set { WrappedToken.val = value; } } } diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index dbbdfd9e7d4..3b11a3ac560 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -113,7 +113,7 @@ public static string Parse(IList files, string programName, ErrorRepo Console.WriteLine("Parsing " + dafnyFile.FilePath); } - string err = ParseFile(dafnyFile, Bpl.Token.NoToken, module, builtIns, new Errors(reporter)); + string err = ParseFile(dafnyFile, null, module, builtIns, new Errors(reporter)); if (err != null) { return err; } @@ -188,7 +188,7 @@ public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, IList -public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ { +public static int Parse (string/*!*/ filename, Include include, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ { Contract.Requires(filename != null); Contract.Requires(module != null); string s; if (filename == "stdin.dfy") { s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List()); - return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile); + return Parse(s, filename, filename, include, module, builtIns, errors, verifyThisFile); } else { using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { s = Microsoft.Boogie.ParserHelper.Fill(reader, new List()); - return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile); + return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, include, module, builtIns, errors, verifyThisFile); } } } @@ -240,7 +241,7 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi Contract.Requires(filename != null); Contract.Requires(module != null); Errors errors = new Errors(reporter); - return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile); + return Parse(s, fullFilename, filename, null, module, builtIns, errors, verifyThisFile); } /// /// Parses top-level things (modules, classes, datatypes, class members) @@ -248,7 +249,7 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner with the given Errors sink. /// -public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module, +public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, Include include, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) { Contract.Requires(s != null); Contract.Requires(filename != null); @@ -257,11 +258,11 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s)); MemoryStream ms = new MemoryStream(buffer,false); Scanner scanner = new Scanner(ms, errors, fullFilename, filename); - Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile); + Parser parser = new Parser(scanner, errors, include, module, builtIns, verifyThisFile); parser.Parse(); return parser.errors.ErrorCount; } -public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) +public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) : this(scanner, errors) // the real work { // initialize readonly fields @@ -269,6 +270,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyRhs = new ExprRhs(dummyExpr, null); dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null); dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null); + theInclude = include; // the "include" that includes this file theModule = module; theBuiltIns = builtIns; theVerifyThisFile = verifyThisFile; @@ -679,7 +681,7 @@ public void SemErr(IToken tok, string msg) { void Get () { for (;;) { - t = la; + t = theVerifyThisFile ? la : new IncludeToken(theInclude, la); la = scanner.Scan(); if (la.kind <= maxT) { ++errDist; break; } @@ -1089,10 +1091,10 @@ void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDec if (baseType == null) { baseType = new InferredTypeProxy(); } Expect(24); Expression(out wh, false, true); - td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); + td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); } else if (StartOf(6)) { Type(out baseType); - td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); + td = new NewtypeDecl(id, id.val, module, baseType, attrs); } else SynErr(161); } @@ -1134,7 +1136,7 @@ void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelD if (ty == null) { ty = new InferredTypeProxy(); } Expect(24); Expression(out constraint, false, true); - td = new SubsetTypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs); + td = new SubsetTypeDecl(id, id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs); kind = "Subset type"; } else if (StartOf(6)) { @@ -1665,7 +1667,7 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute"); } EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ true); - IToken tok = theVerifyThisFile ? id : new IncludeToken(id); + IToken tok = id; if (isTwoState && isPredicate) { f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals, reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis); @@ -1824,8 +1826,8 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } - - IToken tok = theVerifyThisFile ? id : new IncludeToken(id); + + IToken tok = id; if (isConstructor) { m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); @@ -2990,7 +2992,7 @@ void WhileStmt(out Statement stmt) { void MatchStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); - Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; + IToken x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; List cases = new List(); bool usesOptionalBraces = false; @@ -3080,7 +3082,7 @@ void ForallStmt(out Statement/*!*/ s) { void CalcStmt(out Statement s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); - Token x; + IToken x; Attributes attrs = null; CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp; var lines = new List(); diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 7f3bfe3f7a4..62df89bda62 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -37,7 +37,7 @@ protected ErrorReporter() { // This is the only thing that needs to be overriden public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set - (tok is TokenWrapper && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for nested and refinement + (tok is TokenWrapper && !(tok is IncludeToken) && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for included, nested and refinement if (!discard) { AllMessages[level].Add(new ErrorMessage { token = tok, message = msg }); } @@ -51,6 +51,16 @@ public int Count(ErrorLevel level) { public void Error(MessageSource source, IToken tok, string msg) { Contract.Requires(tok != null); Contract.Requires(msg != null); + // if the tok is IncludeToken, we need to indicate to the including file + // that there are errors in the included file. + if (tok is IncludeToken) { + IncludeToken includeToken = (IncludeToken) tok; + Include include = includeToken.Include; + if (!include.ErrorReported) { + Message(source, ErrorLevel.Error, include.tok, "the included file " + tok.filename + " contains error(s)"); + include.ErrorReported = true; + } + } Message(source, ErrorLevel.Error, tok, msg); } diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index d2910a3711f..ed26277bd29 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -50,7 +50,7 @@ public bool Verify() { private bool Parse() { Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); - var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, new Dafny.Errors(reporter)) == 0 && + var success = (Dafny.Parser.Parse(source, fname, fname, null, module, builtIns, new Dafny.Errors(reporter)) == 0 && Dafny.Main.ParseIncludes(module, builtIns, new List(), new Dafny.Errors(reporter)) == null); if (success) { dafnyProgram = new Dafny.Program(fname, module, builtIns, reporter); diff --git a/Test/allocated1/dafny0/AssumptionVariables0.dfy.expect b/Test/allocated1/dafny0/AssumptionVariables0.dfy.expect index 248c815c88a..486147dbbd5 100644 --- a/Test/allocated1/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/allocated1/dafny0/AssumptionVariables0.dfy.expect @@ -1,3 +1,4 @@ +AssumptionVariables0.dfy(3,8): Error: the included file AssumptionVariables0.dfy contains error(s) 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,26): Error: assumption variable must be of type 'bool' @@ -10,4 +11,4 @@ AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to a AssumptionVariables0.dfy(61,34): 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 && " AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost -12 resolution/type errors detected in AssumptionVariables0.dfy +13 resolution/type errors detected in AssumptionVariables0.dfy diff --git a/Test/allocated1/dafny0/BindingGuardsResolution.dfy.expect b/Test/allocated1/dafny0/BindingGuardsResolution.dfy.expect index 058031fd5b9..6a90156320f 100644 --- a/Test/allocated1/dafny0/BindingGuardsResolution.dfy.expect +++ b/Test/allocated1/dafny0/BindingGuardsResolution.dfy.expect @@ -154,6 +154,7 @@ module Ghost { b := exists y {:myattribute P(y)} :: 0 <= y < 100; } } +BindingGuardsResolution.dfy(3,8): Error: the included file BindingGuardsResolution.dfy contains error(s) BindingGuardsResolution.dfy(12,10): Error: Duplicate local-variable name: x BindingGuardsResolution.dfy(19,6): Error: LHS of assignment must denote a mutable variable BindingGuardsResolution.dfy(39,8): Error: Duplicate local-variable name: x @@ -165,4 +166,4 @@ BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is n BindingGuardsResolution.dfy(142,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) BindingGuardsResolution.dfy(146,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) BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -11 resolution/type errors detected in BindingGuardsResolution.dfy +12 resolution/type errors detected in BindingGuardsResolution.dfy diff --git a/Test/allocated1/dafny0/BitvectorResolution.dfy.expect b/Test/allocated1/dafny0/BitvectorResolution.dfy.expect index 7ddc7f28812..ec8d1b2b8b4 100644 --- a/Test/allocated1/dafny0/BitvectorResolution.dfy.expect +++ b/Test/allocated1/dafny0/BitvectorResolution.dfy.expect @@ -1,3 +1,4 @@ +BitvectorResolution.dfy(3,8): Error: the included file BitvectorResolution.dfy contains error(s) BitvectorResolution.dfy(9,13): Error: bitvector literal (5000) is too large for the type bv1 BitvectorResolution.dfy(15,9): Error: bitvector literal (1) is too large for the type bv0 BitvectorResolution.dfy(18,9): Error: bitvector literal (4294967296) is too large for the type bv32 @@ -11,4 +12,4 @@ BitvectorResolution.dfy(43,26): Error: type mismatch for argument 0 (function ex BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must be an integer-numeric or bitvector type BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type BitvectorResolution.dfy(110,19): Error: the type of this expression is underspecified -13 resolution/type errors detected in BitvectorResolution.dfy +14 resolution/type errors detected in BitvectorResolution.dfy diff --git a/Test/allocated1/dafny0/CallStmtTests.dfy.expect b/Test/allocated1/dafny0/CallStmtTests.dfy.expect index 93cfe895112..52b0b6edaf9 100644 --- a/Test/allocated1/dafny0/CallStmtTests.dfy.expect +++ b/Test/allocated1/dafny0/CallStmtTests.dfy.expect @@ -1,3 +1,4 @@ +CallStmtTests.dfy(3,8): Error: the included file CallStmtTests.dfy contains error(s) CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable -2 resolution/type errors detected in CallStmtTests.dfy +3 resolution/type errors detected in CallStmtTests.dfy diff --git a/Test/allocated1/dafny0/CoResolution.dfy.expect b/Test/allocated1/dafny0/CoResolution.dfy.expect index a64c31eba04..87fb4da49ee 100644 --- a/Test/allocated1/dafny0/CoResolution.dfy.expect +++ b/Test/allocated1/dafny0/CoResolution.dfy.expect @@ -1,3 +1,4 @@ +CoResolution.dfy(3,8): Error: the included file CoResolution.dfy contains error(s) CoResolution.dfy(18,11): Error: member Undeclared# does not exist in class TestClass CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared# CoResolution.dfy(22,9): Error: unresolved identifier: _k @@ -23,4 +24,4 @@ CoResolution.dfy(206,12): Error: type variable '_T0' in the function call to 'A' CoResolution.dfy(206,13): Error: the type of this expression is underspecified CoResolution.dfy(206,19): Error: type variable '_T0' in the function call to 'S' could not be determined CoResolution.dfy(206,20): Error: the type of this expression is underspecified -25 resolution/type errors detected in CoResolution.dfy +26 resolution/type errors detected in CoResolution.dfy diff --git a/Test/allocated1/dafny0/Coinductive.dfy.expect b/Test/allocated1/dafny0/Coinductive.dfy.expect index d69d1d53685..f3b7255af0f 100644 --- a/Test/allocated1/dafny0/Coinductive.dfy.expect +++ b/Test/allocated1/dafny0/Coinductive.dfy.expect @@ -1,3 +1,4 @@ +Coinductive.dfy(3,8): Error: the included file Coinductive.dfy contains error(s) 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 @@ -28,4 +29,4 @@ Coinductive.dfy(253,12): Error: an inductive predicate can be called recursively Coinductive.dfy(259,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier Coinductive.dfy(260,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier Coinductive.dfy(280,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates -30 resolution/type errors detected in Coinductive.dfy +31 resolution/type errors detected in Coinductive.dfy diff --git a/Test/allocated1/dafny0/DatatypeUpdateResolution.dfy.expect b/Test/allocated1/dafny0/DatatypeUpdateResolution.dfy.expect index 4852624b129..2368d32395f 100644 --- a/Test/allocated1/dafny0/DatatypeUpdateResolution.dfy.expect +++ b/Test/allocated1/dafny0/DatatypeUpdateResolution.dfy.expect @@ -1,5 +1,6 @@ +DatatypeUpdateResolution.dfy(3,8): Error: the included file DatatypeUpdateResolution.dfy contains error(s) DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType' DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType' DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool' DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor' -4 resolution/type errors detected in DatatypeUpdateResolution.dfy +5 resolution/type errors detected in DatatypeUpdateResolution.dfy diff --git a/Test/allocated1/dafny0/DiscoverBoundsErrors.dfy.expect b/Test/allocated1/dafny0/DiscoverBoundsErrors.dfy.expect index 5f1486ae98d..5561e212eec 100644 --- a/Test/allocated1/dafny0/DiscoverBoundsErrors.dfy.expect +++ b/Test/allocated1/dafny0/DiscoverBoundsErrors.dfy.expect @@ -1,4 +1,5 @@ +DiscoverBoundsErrors.dfy(3,8): Error: the included file DiscoverBoundsErrors.dfy contains error(s) DiscoverBoundsErrors.dfy(11,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'' DiscoverBoundsErrors.dfy(12,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r' DiscoverBoundsErrors.dfy(13,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r'' -3 resolution/type errors detected in DiscoverBoundsErrors.dfy +4 resolution/type errors detected in DiscoverBoundsErrors.dfy diff --git a/Test/allocated1/dafny0/DisplayExpressions.dfy.expect b/Test/allocated1/dafny0/DisplayExpressions.dfy.expect index 907e1522f84..15ba04f127e 100644 --- a/Test/allocated1/dafny0/DisplayExpressions.dfy.expect +++ b/Test/allocated1/dafny0/DisplayExpressions.dfy.expect @@ -1,3 +1,4 @@ +DisplayExpressions.dfy(3,8): Error: the included file DisplayExpressions.dfy contains error(s) DisplayExpressions.dfy(7,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(12,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(17,8): Error: the type of this variable is underspecified @@ -6,4 +7,4 @@ DisplayExpressions.dfy(27,14): Error: the type of this expression is underspecif DisplayExpressions.dfy(27,31): Error: the type of this expression is underspecified DisplayExpressions.dfy(42,6): Error: RHS (of type seq) not assignable to LHS (of type seq) (covariant type parameter would require byte <: int) DisplayExpressions.dfy(74,17): Error: arguments must have the same type (got seq and seq) -8 resolution/type errors detected in DisplayExpressions.dfy +9 resolution/type errors detected in DisplayExpressions.dfy diff --git a/Test/allocated1/dafny0/EqualityTypes.dfy.expect b/Test/allocated1/dafny0/EqualityTypes.dfy.expect index b204ec966f0..9e7aaf07fc7 100644 --- a/Test/allocated1/dafny0/EqualityTypes.dfy.expect +++ b/Test/allocated1/dafny0/EqualityTypes.dfy.expect @@ -1,3 +1,4 @@ +EqualityTypes.dfy(3,8): Error: the included file EqualityTypes.dfy contains error(s) EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype EqualityTypes.dfy(35,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality EqualityTypes.dfy(40,11): Error: opaque type 'X' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0) @@ -57,4 +58,4 @@ EqualityTypes.dfy(319,31): Error: type parameter 1 (X) passed to function H must EqualityTypes.dfy(321,41): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream) EqualityTypes.dfy(323,28): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream) EqualityTypes.dfy(326,48): Error: type parameter 1 (B) passed to method Q must support equality (got Stream) -59 resolution/type errors detected in EqualityTypes.dfy +60 resolution/type errors detected in EqualityTypes.dfy diff --git a/Test/allocated1/dafny0/ErrorsInRelatedModules.dfy.expect b/Test/allocated1/dafny0/ErrorsInRelatedModules.dfy.expect index 9d4ac6fbaf2..036bcf5dbbf 100644 --- a/Test/allocated1/dafny0/ErrorsInRelatedModules.dfy.expect +++ b/Test/allocated1/dafny0/ErrorsInRelatedModules.dfy.expect @@ -1,3 +1,4 @@ +ErrorsInRelatedModules.dfy(3,8): Error: the included file ErrorsInRelatedModules.dfy contains error(s) ErrorsInRelatedModules.dfy(9,29): Error: Undeclared top-level type or type parameter: UndeclaredType (did you forget to qualify a name or declare a module import 'opened?') ErrorsInRelatedModules.dfy(13,11): Error: not resolving module 'MainModule' because there were errors in resolving its import 'LibraryModule' ErrorsInRelatedModules.dfy(23,31): Error: Undeclared top-level type or type parameter: UndeclaredType (did you forget to qualify a name or declare a module import 'opened?') @@ -6,4 +7,4 @@ ErrorsInRelatedModules.dfy(34,29): Error: Undeclared top-level type or type para ErrorsInRelatedModules.dfy(34,29): Error: Undeclared top-level type or type parameter: UndeclaredType (did you forget to qualify a name or declare a module import 'opened?') ErrorsInRelatedModules.dfy(38,11): Error: not resolving module 'ClientModule' because there were errors in resolving its import 'T' ErrorsInRelatedModules.dfy(59,21): Error: module I does not exist (position 1 in path Middle.I) -8 resolution/type errors detected in ErrorsInRelatedModules.dfy +9 resolution/type errors detected in ErrorsInRelatedModules.dfy diff --git a/Test/allocated1/dafny0/Fuel.dfy.expect b/Test/allocated1/dafny0/Fuel.dfy.expect index b552189e93c..fab5d44e368 100644 --- a/Test/allocated1/dafny0/Fuel.dfy.expect +++ b/Test/allocated1/dafny0/Fuel.dfy.expect @@ -19,6 +19,7 @@ Execution trace: Fuel.dfy(94,22): Error: assertion violation Execution trace: (0,0): anon0 +Fuel.dfy(3,8): Error: the included file Fuel.dfy contains error(s) Fuel.dfy(129,8): Error: Fuel can only increase within a given scope. Fuel.dfy(120,22): Error: assertion violation Execution trace: diff --git a/Test/allocated1/dafny0/IMaps2.dfy.expect b/Test/allocated1/dafny0/IMaps2.dfy.expect index e1e1b8ba627..15e9e567eb1 100644 --- a/Test/allocated1/dafny0/IMaps2.dfy.expect +++ b/Test/allocated1/dafny0/IMaps2.dfy.expect @@ -1,2 +1,3 @@ +IMaps2.dfy(3,8): Error: the included file IMaps2.dfy contains error(s) IMaps2.dfy(7,3): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 's' -1 resolution/type errors detected in IMaps2.dfy +2 resolution/type errors detected in IMaps2.dfy diff --git a/Test/allocated1/dafny0/LiberalEquality.dfy.expect b/Test/allocated1/dafny0/LiberalEquality.dfy.expect index 2aafd59118e..ddb4a4a1b2a 100644 --- a/Test/allocated1/dafny0/LiberalEquality.dfy.expect +++ b/Test/allocated1/dafny0/LiberalEquality.dfy.expect @@ -1,3 +1,4 @@ +LiberalEquality.dfy(3,8): Error: the included file LiberalEquality.dfy contains error(s) LiberalEquality.dfy(22,14): Error: arguments must have the same type (got T and U) LiberalEquality.dfy(23,14): Error: arguments must have the same type (got U and int) LiberalEquality.dfy(31,14): Error: arguments must have the same type (got array and array3) @@ -13,4 +14,4 @@ LiberalEquality.dfy(84,13): Error: arguments must have the same type (got Syn> and array>) LiberalEquality.dfy(97,13): Error: arguments must have the same type (got array> and array>) LiberalEquality.dfy(103,13): Error: arguments must have the same type (got array> and array>>) -15 resolution/type errors detected in LiberalEquality.dfy +16 resolution/type errors detected in LiberalEquality.dfy diff --git a/Test/allocated1/dafny0/Modules0.dfy.expect b/Test/allocated1/dafny0/Modules0.dfy.expect index a585d8e9aa8..0757f1af1a7 100644 --- a/Test/allocated1/dafny0/Modules0.dfy.expect +++ b/Test/allocated1/dafny0/Modules0.dfy.expect @@ -1,5 +1,6 @@ Modules0.dfy(333,2): Warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here Modules0.dfy(335,2): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Modules0.dfy(3,8): Error: the included file Modules0.dfy contains error(s) 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 @@ -32,4 +33,4 @@ Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_I Modules0.dfy(324,30): Error: member Create does not exist in class Klassy Modules0.dfy(318,13): Error: arguments must have the same type (got Q_Imp.Node and Node) Modules0.dfy(348,11): Error: a datatype declaration (T) in a refinement module can only replace an opaque type declaration -32 resolution/type errors detected in Modules0.dfy +33 resolution/type errors detected in Modules0.dfy diff --git a/Test/allocated1/dafny0/Modules2.dfy.expect b/Test/allocated1/dafny0/Modules2.dfy.expect index 068532b9a0a..2e5f71b5ab9 100644 --- a/Test/allocated1/dafny0/Modules2.dfy.expect +++ b/Test/allocated1/dafny0/Modules2.dfy.expect @@ -1,6 +1,7 @@ +Modules2.dfy(3,8): Error: the included file Modules2.dfy contains error(s) 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 (try qualifying the type name with the module name) Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B (try qualifying the member name with the module name) -5 resolution/type errors detected in Modules2.dfy +6 resolution/type errors detected in Modules2.dfy diff --git a/Test/allocated1/dafny0/ModulesCycle.dfy.expect b/Test/allocated1/dafny0/ModulesCycle.dfy.expect index dbe8fb3f3f5..e50ad278165 100644 --- a/Test/allocated1/dafny0/ModulesCycle.dfy.expect +++ b/Test/allocated1/dafny0/ModulesCycle.dfy.expect @@ -1,3 +1,4 @@ +ModulesCycle.dfy(3,8): Error: the included file ModulesCycle.dfy contains error(s) 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 +3 resolution/type errors detected in ModulesCycle.dfy diff --git a/Test/allocated1/dafny0/NestedPatterns.dfy.expect b/Test/allocated1/dafny0/NestedPatterns.dfy.expect index e9dfc79024f..90e421a0b24 100644 --- a/Test/allocated1/dafny0/NestedPatterns.dfy.expect +++ b/Test/allocated1/dafny0/NestedPatterns.dfy.expect @@ -1,3 +1,4 @@ +NestedPatterns.dfy(3,8): Error: the included file NestedPatterns.dfy contains error(s) NestedPatterns.dfy(69,2): Error: member Cons appears in more than one case NestedPatterns.dfy(75,2): Error: member does not exist in datatype List NestedPatterns.dfy(76,2): Error: member does not exist in datatype List @@ -6,4 +7,4 @@ NestedPatterns.dfy(92,20): Error: Duplicate parameter name: h NestedPatterns.dfy(100,23): Error: Duplicate parameter name: e NestedPatterns.dfy(116,2): Error: case arguments count does not match source arguments count NestedPatterns.dfy(122,2): Error: match source tuple needs at least 1 argument -8 resolution/type errors detected in NestedPatterns.dfy +9 resolution/type errors detected in NestedPatterns.dfy diff --git a/Test/allocated1/dafny0/NonGhostQuantifiers.dfy.expect b/Test/allocated1/dafny0/NonGhostQuantifiers.dfy.expect index d08400acbea..8f9fe4b7d4b 100644 --- a/Test/allocated1/dafny0/NonGhostQuantifiers.dfy.expect +++ b/Test/allocated1/dafny0/NonGhostQuantifiers.dfy.expect @@ -1,3 +1,4 @@ +NonGhostQuantifiers.dfy(3,8): Error: the included file NonGhostQuantifiers.dfy contains error(s) NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile 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 or compile 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 or compile a bounded set of values for 'd' @@ -14,4 +15,4 @@ NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function defin 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(192,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'c' -16 resolution/type errors detected in NonGhostQuantifiers.dfy +17 resolution/type errors detected in NonGhostQuantifiers.dfy diff --git a/Test/allocated1/dafny0/ParallelResolveErrors.dfy.expect b/Test/allocated1/dafny0/ParallelResolveErrors.dfy.expect index 821ffe53a74..c03e8f4efbd 100644 --- a/Test/allocated1/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/allocated1/dafny0/ParallelResolveErrors.dfy.expect @@ -1,3 +1,4 @@ +ParallelResolveErrors.dfy(3,8): Error: the included file ParallelResolveErrors.dfy contains error(s) ParallelResolveErrors.dfy(20,4): Error: LHS of assignment must denote a mutable variable ParallelResolveErrors.dfy(25,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement ParallelResolveErrors.dfy(42,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement @@ -20,4 +21,4 @@ ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing forall statem ParallelResolveErrors.dfy(114,29): 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(119,29): 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(129,11): 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) -22 resolution/type errors detected in ParallelResolveErrors.dfy +23 resolution/type errors detected in ParallelResolveErrors.dfy diff --git a/Test/allocated1/dafny0/ParseErrors.dfy.expect b/Test/allocated1/dafny0/ParseErrors.dfy.expect index a472b30b5c7..6a48b916ab2 100644 --- a/Test/allocated1/dafny0/ParseErrors.dfy.expect +++ b/Test/allocated1/dafny0/ParseErrors.dfy.expect @@ -1,3 +1,4 @@ +ParseErrors.dfy(3,8): Error: the included file ParseErrors.dfy contains error(s) ParseErrors.dfy(7,18): Error: a chain cannot have more than one != operator ParseErrors.dfy(9,36): Error: this operator chain cannot continue with a descending operator ParseErrors.dfy(10,37): Error: this operator chain cannot continue with an ascending operator diff --git a/Test/allocated1/dafny0/RefinementModificationChecking.dfy.expect b/Test/allocated1/dafny0/RefinementModificationChecking.dfy.expect index d2457fbcb04..3929fba2c23 100644 --- a/Test/allocated1/dafny0/RefinementModificationChecking.dfy.expect +++ b/Test/allocated1/dafny0/RefinementModificationChecking.dfy.expect @@ -1,6 +1,7 @@ +RefinementModificationChecking.dfy(3,8): Error: the included file RefinementModificationChecking.dfy contains error(s) RefinementModificationChecking.dfy(22,6): Error: refinement method cannot assign to variable defined in parent module ('t') RefinementModificationChecking.dfy(23,6): Error: refinement method cannot assign to variable defined in parent module ('r') RefinementModificationChecking.dfy(24,6): Error: refinement method cannot assign to a field defined in parent module ('f') RefinementModificationChecking.dfy(51,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state RefinementModificationChecking.dfy(53,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements) -5 resolution/type errors detected in RefinementModificationChecking.dfy +6 resolution/type errors detected in RefinementModificationChecking.dfy diff --git a/Test/allocated1/dafny0/ReturnErrors.dfy.expect b/Test/allocated1/dafny0/ReturnErrors.dfy.expect index c782489def6..db10c4ddc06 100644 --- a/Test/allocated1/dafny0/ReturnErrors.dfy.expect +++ b/Test/allocated1/dafny0/ReturnErrors.dfy.expect @@ -1,4 +1,5 @@ +ReturnErrors.dfy(3,8): Error: the included file ReturnErrors.dfy contains error(s) ReturnErrors.dfy(32,11): Error: cannot have method call in return statement. ReturnErrors.dfy(38,11): 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 +4 resolution/type errors detected in ReturnErrors.dfy diff --git a/Test/allocated1/dafny0/Shadows.dfy.expect b/Test/allocated1/dafny0/Shadows.dfy.expect index 2a18c8dd164..1e2d1b7cd90 100644 --- a/Test/allocated1/dafny0/Shadows.dfy.expect +++ b/Test/allocated1/dafny0/Shadows.dfy.expect @@ -1,3 +1,4 @@ +Shadows.dfy(3,8): Error: the included file Shadows.dfy contains error(s) Shadows.dfy(6,19): Error: Duplicate type-parameter name: beta Shadows.dfy(7,13): Warning: Shadowed type-parameter name: alpha Shadows.dfy(8,21): Error: Duplicate type-parameter name: beta @@ -9,4 +10,4 @@ Shadows.dfy(26,10): Error: Duplicate local-variable name: f Shadows.dfy(32,12): Warning: Shadowed local-variable name: x Shadows.dfy(38,28): Warning: Shadowed bound-variable name: x Shadows.dfy(39,40): Warning: Shadowed bound-variable name: y -5 resolution/type errors detected in Shadows.dfy +6 resolution/type errors detected in Shadows.dfy diff --git a/Test/allocated1/dafny0/TypeConstraints.dfy.expect b/Test/allocated1/dafny0/TypeConstraints.dfy.expect index f691c9c53bc..cbecedd4d42 100644 --- a/Test/allocated1/dafny0/TypeConstraints.dfy.expect +++ b/Test/allocated1/dafny0/TypeConstraints.dfy.expect @@ -1,3 +1,4 @@ +TypeConstraints.dfy(3,8): Error: the included file TypeConstraints.dfy contains error(s) TypeConstraints.dfy(42,6): Error: RHS (of type int) not assignable to LHS (of type bool) TypeConstraints.dfy(50,6): Error: RHS (of type bool) not assignable to LHS (of type int) TypeConstraints.dfy(58,6): Error: RHS (of type int) not assignable to LHS (of type bool) @@ -589,4 +590,4 @@ module Arrays_and_SubsetTypes { } } } -18 resolution/type errors detected in TypeConstraints.dfy +19 resolution/type errors detected in TypeConstraints.dfy diff --git a/Test/allocated1/dafny0/TypeInstantiations.dfy.expect b/Test/allocated1/dafny0/TypeInstantiations.dfy.expect index 04fd56de660..874270cdab9 100644 --- a/Test/allocated1/dafny0/TypeInstantiations.dfy.expect +++ b/Test/allocated1/dafny0/TypeInstantiations.dfy.expect @@ -1,3 +1,4 @@ +TypeInstantiations.dfy(3,8): Error: the included file TypeInstantiations.dfy contains error(s) TypeInstantiations.dfy(33,7): Error: an opaque type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base TypeInstantiations.dfy(36,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype TypeInstantiations.dfy(40,7): Error: opaque type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0) @@ -10,4 +11,4 @@ TypeInstantiations.dfy(56,7): Error: type 'TP1' is not allowed to change its num TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an opaque type with equality support, but 'C' does not support equality TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an opaque type with equality support, but 'D' does not support equality TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an opaque type with equality support, but 'N' does not support equality -12 resolution/type errors detected in TypeInstantiations.dfy +13 resolution/type errors detected in TypeInstantiations.dfy diff --git a/Test/allocated1/dafny0/TypeTests.dfy.expect b/Test/allocated1/dafny0/TypeTests.dfy.expect index aa24d8f1272..644dfd3aa8c 100644 --- a/Test/allocated1/dafny0/TypeTests.dfy.expect +++ b/Test/allocated1/dafny0/TypeTests.dfy.expect @@ -1,3 +1,4 @@ +TypeTests.dfy(3,8): Error: the included file TypeTests.dfy contains error(s) TypeTests.dfy(9,17): Error: type mismatch for argument 0 (function expects C, got D) TypeTests.dfy(9,20): Error: type mismatch for argument 1 (function expects D, got C) TypeTests.dfy(10,15): Error: type mismatch for argument 0 (function expects C, got int) @@ -30,4 +31,4 @@ TypeTests.dfy(198,15): Error: incorrect type of datatype constructor argument (f TypeTests.dfy(204,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt) (covariant type parameter 1 would require Dt <: ?) TypeTests.dfy(211,6): Error: RHS (of type set) not assignable to LHS (of type ?) TypeTests.dfy(222,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) -32 resolution/type errors detected in TypeTests.dfy +33 resolution/type errors detected in TypeTests.dfy diff --git a/Test/allocated1/dafny0/UserSpecifiedTypeParameters.dfy.expect b/Test/allocated1/dafny0/UserSpecifiedTypeParameters.dfy.expect index ebe8a8f7b12..fa0d147158a 100644 --- a/Test/allocated1/dafny0/UserSpecifiedTypeParameters.dfy.expect +++ b/Test/allocated1/dafny0/UserSpecifiedTypeParameters.dfy.expect @@ -1,3 +1,4 @@ +UserSpecifiedTypeParameters.dfy(3,8): Error: the included file UserSpecifiedTypeParameters.dfy contains error(s) UserSpecifiedTypeParameters.dfy(27,12): Error: the type of this variable is underspecified UserSpecifiedTypeParameters.dfy(27,26): Error: type variable 'T' in the function call to 'H' could not be determined UserSpecifiedTypeParameters.dfy(27,26): Error: type variable 'U' in the function call to 'H' could not be determined @@ -8,4 +9,4 @@ UserSpecifiedTypeParameters.dfy(48,30): Error: non-function expression (of type UserSpecifiedTypeParameters.dfy(48,16): Error: wrong number of arguments to function application (function 'F' expects 2, got 1) UserSpecifiedTypeParameters.dfy(79,15): Error: incorrect type of method in-parameter 0 (expected A, got int) UserSpecifiedTypeParameters.dfy(91,15): Error: type mismatch for argument 0 (function expects A, got int) -10 resolution/type errors detected in UserSpecifiedTypeParameters.dfy +11 resolution/type errors detected in UserSpecifiedTypeParameters.dfy diff --git a/Test/dafny4/git-issue16.dfy b/Test/dafny4/git-issue16.dfy new file mode 100644 index 00000000000..5f8b8ca355b --- /dev/null +++ b/Test/dafny4/git-issue16.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "git-issue16.dfyi" + +lemma UhOh() + ensures false +{ +} diff --git a/Test/dafny4/git-issue16.dfy.expect b/Test/dafny4/git-issue16.dfy.expect new file mode 100644 index 00000000000..2a217160859 --- /dev/null +++ b/Test/dafny4/git-issue16.dfy.expect @@ -0,0 +1,3 @@ +git-issue16.dfy(4,8): Error: the included file git-issue16.dfyi contains error(s) +git-issue16.dfyi(2,5): Error: arguments must have the same type (got int and bool) +2 resolution/type errors detected in git-issue16.dfy diff --git a/Test/dafny4/git-issue16.dfyi b/Test/dafny4/git-issue16.dfyi new file mode 100644 index 00000000000..a104256d12e --- /dev/null +++ b/Test/dafny4/git-issue16.dfyi @@ -0,0 +1,3 @@ +predicate Problem() { + 1 == false +}