From 17405efd598d2a8a2dac304ee9a7f7d9bd30a558 Mon Sep 17 00:00:00 2001 From: "Richard L. Ford" Date: Wed, 27 Jan 2016 14:09:16 -0800 Subject: Implement 'extern' declaration modifier. The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed. --- Test/dafny0/Extern.dfy.expect | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 Test/dafny0/Extern.dfy.expect (limited to 'Test/dafny0/Extern.dfy.expect') diff --git a/Test/dafny0/Extern.dfy.expect b/Test/dafny0/Extern.dfy.expect new file mode 100644 index 00000000..fec087d9 --- /dev/null +++ b/Test/dafny0/Extern.dfy.expect @@ -0,0 +1,4 @@ + +Dafny program verifier finished with 7 verified, 0 errors +Compiled program written to D:\de\dafny\Test\dafny0\Extern.cs +Compiled assembly into Extern.exe -- cgit v1.2.3 From 348beb7f706f35256f5fb07349182e252aae8860 Mon Sep 17 00:00:00 2001 From: "Richard L. Ford" Date: Wed, 27 Jan 2016 16:43:01 -0800 Subject: Fix build and test failures, cleanup grammar. 1. A build failure caused by a method call before a contract was fixed. 2. An absolute path in an ".expect" file was changed to relative. 3. I eliminated the TopDecls and DeclModifiers non-terminals. They were giving a warning from Coco/R about being deletable. Instead I used repetition of the TopDecl or DeclModifier non-terminals where they had been used. I think this is also cleaner to talk about. --- Source/Dafny/Dafny.atg | 33 ++- Source/Dafny/Parser.cs | 472 +++++++++++++++++++------------------- Source/DafnyDriver/DafnyDriver.cs | 5 +- Test/dafny0/Extern.dfy.expect | 2 +- 4 files changed, 258 insertions(+), 254 deletions(-) (limited to 'Test/dafny0/Extern.dfy.expect') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 87e75541..eb0c3303 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -640,7 +640,7 @@ Dafny } .) } - TopDecls + { TopDecl } (. // find the default class in the default module, then append membersDefaultClass to its member list DefaultClassDecl defaultClass = null; foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { @@ -657,13 +657,8 @@ Dafny EOF . -TopDecls<. ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract .> -= { TopDecl } - . - -DeclModifiers -= (. dmod = new DeclModifierData(); .) - { "abstract" (. dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); .) +DeclModifier += ( "abstract" (. dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); .) | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); .) | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); .) | "protected" (. dmod.IsProtected = true; CheckAndSetToken(ref dmod.ProtectedToken); .) @@ -673,15 +668,15 @@ DeclModifiers dmod.ExternName = new StringLiteralExpr(t, s, isVerbatimString); .) ] - } + ) . TopDecl<. ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract .> -= (. DeclModifierData dmod; ModuleDecl submodule; += (. DeclModifierData dmod = new DeclModifierData(); ModuleDecl submodule; ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; TraitDecl/*!*/ trait; .) - DeclModifiers + { DeclModifier } ( SubModuleDecl (. module.TopLevelDecls.Add(submodule); .) | ClassDecl (. module.TopLevelDecls.Add(c); .) | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) @@ -713,7 +708,7 @@ SubModuleDecl (. isExclusively = false; .) ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); .) "{" (. module.BodyStartTok = t; .) - TopDecls + { TopDecl } "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); .) @@ -773,7 +768,9 @@ ClassDecl (. traits.Add(trait); .) } ] "{" (. bodyStart = t; .) - { DeclModifiers ClassMemberDecl + { (. dmod = new DeclModifierData(); .) + { DeclModifier } + ClassMemberDecl } "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -784,8 +781,8 @@ ClassDecl = (. Contract.Requires(module != null); - CheckDeclModifiers(dmodIn, "Traits", AllowedDeclModifiers.None); Contract.Ensures(Contract.ValueAtReturn(out trait) != null); + CheckDeclModifiers(dmodIn, "Traits", AllowedDeclModifiers.None); IToken/*!*/ id; Attributes attrs = null; List typeArgs = new List(); //traits should not support type parameters at the moment @@ -798,9 +795,11 @@ TraitDecl } NoUSIdent [ GenericParameters ] - "{" (. bodyStart = t; .) - { DeclModifiers ClassMemberDecl - } + "{" (. bodyStart = t; .) + { (. dmod = new DeclModifierData(); .) + { DeclModifier } + ClassMemberDecl + } "}" (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); trait.BodyStartTok = bodyStart; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index dc661fc5..943e2cf6 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -670,7 +670,9 @@ bool IsType(ref IToken pt) { } } - TopDecls(defaultModule, membersDefaultClass, /* isTopLevel */ true, /* isAbstract */ false); + while (StartOf(1)) { + TopDecl(defaultModule, membersDefaultClass, /* isTopLevel */ true, /* isAbstract */ false); + } DefaultClassDecl defaultClass = null; foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { defaultClass = topleveldecl as DefaultClassDecl; @@ -686,18 +688,14 @@ bool IsType(ref IToken pt) { Expect(0); } - void TopDecls(ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract ) { - while (StartOf(1)) { - TopDecl(module, membersDefaultClass, isTopLevel, isAbstract); - } - } - void TopDecl(ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract ) { - DeclModifierData dmod; ModuleDecl submodule; + DeclModifierData dmod = new DeclModifierData(); ModuleDecl submodule; ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; TraitDecl/*!*/ trait; - DeclModifiers(out dmod); + while (StartOf(2)) { + DeclModifier(ref dmod); + } switch (la.kind) { case 66: case 69: { SubModuleDecl(dmod, module, out submodule); @@ -743,33 +741,30 @@ bool IsType(ref IToken pt) { } } - void DeclModifiers(out DeclModifierData dmod) { - dmod = new DeclModifierData(); - while (StartOf(2)) { - if (la.kind == 61) { - Get(); - dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); - } else if (la.kind == 62) { - Get(); - dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); - } else if (la.kind == 63) { - Get(); - dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); - } else if (la.kind == 64) { - Get(); - dmod.IsProtected = true; CheckAndSetToken(ref dmod.ProtectedToken); - } else { + void DeclModifier(ref DeclModifierData dmod) { + if (la.kind == 61) { + Get(); + dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); + } else if (la.kind == 62) { + Get(); + dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); + } else if (la.kind == 63) { + Get(); + dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); + } else if (la.kind == 64) { + Get(); + dmod.IsProtected = true; CheckAndSetToken(ref dmod.ProtectedToken); + } else if (la.kind == 65) { + Get(); + dmod.IsExtern = true; CheckAndSetToken(ref dmod.ExternToken); + if (la.kind == 20) { Get(); - dmod.IsExtern = true; CheckAndSetToken(ref dmod.ExternToken); - if (la.kind == 20) { - Get(); - bool isVerbatimString; - string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString); - dmod.ExternName = new StringLiteralExpr(t, s, isVerbatimString); - - } + bool isVerbatimString; + string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString); + dmod.ExternName = new StringLiteralExpr(t, s, isVerbatimString); + } - } + } else SynErr(141); } void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDecl submodule) { @@ -805,7 +800,9 @@ bool IsType(ref IToken pt) { module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); Expect(46); module.BodyStartTok = t; - TopDecls(module, namedModuleDefaultClassMembers, /* isTopLevel */ false, isAbstract); + while (StartOf(1)) { + TopDecl(module, namedModuleDefaultClassMembers, /* isTopLevel */ false, isAbstract); + } Expect(47); module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); @@ -834,7 +831,7 @@ bool IsType(ref IToken pt) { } } if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(141); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(142); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -844,7 +841,7 @@ bool IsType(ref IToken pt) { submodule = new AliasModuleDecl(idPath, id, parent, opened); } - } else SynErr(142); + } else SynErr(143); } void ClassDecl(DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { @@ -860,7 +857,7 @@ bool IsType(ref IToken pt) { CheckDeclModifiers(dmodClass, "Classes", AllowedDeclModifiers.Extern); DeclModifierData dmod; - while (!(la.kind == 0 || la.kind == 74)) {SynErr(143); Get();} + while (!(la.kind == 0 || la.kind == 74)) {SynErr(144); Get();} Expect(74); while (la.kind == 46) { Attribute(ref attrs); @@ -883,7 +880,10 @@ bool IsType(ref IToken pt) { Expect(46); bodyStart = t; while (StartOf(3)) { - DeclModifiers(out dmod); + dmod = new DeclModifierData(); + while (StartOf(2)) { + DeclModifier(ref dmod); + } ClassMemberDecl(dmod, members, true, false, false); } Expect(47); @@ -904,13 +904,13 @@ bool IsType(ref IToken pt) { bool co = false; CheckDeclModifiers(dmod, "Datatypes or codatatypes", AllowedDeclModifiers.None); - while (!(la.kind == 0 || la.kind == 77 || la.kind == 78)) {SynErr(144); Get();} + while (!(la.kind == 0 || la.kind == 77 || la.kind == 78)) {SynErr(145); Get();} if (la.kind == 77) { Get(); } else if (la.kind == 78) { Get(); co = true; - } else SynErr(145); + } else SynErr(146); while (la.kind == 46) { Attribute(ref attrs); } @@ -926,7 +926,7 @@ bool IsType(ref IToken pt) { DatatypeMemberDecl(ctors); } if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(146); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(147); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -967,7 +967,7 @@ bool IsType(ref IToken pt) { } else if (StartOf(4)) { Type(out baseType); td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); - } else SynErr(147); + } else SynErr(148); } void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td) { @@ -1001,13 +1001,13 @@ bool IsType(ref IToken pt) { Type(out ty); td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); } - } else SynErr(148); + } else SynErr(149); if (td == null) { td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs); } if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(149); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(150); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -1037,7 +1037,7 @@ bool IsType(ref IToken pt) { IToken bodyEnd = Token.NoToken; CheckDeclModifiers(dmod, "Iterators", AllowedDeclModifiers.None); - while (!(la.kind == 0 || la.kind == 82)) {SynErr(150); Get();} + while (!(la.kind == 0 || la.kind == 82)) {SynErr(151); Get();} Expect(82); while (la.kind == 46) { Attribute(ref attrs); @@ -1060,7 +1060,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(151); + } else SynErr(152); while (StartOf(6)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } @@ -1089,7 +1089,7 @@ bool IsType(ref IToken pt) { IToken bodyStart; DeclModifierData dmod; - while (!(la.kind == 0 || la.kind == 76)) {SynErr(152); Get();} + while (!(la.kind == 0 || la.kind == 76)) {SynErr(153); Get();} Expect(76); while (la.kind == 46) { Attribute(ref attrs); @@ -1101,7 +1101,10 @@ bool IsType(ref IToken pt) { Expect(46); bodyStart = t; while (StartOf(3)) { - DeclModifiers(out dmod); + dmod = new DeclModifierData(); + while (StartOf(2)) { + DeclModifier(ref dmod); + } ClassMemberDecl(dmod, members, true, false, false); } Expect(47); @@ -1139,7 +1142,7 @@ bool IsType(ref IToken pt) { MethodDecl(dmod, allowConstructors, isWithinAbstractModule, out m); mm.Add(m); - } else SynErr(153); + } else SynErr(154); } void Attribute(ref Attributes attrs) { @@ -1225,7 +1228,7 @@ bool IsType(ref IToken pt) { IToken/*!*/ id; Type/*!*/ ty; CheckDeclModifiers(dmod, "Fields", AllowedDeclModifiers.Ghost); - while (!(la.kind == 0 || la.kind == 79)) {SynErr(154); Get();} + while (!(la.kind == 0 || la.kind == 79)) {SynErr(155); Get();} Expect(79); while (la.kind == 46) { Attribute(ref attrs); @@ -1287,7 +1290,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(155); + } else SynErr(156); } else if (la.kind == 39) { Get(); isPredicate = true; @@ -1324,7 +1327,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(156); + } else SynErr(157); } else if (la.kind == 40) { Get(); Expect(39); @@ -1348,7 +1351,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(157); + } else SynErr(158); } else if (la.kind == 42) { Get(); isCoPredicate = true; @@ -1371,8 +1374,8 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(158); - } else SynErr(159); + } else SynErr(159); + } else SynErr(160); decreases = isIndPredicate || isCoPredicate ? null : new List(); while (StartOf(10)) { FunctionSpec(reqs, reads, ens, decreases); @@ -1434,7 +1437,7 @@ bool IsType(ref IToken pt) { AllowedDeclModifiers allowed = AllowedDeclModifiers.None; string caption = ""; - while (!(StartOf(11))) {SynErr(160); Get();} + while (!(StartOf(11))) {SynErr(161); Get();} switch (la.kind) { case 85: { Get(); @@ -1485,7 +1488,7 @@ bool IsType(ref IToken pt) { break; } - default: SynErr(161); break; + default: SynErr(162); break; } keywordToken = t; CheckDeclModifiers(dmod, caption, allowed); @@ -1517,7 +1520,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(162); + } else SynErr(163); while (StartOf(12)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } @@ -1590,14 +1593,14 @@ bool IsType(ref IToken pt) { } else if (la.kind == 2) { Get(); id = t; - } else SynErr(163); + } else SynErr(164); Expect(21); Type(out ty); } void OldSemi() { if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(164); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(165); Get();} Get(); } } @@ -1694,7 +1697,7 @@ bool IsType(ref IToken pt) { id = t; name = id.val; Expect(21); Type(out ty); - } else SynErr(165); + } else SynErr(166); if (name != null) { identName = name; } else { @@ -1882,7 +1885,7 @@ bool IsType(ref IToken pt) { ty = new UserDefinedType(e.tok, e); break; } - default: SynErr(166); break; + default: SynErr(167); break; } if (la.kind == 30) { Type t2; @@ -1921,7 +1924,7 @@ List/*!*/ yieldReq, List/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; - while (!(StartOf(14))) {SynErr(167); Get();} + while (!(StartOf(14))) {SynErr(168); Get();} if (la.kind == 44) { Get(); while (IsAttribute()) { @@ -1982,7 +1985,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } - } else SynErr(168); + } else SynErr(169); } else if (la.kind == 36) { Get(); while (IsAttribute()) { @@ -1990,7 +1993,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(169); + } else SynErr(170); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -2012,7 +2015,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; - while (!(StartOf(17))) {SynErr(170); Get();} + while (!(StartOf(17))) {SynErr(171); Get();} if (la.kind == 43) { Get(); while (IsAttribute()) { @@ -2046,7 +2049,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false, false); OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(171); + } else SynErr(172); } else if (la.kind == 36) { Get(); while (IsAttribute()) { @@ -2054,7 +2057,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, true, false); OldSemi(); - } else SynErr(172); + } else SynErr(173); } void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) { @@ -2078,7 +2081,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id); fieldName = id.val; fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); - } else SynErr(173); + } else SynErr(174); } void DecreasesList(List decreases, bool allowWildcard, bool allowLambda) { @@ -2133,7 +2136,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - while (!(StartOf(18))) {SynErr(174); Get();} + while (!(StartOf(18))) {SynErr(175); Get();} if (la.kind == 45) { Get(); Expression(out e, false, false); @@ -2163,7 +2166,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(175); + } else SynErr(176); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -2182,7 +2185,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(19)) { FrameExpression(out fe, allowSemi, false); - } else SynErr(176); + } else SynErr(177); } void PossiblyWildExpression(out Expression e, bool allowLambda) { @@ -2193,7 +2196,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t); } else if (StartOf(8)) { Expression(out e, false, allowLambda); - } else SynErr(177); + } else SynErr(178); } void Stmt(List/*!*/ ss) { @@ -2210,7 +2213,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(20))) {SynErr(178); Get();} + while (!(StartOf(20))) {SynErr(179); Get();} switch (la.kind) { case 46: { BlockStmt(out bs, out bodyStart, out bodyEnd); @@ -2281,8 +2284,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); breakCount++; } - } else SynErr(179); - while (!(la.kind == 0 || la.kind == 28)) {SynErr(180); Get();} + } else SynErr(180); + while (!(la.kind == 0 || la.kind == 28)) {SynErr(181); Get();} Expect(28); s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); break; @@ -2295,7 +2298,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo SkeletonStmt(out s); break; } - default: SynErr(181); break; + default: SynErr(182); break; } } @@ -2314,7 +2317,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 59) { Get(); dotdotdot = t; - } else SynErr(182); + } else SynErr(183); Expect(28); if (dotdotdot != null) { s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null); @@ -2339,7 +2342,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 59) { Get(); dotdotdot = t; - } else SynErr(183); + } else SynErr(184); Expect(28); if (dotdotdot != null) { s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null); @@ -2409,13 +2412,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo suchThatAssume = t; } Expression(out suchThat, false, true); - } else SynErr(184); + } else SynErr(185); Expect(28); endTok = t; } else if (la.kind == 21) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(185); + } else SynErr(186); if (suchThat != null) { s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume, null); } else { @@ -2484,7 +2487,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out suchThat, false, true); } } - while (!(la.kind == 0 || la.kind == 28)) {SynErr(186); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(187); Get();} Expect(28); endTok = t; ConcreteUpdateStatement update; @@ -2538,12 +2541,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(25); SemErr(pat.tok, "LHS of assign-such-that expression must be variables, not general patterns"); - } else SynErr(187); + } else SynErr(188); Expression(out e, false, true); letRHSs.Add(e); Expect(28); s = new LetStmt(e.tok, e.tok, letLHSs, letRHSs); - } else SynErr(188); + } else SynErr(189); } void IfStmt(out Statement/*!*/ ifStmt) { @@ -2582,7 +2585,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 46) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; endTok = bs.EndTok; - } else SynErr(189); + } else SynErr(190); } if (guardEllipsis != null) { ifStmt = new SkeletonStatement(new IfStmt(x, endTok, isExistentialGuard, guard, thn, els), guardEllipsis, null); @@ -2590,7 +2593,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ifStmt = new IfStmt(x, endTok, isExistentialGuard, guard, thn, els); } - } else SynErr(190); + } else SynErr(191); } void WhileStmt(out Statement stmt) { @@ -2635,7 +2638,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(59); bodyEllipsis = t; endTok = t; isDirtyLoop = false; } else if (StartOf(24)) { - } else SynErr(191); + } else SynErr(192); if (guardEllipsis != null || bodyEllipsis != null) { if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); @@ -2653,7 +2656,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, endTok, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } - } else SynErr(192); + } else SynErr(193); } void MatchStmt(out Statement/*!*/ s) { @@ -2678,7 +2681,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseStatement(out c); cases.Add(c); } - } else SynErr(193); + } else SynErr(194); s = new MatchStmt(x, t, e, cases, usesOptionalBrace); } @@ -2703,7 +2706,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)"); - } else SynErr(194); + } else SynErr(195); if (la.kind == _openparen) { Expect(50); if (la.kind == 1) { @@ -2714,7 +2717,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == _ident) { QuantifierDomain(out bvars, out attrs, out range); } - } else SynErr(195); + } else SynErr(196); if (bvars == null) { bvars = new List(); } if (range == null) { range = new LiteralExpr(x, true); } @@ -2804,7 +2807,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 32) { CalcStmt(out subCalc); hintEnd = subCalc.EndTok; subhints.Add(subCalc); - } else SynErr(196); + } else SynErr(197); } var h = new BlockStmt(hintStart, hintEnd, subhints); // if the hint is empty, hintStart is the first token of the next line, but it doesn't matter because the block statement is just used as a container hints.Add(h); @@ -2846,14 +2849,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 59) { Get(); ellipsisToken = t; - } else SynErr(197); + } else SynErr(198); if (la.kind == 46) { BlockStmt(out body, out bodyStart, out endTok); } else if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(198); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(199); Get();} Get(); endTok = t; - } else SynErr(199); + } else SynErr(200); s = new ModifyStmt(tok, endTok, mod, attrs, body); if (ellipsisToken != null) { s = new SkeletonStatement(s, ellipsisToken, null); @@ -2873,7 +2876,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 91) { Get(); returnTok = t; isYield = true; - } else SynErr(200); + } else SynErr(201); if (StartOf(27)) { Rhs(out r); rhss = new List(); rhss.Add(r); @@ -2971,7 +2974,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out e, false, true); r = new ExprRhs(e); - } else SynErr(201); + } else SynErr(202); while (la.kind == 46) { Attribute(ref attrs); } @@ -2992,7 +2995,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 27 || la.kind == 48 || la.kind == 50) { Suffix(ref e); } - } else SynErr(202); + } else SynErr(203); } void Expressions(List args) { @@ -3049,7 +3052,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); pat = new CasePattern(bv.tok, bv); - } else SynErr(203); + } else SynErr(204); if (pat == null) { pat = new CasePattern(t, "_ParseError", new List()); } @@ -3071,7 +3074,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo isExistentialGuard = true; } else if (StartOf(8)) { Expression(out e, true, false); - } else SynErr(204); + } else SynErr(205); Expect(29); body = new List(); while (StartOf(16)) { @@ -3117,7 +3120,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out ee, true, true); e = ee; - } else SynErr(205); + } else SynErr(206); } void LoopSpec(List invariants, List decreases, ref List mod, ref Attributes decAttrs, ref Attributes modAttrs) { @@ -3125,7 +3128,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo bool isFree = false; Attributes attrs = null; if (la.kind == 37 || la.kind == 89) { - while (!(la.kind == 0 || la.kind == 37 || la.kind == 89)) {SynErr(206); Get();} + while (!(la.kind == 0 || la.kind == 37 || la.kind == 89)) {SynErr(207); Get();} if (la.kind == 89) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); @@ -3138,7 +3141,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo invariants.Add(new MaybeFreeExpression(e, isFree, attrs)); OldSemi(); } else if (la.kind == 36) { - while (!(la.kind == 0 || la.kind == 36)) {SynErr(207); Get();} + while (!(la.kind == 0 || la.kind == 36)) {SynErr(208); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); @@ -3146,7 +3149,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, true, true); OldSemi(); } else if (la.kind == 43) { - while (!(la.kind == 0 || la.kind == 43)) {SynErr(208); Get();} + while (!(la.kind == 0 || la.kind == 43)) {SynErr(209); Get();} Get(); mod = mod ?? new List(); while (IsAttribute()) { @@ -3160,7 +3163,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } OldSemi(); - } else SynErr(209); + } else SynErr(210); } void CaseStatement(out MatchCaseStmt/*!*/ c) { @@ -3197,12 +3200,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo arguments.Add(pat); } Expect(51); - } else SynErr(210); + } else SynErr(211); Expect(29); - while (!(StartOf(29))) {SynErr(211); Get();} + while (!(StartOf(29))) {SynErr(212); Get();} while (IsNotEndOfCase()) { Stmt(body); - while (!(StartOf(29))) {SynErr(212); Get();} + while (!(StartOf(29))) {SynErr(213); Get();} } c = new MatchCaseStmt(x, name, arguments, body); } @@ -3301,7 +3304,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp; break; } - default: SynErr(213); break; + default: SynErr(214); break; } if (k == null) { op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp); @@ -3316,7 +3319,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 113) { Get(); - } else SynErr(214); + } else SynErr(215); } void ImpliesOp() { @@ -3324,7 +3327,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 115) { Get(); - } else SynErr(215); + } else SynErr(216); } void ExpliesOp() { @@ -3332,7 +3335,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 117) { Get(); - } else SynErr(216); + } else SynErr(217); } void AndOp() { @@ -3340,7 +3343,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 119) { Get(); - } else SynErr(217); + } else SynErr(218); } void OrOp() { @@ -3348,7 +3351,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 121) { Get(); - } else SynErr(218); + } else SynErr(219); } void NegOp() { @@ -3356,7 +3359,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 123) { Get(); - } else SynErr(219); + } else SynErr(220); } void Forall() { @@ -3364,7 +3367,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 124) { Get(); - } else SynErr(220); + } else SynErr(221); } void Exists() { @@ -3372,7 +3375,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 126) { Get(); - } else SynErr(221); + } else SynErr(222); } void QSep() { @@ -3380,7 +3383,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 26) { Get(); - } else SynErr(222); + } else SynErr(223); } void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) { @@ -3415,7 +3418,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); } - } else SynErr(223); + } else SynErr(224); } } @@ -3445,7 +3448,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo RelationalExpression(out e1, allowSemi, allowLambda); e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); } - } else SynErr(224); + } else SynErr(225); } } @@ -3663,7 +3666,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(225); break; + default: SynErr(226); break; } } @@ -3685,7 +3688,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 129) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(226); + } else SynErr(227); } void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3745,7 +3748,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsSuffix()) { Suffix(ref e); } - } else SynErr(227); + } else SynErr(228); } void MulOp(out IToken x, out BinaryExpr.Opcode op) { @@ -3759,7 +3762,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 131) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(228); + } else SynErr(229); } void MapDisplayExpr(IToken/*!*/ mapToken, bool finite, out Expression e) { @@ -3813,13 +3816,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 107) { HashCall(id, out openParen, out typeArgs, out args); } else if (StartOf(32)) { - } else SynErr(229); + } else SynErr(230); e = new ExprDotName(id, e, id.val, typeArgs); if (openParen != null) { e = new ApplySuffix(openParen, e, args); } - } else SynErr(230); + } else SynErr(231); } else if (la.kind == 48) { Get(); x = t; @@ -3867,7 +3870,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(231); + } else SynErr(232); } else if (la.kind == 138) { Get(); anyDots = true; @@ -3875,7 +3878,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true, true); e1 = ee; } - } else SynErr(232); + } else SynErr(233); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -3919,7 +3922,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(51); e = new ApplySuffix(openParen, e, args); - } else SynErr(233); + } else SynErr(234); } void ISetDisplayExpr(IToken/*!*/ setToken, bool finite, out Expression e) { @@ -3961,7 +3964,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } Expect(51); - } else SynErr(234); + } else SynErr(235); while (la.kind == 44 || la.kind == 45) { if (la.kind == 44) { Get(); @@ -4044,7 +4047,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda); break; } - default: SynErr(235); break; + default: SynErr(236); break; } } @@ -4059,7 +4062,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 107) { HashCall(id, out openParen, out typeArgs, out args); } else if (StartOf(32)) { - } else SynErr(236); + } else SynErr(237); e = new NameSegment(id, id.val, typeArgs); if (openParen != null) { e = new ApplySuffix(openParen, e, args); @@ -4088,7 +4091,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SeqDisplayExpr(x, elements); Expect(49); - } else SynErr(237); + } else SynErr(238); } void MultiSetExpr(out Expression e) { @@ -4112,7 +4115,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, true); e = new MultiSetFormingExpr(x, e); Expect(51); - } else SynErr(238); + } else SynErr(239); } void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -4208,7 +4211,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda); break; } - default: SynErr(239); break; + default: SynErr(240); break; } } @@ -4237,7 +4240,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero; } - } else SynErr(240); + } else SynErr(241); } void Dec(out Basetypes.BigDec d) { @@ -4281,7 +4284,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 30) { Get(); oneShot = true; - } else SynErr(241); + } else SynErr(242); } void MapLiteralExpressions(out List elements) { @@ -4344,7 +4347,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseExpression(out c, allowSemi, allowLambda); cases.Add(c); } - } else SynErr(242); + } else SynErr(243); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -4362,7 +4365,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 125 || la.kind == 126) { Exists(); x = t; - } else SynErr(243); + } else SynErr(244); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi, allowLambda); @@ -4411,7 +4414,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 32) { CalcStmt(out s); - } else SynErr(244); + } else SynErr(245); } void LetExpr(out Expression e, bool allowSemi, bool allowLambda) { @@ -4455,7 +4458,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(245); + } else SynErr(246); Expression(out e, false, true); letRHSs.Add(e); while (la.kind == 22) { @@ -4515,7 +4518,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo arguments.Add(pat); } Expect(51); - } else SynErr(246); + } else SynErr(247); Expect(29); Expression(out body, allowSemi, allowLambda); c = new MatchCaseExpr(x, name, arguments, body); @@ -4549,7 +4552,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 2) { Get(); id = t; - } else SynErr(247); + } else SynErr(248); Expect(96); Expression(out e, true, true); } @@ -4592,7 +4595,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 44) { Get(); x = t; - } else SynErr(248); + } else SynErr(249); } @@ -4809,114 +4812,115 @@ public class Errors { case 138: s = "\"..\" expected"; break; case 139: s = "??? expected"; break; case 140: s = "invalid TopDecl"; break; - case 141: s = "this symbol not expected in SubModuleDecl"; break; - case 142: s = "invalid SubModuleDecl"; break; - case 143: s = "this symbol not expected in ClassDecl"; break; - case 144: s = "this symbol not expected in DatatypeDecl"; break; - case 145: s = "invalid DatatypeDecl"; break; - case 146: s = "this symbol not expected in DatatypeDecl"; break; - case 147: s = "invalid NewtypeDecl"; break; - case 148: s = "invalid OtherTypeDecl"; break; - case 149: s = "this symbol not expected in OtherTypeDecl"; break; - case 150: s = "this symbol not expected in IteratorDecl"; break; - case 151: s = "invalid IteratorDecl"; break; - case 152: s = "this symbol not expected in TraitDecl"; break; - case 153: s = "invalid ClassMemberDecl"; break; - case 154: s = "this symbol not expected in FieldDecl"; break; - case 155: s = "invalid FunctionDecl"; break; + case 141: s = "invalid DeclModifier"; break; + case 142: s = "this symbol not expected in SubModuleDecl"; break; + case 143: s = "invalid SubModuleDecl"; break; + case 144: s = "this symbol not expected in ClassDecl"; break; + case 145: s = "this symbol not expected in DatatypeDecl"; break; + case 146: s = "invalid DatatypeDecl"; break; + case 147: s = "this symbol not expected in DatatypeDecl"; break; + case 148: s = "invalid NewtypeDecl"; break; + case 149: s = "invalid OtherTypeDecl"; break; + case 150: s = "this symbol not expected in OtherTypeDecl"; break; + case 151: s = "this symbol not expected in IteratorDecl"; break; + case 152: s = "invalid IteratorDecl"; break; + case 153: s = "this symbol not expected in TraitDecl"; break; + case 154: s = "invalid ClassMemberDecl"; break; + case 155: s = "this symbol not expected in FieldDecl"; break; case 156: s = "invalid FunctionDecl"; break; case 157: s = "invalid FunctionDecl"; break; case 158: s = "invalid FunctionDecl"; break; case 159: s = "invalid FunctionDecl"; break; - case 160: s = "this symbol not expected in MethodDecl"; break; - case 161: s = "invalid MethodDecl"; break; + case 160: s = "invalid FunctionDecl"; break; + case 161: s = "this symbol not expected in MethodDecl"; break; case 162: s = "invalid MethodDecl"; break; - case 163: s = "invalid FIdentType"; break; - case 164: s = "this symbol not expected in OldSemi"; break; - case 165: s = "invalid TypeIdentOptional"; break; - case 166: s = "invalid TypeAndToken"; break; - case 167: s = "this symbol not expected in IteratorSpec"; break; - case 168: s = "invalid IteratorSpec"; break; + case 163: s = "invalid MethodDecl"; break; + case 164: s = "invalid FIdentType"; break; + case 165: s = "this symbol not expected in OldSemi"; break; + case 166: s = "invalid TypeIdentOptional"; break; + case 167: s = "invalid TypeAndToken"; break; + case 168: s = "this symbol not expected in IteratorSpec"; break; case 169: s = "invalid IteratorSpec"; break; - case 170: s = "this symbol not expected in MethodSpec"; break; - case 171: s = "invalid MethodSpec"; break; + case 170: s = "invalid IteratorSpec"; break; + case 171: s = "this symbol not expected in MethodSpec"; break; case 172: s = "invalid MethodSpec"; break; - case 173: s = "invalid FrameExpression"; break; - case 174: s = "this symbol not expected in FunctionSpec"; break; - case 175: s = "invalid FunctionSpec"; break; - case 176: s = "invalid PossiblyWildFrameExpression"; break; - case 177: s = "invalid PossiblyWildExpression"; break; - case 178: s = "this symbol not expected in OneStmt"; break; - case 179: s = "invalid OneStmt"; break; - case 180: s = "this symbol not expected in OneStmt"; break; - case 181: s = "invalid OneStmt"; break; - case 182: s = "invalid AssertStmt"; break; - case 183: s = "invalid AssumeStmt"; break; - case 184: s = "invalid UpdateStmt"; break; + case 173: s = "invalid MethodSpec"; break; + case 174: s = "invalid FrameExpression"; break; + case 175: s = "this symbol not expected in FunctionSpec"; break; + case 176: s = "invalid FunctionSpec"; break; + case 177: s = "invalid PossiblyWildFrameExpression"; break; + case 178: s = "invalid PossiblyWildExpression"; break; + case 179: s = "this symbol not expected in OneStmt"; break; + case 180: s = "invalid OneStmt"; break; + case 181: s = "this symbol not expected in OneStmt"; break; + case 182: s = "invalid OneStmt"; break; + case 183: s = "invalid AssertStmt"; break; + case 184: s = "invalid AssumeStmt"; break; case 185: s = "invalid UpdateStmt"; break; - case 186: s = "this symbol not expected in VarDeclStatement"; break; - case 187: s = "invalid VarDeclStatement"; break; + case 186: s = "invalid UpdateStmt"; break; + case 187: s = "this symbol not expected in VarDeclStatement"; break; case 188: s = "invalid VarDeclStatement"; break; - case 189: s = "invalid IfStmt"; break; + case 189: s = "invalid VarDeclStatement"; break; case 190: s = "invalid IfStmt"; break; - case 191: s = "invalid WhileStmt"; break; + case 191: s = "invalid IfStmt"; break; case 192: s = "invalid WhileStmt"; break; - case 193: s = "invalid MatchStmt"; break; - case 194: s = "invalid ForallStmt"; break; + case 193: s = "invalid WhileStmt"; break; + case 194: s = "invalid MatchStmt"; break; case 195: s = "invalid ForallStmt"; break; - case 196: s = "invalid CalcStmt"; break; - case 197: s = "invalid ModifyStmt"; break; - case 198: s = "this symbol not expected in ModifyStmt"; break; - case 199: s = "invalid ModifyStmt"; break; - case 200: s = "invalid ReturnStmt"; break; - case 201: s = "invalid Rhs"; break; - case 202: s = "invalid Lhs"; break; - case 203: s = "invalid CasePattern"; break; - case 204: s = "invalid AlternativeBlock"; break; - case 205: s = "invalid Guard"; break; - case 206: s = "this symbol not expected in LoopSpec"; break; + case 196: s = "invalid ForallStmt"; break; + case 197: s = "invalid CalcStmt"; break; + case 198: s = "invalid ModifyStmt"; break; + case 199: s = "this symbol not expected in ModifyStmt"; break; + case 200: s = "invalid ModifyStmt"; break; + case 201: s = "invalid ReturnStmt"; break; + case 202: s = "invalid Rhs"; break; + case 203: s = "invalid Lhs"; break; + case 204: s = "invalid CasePattern"; break; + case 205: s = "invalid AlternativeBlock"; break; + case 206: s = "invalid Guard"; break; case 207: s = "this symbol not expected in LoopSpec"; break; case 208: s = "this symbol not expected in LoopSpec"; break; - case 209: s = "invalid LoopSpec"; break; - case 210: s = "invalid CaseStatement"; break; - case 211: s = "this symbol not expected in CaseStatement"; break; + case 209: s = "this symbol not expected in LoopSpec"; break; + case 210: s = "invalid LoopSpec"; break; + case 211: s = "invalid CaseStatement"; break; case 212: s = "this symbol not expected in CaseStatement"; break; - case 213: s = "invalid CalcOp"; break; - case 214: s = "invalid EquivOp"; break; - case 215: s = "invalid ImpliesOp"; break; - case 216: s = "invalid ExpliesOp"; break; - case 217: s = "invalid AndOp"; break; - case 218: s = "invalid OrOp"; break; - case 219: s = "invalid NegOp"; break; - case 220: s = "invalid Forall"; break; - case 221: s = "invalid Exists"; break; - case 222: s = "invalid QSep"; break; - case 223: s = "invalid ImpliesExpliesExpression"; break; - case 224: s = "invalid LogicalExpression"; break; - case 225: s = "invalid RelOp"; break; - case 226: s = "invalid AddOp"; break; - case 227: s = "invalid UnaryExpression"; break; - case 228: s = "invalid MulOp"; break; - case 229: s = "invalid Suffix"; break; + case 213: s = "this symbol not expected in CaseStatement"; break; + case 214: s = "invalid CalcOp"; break; + case 215: s = "invalid EquivOp"; break; + case 216: s = "invalid ImpliesOp"; break; + case 217: s = "invalid ExpliesOp"; break; + case 218: s = "invalid AndOp"; break; + case 219: s = "invalid OrOp"; break; + case 220: s = "invalid NegOp"; break; + case 221: s = "invalid Forall"; break; + case 222: s = "invalid Exists"; break; + case 223: s = "invalid QSep"; break; + case 224: s = "invalid ImpliesExpliesExpression"; break; + case 225: s = "invalid LogicalExpression"; break; + case 226: s = "invalid RelOp"; break; + case 227: s = "invalid AddOp"; break; + case 228: s = "invalid UnaryExpression"; break; + case 229: s = "invalid MulOp"; break; case 230: s = "invalid Suffix"; break; case 231: s = "invalid Suffix"; break; case 232: s = "invalid Suffix"; break; case 233: s = "invalid Suffix"; break; - case 234: s = "invalid LambdaExpression"; break; - case 235: s = "invalid EndlessExpression"; break; - case 236: s = "invalid NameSegment"; break; - case 237: s = "invalid DisplayExpr"; break; - case 238: s = "invalid MultiSetExpr"; break; - case 239: s = "invalid ConstAtomExpression"; break; - case 240: s = "invalid Nat"; break; - case 241: s = "invalid LambdaArrow"; break; - case 242: s = "invalid MatchExpression"; break; - case 243: s = "invalid QuantifierGuts"; break; - case 244: s = "invalid StmtInExpr"; break; - case 245: s = "invalid LetExpr"; break; - case 246: s = "invalid CaseExpression"; break; - case 247: s = "invalid MemberBindingUpdate"; break; - case 248: s = "invalid DotSuffix"; break; + case 234: s = "invalid Suffix"; break; + case 235: s = "invalid LambdaExpression"; break; + case 236: s = "invalid EndlessExpression"; break; + case 237: s = "invalid NameSegment"; break; + case 238: s = "invalid DisplayExpr"; break; + case 239: s = "invalid MultiSetExpr"; break; + case 240: s = "invalid ConstAtomExpression"; break; + case 241: s = "invalid Nat"; break; + case 242: s = "invalid LambdaArrow"; break; + case 243: s = "invalid MatchExpression"; break; + case 244: s = "invalid QuantifierGuts"; break; + case 245: s = "invalid StmtInExpr"; break; + case 246: s = "invalid LetExpr"; break; + case 247: s = "invalid CaseExpression"; break; + case 248: s = "invalid MemberBindingUpdate"; break; + case 249: s = "invalid DotSuffix"; break; default: s = "error " + n; break; } diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a60971b1..464aff79 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -310,11 +310,12 @@ namespace Microsoft.Dafny string targetFilename = Path.ChangeExtension(dafnyProgramName, "cs"); using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) { target.Write(csharpProgram); + string relativeTarget = Path.GetFileName(targetFilename); if (completeProgram) { - outputWriter.WriteLine("Compiled program written to {0}", targetFilename); + outputWriter.WriteLine("Compiled program written to {0}", relativeTarget); } else { - outputWriter.WriteLine("File {0} contains the partially compiled program", targetFilename); + outputWriter.WriteLine("File {0} contains the partially compiled program", relativeTarget); } } return targetFilename; diff --git a/Test/dafny0/Extern.dfy.expect b/Test/dafny0/Extern.dfy.expect index fec087d9..25c1c3ee 100644 --- a/Test/dafny0/Extern.dfy.expect +++ b/Test/dafny0/Extern.dfy.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 7 verified, 0 errors -Compiled program written to D:\de\dafny\Test\dafny0\Extern.cs +Compiled program written to Extern.cs Compiled assembly into Extern.exe -- cgit v1.2.3