From 40f36d68b8cb9489d052ababada29539c7d8de92 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 23 Oct 2014 21:52:12 -0700 Subject: Allow underscores in numeric literals (and in field/destructor names that are written as numeric strings). The underscores have no semantic meaning, but can help a human parse the numbers. --- Test/dafny0/Basics.dfy | 28 ++++++++++++++-------------- Test/dafny0/Compilation.dfy | 17 +++++++++++++++++ Test/dafny0/Compilation.dfy.expect | 2 +- Test/dafny0/RealTypes.dfy | 8 ++++---- Test/dafny4/BinarySearch.dfy | 6 +++--- 5 files changed, 39 insertions(+), 22 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 6e71e5b2..26baa35f 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -427,23 +427,23 @@ method HexTest() assert forall i :: 0 <= i < |first16upper| ==> first16upper[i] == i; var randomHex := [ 0xCF4458F2, 0x9A5C5BAF, 0x26A6ABD6, 0x00EB3933, 0x9123D2CF, 0xBE040001, 0x5AD038FA, 0xC75597A6, 0x7CF821A7, 0xCDEFB617, 0x4889D968, 0xB05F896A, - 0x75B18DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46, - 0x610D0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D, - 0x02FBF254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D, - 0x730D85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190, - 0xc95f056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143, - 0x1520b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e, - 0xbfcd3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30, - 0xcd85f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd8C6FAF7 ]; + 0x75B1_8DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46, + 0x610D_0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D, + 0x02FB_F254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D, + 0x730D_85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190, + 0xc95f_056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143, + 0x1520_b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e, + 0xbfcd_3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30, + 0xcd85_f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd_8_C_6_F_A_F_7 ]; var randomDec := [ 3477362930, 2589744047, 648457174, 15415603, 2435044047, 3187933185, 1523595514, 3344275366, 2096636327, 3455038999, 1216993640, 2959051114, - 1974570418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470, - 1628242745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885, - 50066004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605, - 1930266087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040, - 3378447726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811, + 1_974_570_418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470, + 1_628_242_745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885, + 50_066_004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605, + 1_930_266_087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040, + 3_378_447_726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811, 354465647, 2080258281, 2351471473, 1736439093, 196693838, 4215372800, 2714419258, 1581046514, 1981216564, 3042395387, 660877099, 2707539070, 3217899519, 2788029817, 1050875824, 3362808767, 3721613, 2510678132, 1993876726, 409501246, 1273417770, 741130572, 1855051115, 1994570544, - 3448107468, 1645859758, 3193559252, 3636919031 ]; + 3448107468, 1645859758, 3_1_9_3_5_5_9_2_5_2, 3636919031 ]; assert forall i :: 0 <= i < |randomHex| ==> randomHex[i] == randomDec[i]; } diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 2bff422f..d8ff3989 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -210,3 +210,20 @@ module GhostLetExpr { G(5, xyz) } } + +class DigitUnderscore_Names { + // the following would be the same integers, but they are different fields + var 0_1_0: int; + var 010: int; + var 10: int; + // ... as we see here: + method M() + modifies this; + { + this.0_1_0 := 007; + this.010 := 000_008; + this.10 := 0x0000_0009; + assert this.0_1_0 == int(00_07.0_0) && this.010 == 8 && this.10 == 9; + this.10 := 20; + } +} diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect index af8ed2fc..0a1938ae 100644 --- a/Test/dafny0/Compilation.dfy.expect +++ b/Test/dafny0/Compilation.dfy.expect @@ -1,3 +1,3 @@ -Dafny program verifier finished with 44 verified, 0 errors +Dafny program verifier finished with 46 verified, 0 errors Compiled assembly into Compilation.exe diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy index 76ac9d93..1004a015 100644 --- a/Test/dafny0/RealTypes.dfy +++ b/Test/dafny0/RealTypes.dfy @@ -23,10 +23,10 @@ method R2(ghost x: real, ghost y: real) { // Check that literals are handled properly method R3() { - ghost var x := 1.5; - ghost var y := real(3); - assert x == y / 2.0000000; - assert x == y / 2.000000000000000000000000001; // error + ghost var x := 000_00_0_1.5_0_0_00_000_0; // 1.5 + ghost var y := real(000_000_003); // 3 + assert x == y / 2.000_000_0; + assert x == y / 2.000_000_000_000_000_000_000_000_001; // error } // Check that real value in decreases clause doesn't scare Dafny diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy index a06f6c4a..1c1d7299 100644 --- a/Test/dafny4/BinarySearch.dfy +++ b/Test/dafny4/BinarySearch.dfy @@ -28,10 +28,10 @@ method BinarySearch(a: array, key: int) returns (r: int) // Binary search using bounded integers -newtype int32 = x | -0x80000000 <= x < 0x80000000 +newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000 method BinarySearchInt32_bad(a: array, key: int) returns (r: int32) - requires a != null && a.Length < 0x80000000; + requires a != null && a.Length < 0x8000_0000; requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; ensures 0 <= r ==> r < int32(a.Length) && a[r] == key; ensures r < 0 ==> key !in a[..]; @@ -54,7 +54,7 @@ method BinarySearchInt32_bad(a: array, key: int) returns (r: int32) } method BinarySearchInt32_good(a: array, key: int) returns (r: int32) - requires a != null && a.Length < 0x80000000; + requires a != null && a.Length < 0x8000_0000; requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; ensures 0 <= r ==> r < int32(a.Length) && a[r] == key; ensures r < 0 ==> key !in a[..]; -- cgit v1.2.3 From abae3f833c387594b1c29f6e8b27c0ad655b3062 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 25 Oct 2014 00:40:22 -0700 Subject: Made semi-colons are specification clauses optional. In a future version, they will no longer be allowed. --- Source/Dafny/Dafny.atg | 53 +++--- Source/Dafny/Parser.cs | 419 ++++++++++++++++++++----------------------- Test/dafny4/BinarySearch.dfy | 36 ++-- 3 files changed, 239 insertions(+), 269 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 20765b74..2134ba6d 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -474,7 +474,7 @@ FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) { "," FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) } - SYNC ";" + OldSemi . NewtypeDecl = (. IToken id, bvId; @@ -494,11 +494,6 @@ NewtypeDecl Expression (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .) | Type (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .) ) - [ SYNC ";" - // In a future version of Dafny, including the following warning message: - // (. 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"); .) - // And in a version after that, don't allow the semi-colon at all. - ] . OtherTypeDecl = (. IToken id; @@ -781,15 +776,15 @@ MethodSpec<.List/*!*/ req, List/ [ FrameExpression (. mod.Add(fe); .) { "," FrameExpression (. mod.Add(fe); .) } - ] SYNC ";" + ] OldSemi | [ "free" (. isFree = true; .) ] - ( "requires" Expression SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .) + ( "requires" Expression OldSemi (. req.Add(new MaybeFreeExpression(e, isFree)); .) | "ensures" { IF(IsAttribute()) Attribute } - Expression SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .) + Expression OldSemi (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .) ) - | "decreases" { IF(IsAttribute()) Attribute } DecreasesList SYNC ";" + | "decreases" { IF(IsAttribute()) Attribute } DecreasesList OldSemi ) . IteratorSpec<.List/*!*/ reads, List/*!*/ mod, List decreases, @@ -803,31 +798,31 @@ IteratorSpec<.List/*!*/ reads, List/ [ FrameExpression (. reads.Add(fe); .) { "," FrameExpression (. reads.Add(fe); .) } - ] SYNC ";" + ] OldSemi | "modifies" { IF(IsAttribute()) Attribute } [ FrameExpression (. mod.Add(fe); .) { "," FrameExpression (. mod.Add(fe); .) } - ] SYNC ";" + ] OldSemi | [ "free" (. isFree = true; .) ] [ "yield" (. isYield = true; .) ] - ( "requires" Expression SYNC ";" (. if (isYield) { + ( "requires" Expression OldSemi (. if (isYield) { yieldReq.Add(new MaybeFreeExpression(e, isFree)); } else { req.Add(new MaybeFreeExpression(e, isFree)); } .) | "ensures" { IF(IsAttribute()) Attribute } - Expression SYNC ";" (. if (isYield) { + Expression OldSemi (. if (isYield) { yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } .) ) - | "decreases" { IF(IsAttribute()) Attribute } DecreasesList SYNC ";" + | "decreases" { IF(IsAttribute()) Attribute } DecreasesList OldSemi ) . Formals<.bool incoming, bool allowGhostKeyword, List formals.> @@ -1054,18 +1049,18 @@ FunctionSpec<.List/*!*/ reqs, List/*!*/ r Expression/*!*/ e; FrameExpression/*!*/ fe; .) ( SYNC - "requires" Expression SYNC ";" (. reqs.Add(e); .) - | "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .) - { "," PossiblyWildFrameExpression (. reads.Add(fe); .) + "requires" Expression OldSemi (. reqs.Add(e); .) + | "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .) + { "," PossiblyWildFrameExpression (. reads.Add(fe); .) } - ] SYNC ";" - | "ensures" Expression SYNC ";" (. ens.Add(e); .) + ] OldSemi + | "ensures" Expression OldSemi (. ens.Add(e); .) | "decreases" (. if (decreases == null) { SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed"); decreases = new List(); } .) - DecreasesList SYNC ";" + DecreasesList OldSemi ) . @@ -1453,16 +1448,16 @@ LoopSpec<.out List invariants, out List SYNC ";" (. invariants.Add(invariant); .) + Invariant OldSemi (. invariants.Add(invariant); .) | SYNC "decreases" { IF(IsAttribute()) Attribute } - DecreasesList SYNC ";" + DecreasesList OldSemi | SYNC "modifies" { IF(IsAttribute()) Attribute } (. mod = mod ?? new List(); .) [ FrameExpression (. mod.Add(fe); .) { "," FrameExpression (. mod.Add(fe); .) } - ] SYNC ";" + ] OldSemi } . Invariant @@ -1616,8 +1611,8 @@ ForallStmt { (. isFree = false; .) [ "free" (. isFree = true; .) ] - "ensures" Expression (. ens.Add(new MaybeFreeExpression(e, isFree)); .) - ";" (. tok = t; .) + "ensures" Expression (. ens.Add(new MaybeFreeExpression(e, isFree)); .) + OldSemi (. tok = t; .) } [ BlockStmt ] @@ -2658,6 +2653,12 @@ WildIdent .) . +OldSemi += /* In the future, semi-colons will be neither needed nor allowed in certain places where, in the past, they + * were required. As a period of transition between the two, such semi-colons are optional. + */ + [ SYNC ";" ]. + Nat = (. n = BigInteger.Zero; string S; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6ce29b9c..20f9332d 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -568,10 +568,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Type(out baseType); td = new NewtypeDecl(id, id.val, module, baseType, attrs); } else SynErr(140); - if (la.kind == 10) { - while (!(la.kind == 0 || la.kind == 10)) {SynErr(141); Get();} - Get(); - } } void OtherTypeDecl(ModuleDefinition module, out TopLevelDecl td) { @@ -604,13 +600,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Type(out ty); td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); } - } else SynErr(142); + } else SynErr(141); if (td == null) { td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs); } if (la.kind == 10) { - while (!(la.kind == 0 || la.kind == 10)) {SynErr(143); Get();} + while (!(la.kind == 0 || la.kind == 10)) {SynErr(142); Get();} Get(); } } @@ -638,7 +634,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 42)) {SynErr(144); Get();} + while (!(la.kind == 0 || la.kind == 42)) {SynErr(143); Get();} Expect(42); while (la.kind == 15) { Attribute(ref attrs); @@ -661,7 +657,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 45) { Get(); signatureEllipsis = t; - } else SynErr(145); + } else SynErr(144); while (StartOf(5)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } @@ -688,7 +684,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 32)) {SynErr(146); Get();} + while (!(la.kind == 0 || la.kind == 32)) {SynErr(145); Get();} Expect(32); while (la.kind == 15) { Attribute(ref attrs); @@ -732,7 +728,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (StartOf(6)) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(147); + } else SynErr(146); } void Attribute(ref Attributes attrs) { @@ -808,7 +804,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 13) { Get(); x = t; - } else SynErr(148); + } else SynErr(147); } void GenericParameters(List/*!*/ typeArgs) { @@ -846,7 +842,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 37)) {SynErr(149); Get();} + while (!(la.kind == 0 || la.kind == 37)) {SynErr(148); Get();} Expect(37); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } @@ -860,8 +856,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { FIdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 10)) {SynErr(150); Get();} - Expect(10); + OldSemi(); } void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) { @@ -905,7 +900,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 45) { Get(); signatureEllipsis = t; - } else SynErr(151); + } else SynErr(149); } else if (la.kind == 71) { Get(); isPredicate = true; @@ -936,7 +931,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 45) { Get(); signatureEllipsis = t; - } else SynErr(152); + } else SynErr(150); } else if (la.kind == 72) { Get(); isCoPredicate = true; @@ -963,8 +958,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 45) { Get(); signatureEllipsis = t; - } else SynErr(153); - } else SynErr(154); + } else SynErr(151); + } else SynErr(152); decreases = isCoPredicate ? null : new List(); while (StartOf(8)) { FunctionSpec(reqs, reads, ens, decreases); @@ -1019,7 +1014,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(StartOf(9))) {SynErr(155); Get();} + while (!(StartOf(9))) {SynErr(153); Get();} if (la.kind == 48) { Get(); } else if (la.kind == 49) { @@ -1041,7 +1036,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { SemErr(t, "constructors are allowed only in classes"); } - } else SynErr(156); + } else SynErr(154); keywordToken = t; if (isLemma) { if (mmod.IsGhost) { @@ -1087,7 +1082,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 45) { Get(); signatureEllipsis = t; - } else SynErr(157); + } else SynErr(155); while (StartOf(10)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } @@ -1161,11 +1156,18 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 2) { Get(); id = t; - } else SynErr(158); + } else SynErr(156); Expect(8); Type(out ty); } + void OldSemi() { + if (la.kind == 10) { + while (!(la.kind == 0 || la.kind == 10)) {SynErr(157); Get();} + Get(); + } + } + void Type(out Type ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; TypeAndToken(out tok, out ty); @@ -1263,7 +1265,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { id = t; name = id.val; Expect(8); Type(out ty); - } else SynErr(159); + } else SynErr(158); if (name != null) { identName = name; } else { @@ -1392,7 +1394,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { ReferenceType(out tok, out ty); break; } - default: SynErr(160); break; + default: SynErr(159); break; } if (la.kind == 12) { Type t2; @@ -1429,7 +1431,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(12))) {SynErr(161); Get();} + while (!(StartOf(12))) {SynErr(160); Get();} if (la.kind == 13) { Get(); while (IsAttribute()) { @@ -1444,8 +1446,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 10)) {SynErr(162); Get();} - Expect(10); + OldSemi(); } else if (la.kind == 53) { Get(); while (IsAttribute()) { @@ -1460,8 +1461,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 10)) {SynErr(163); Get();} - Expect(10); + OldSemi(); } else if (StartOf(14)) { if (la.kind == 54) { Get(); @@ -1474,12 +1474,11 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (la.kind == 14) { Get(); Expression(out e, false, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(164); Get();} - Expect(10); + OldSemi(); if (isYield) { - yieldReq.Add(new MaybeFreeExpression(e, isFree)); + yieldReq.Add(new MaybeFreeExpression(e, isFree)); } else { - req.Add(new MaybeFreeExpression(e, isFree)); + req.Add(new MaybeFreeExpression(e, isFree)); } } else if (la.kind == 55) { @@ -1488,24 +1487,22 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Attribute(ref ensAttrs); } Expression(out e, false, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(165); Get();} - Expect(10); + OldSemi(); if (isYield) { - yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else { - ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } - } else SynErr(166); + } else SynErr(161); } else if (la.kind == 56) { Get(); while (IsAttribute()) { Attribute(ref decrAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(167); Get();} - Expect(10); - } else SynErr(168); + OldSemi(); + } else SynErr(162); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -1527,7 +1524,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(16))) {SynErr(169); Get();} + while (!(StartOf(16))) {SynErr(163); Get();} if (la.kind == 53) { Get(); while (IsAttribute()) { @@ -1542,8 +1539,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 10)) {SynErr(170); Get();} - Expect(10); + OldSemi(); } else if (la.kind == 14 || la.kind == 54 || la.kind == 55) { if (la.kind == 54) { Get(); @@ -1552,8 +1548,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 14) { Get(); Expression(out e, false, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(171); Get();} - Expect(10); + OldSemi(); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 55) { Get(); @@ -1561,19 +1556,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs); } Expression(out e, false, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(172); Get();} - Expect(10); + OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(173); + } else SynErr(164); } else if (la.kind == 56) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(174); Get();} - Expect(10); - } else SynErr(175); + OldSemi(); + } else SynErr(165); } void FrameExpression(out FrameExpression/*!*/ fe) { @@ -1597,7 +1590,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(176); + } else SynErr(166); } void DecreasesList(List decreases, bool allowWildcard) { @@ -1665,7 +1658,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt, path); - } else SynErr(177); + } else SynErr(167); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases) { @@ -1674,11 +1667,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; if (la.kind == 14) { - while (!(la.kind == 0 || la.kind == 14)) {SynErr(178); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(168); Get();} Get(); Expression(out e, false, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(179); Get();} - Expect(10); + OldSemi(); reqs.Add(e); } else if (la.kind == 13) { Get(); @@ -1691,13 +1683,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 10)) {SynErr(180); Get();} - Expect(10); + OldSemi(); } else if (la.kind == 55) { Get(); Expression(out e, false, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(181); Get();} - Expect(10); + OldSemi(); ens.Add(e); } else if (la.kind == 56) { Get(); @@ -1707,9 +1697,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(182); Get();} - Expect(10); - } else SynErr(183); + OldSemi(); + } else SynErr(169); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1728,7 +1717,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(13)) { FrameExpression(out fe); - } else SynErr(184); + } else SynErr(170); } void LambdaSpec(out Expression req, List reads) { @@ -1760,7 +1749,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t); } else if (StartOf(17)) { Expression(out e, false, false); - } else SynErr(185); + } else SynErr(171); } void Stmt(List/*!*/ ss) { @@ -1777,7 +1766,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(19))) {SynErr(186); Get();} + while (!(StartOf(19))) {SynErr(172); Get();} switch (la.kind) { case 15: { BlockStmt(out bs, out bodyStart, out bodyEnd); @@ -1848,8 +1837,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); breakCount++; } - } else SynErr(187); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(188); Get();} + } else SynErr(173); + while (!(la.kind == 0 || la.kind == 10)) {SynErr(174); Get();} Expect(10); s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); break; @@ -1862,7 +1851,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo SkeletonStmt(out s); break; } - default: SynErr(189); break; + default: SynErr(175); break; } } @@ -1881,7 +1870,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 45) { Get(); dotdotdot = t; - } else SynErr(190); + } else SynErr(176); Expect(10); if (dotdotdot != null) { s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null); @@ -1906,7 +1895,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 45) { Get(); dotdotdot = t; - } else SynErr(191); + } else SynErr(177); Expect(10); if (dotdotdot != null) { s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null); @@ -1976,13 +1965,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo suchThatAssume = t; } Expression(out suchThat, false, true); - } else SynErr(192); + } else SynErr(178); Expect(10); endTok = t; } else if (la.kind == 8) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(193); + } else SynErr(179); if (suchThat != null) { s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume); } else { @@ -2103,7 +2092,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 15) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; endTok = bs.EndTok; - } else SynErr(194); + } else SynErr(180); } if (guardEllipsis != null) { ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null); @@ -2111,7 +2100,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ifStmt = new IfStmt(x, endTok, guard, thn, els); } - } else SynErr(195); + } else SynErr(181); } void WhileStmt(out Statement/*!*/ stmt) { @@ -2148,7 +2137,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 45) { Get(); bodyEllipsis = t; endTok = t; - } else SynErr(196); + } else SynErr(182); if (guardEllipsis != null || bodyEllipsis != null) { if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); @@ -2164,7 +2153,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(197); + } else SynErr(183); } void MatchStmt(out Statement/*!*/ s) { @@ -2188,7 +2177,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(16); } else if (StartOf(22)) { if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } - } else SynErr(198); + } else SynErr(184); s = new MatchStmt(x, t, e, cases, usesOptionalBrace); } @@ -2214,7 +2203,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(199); + } else SynErr(185); if (la.kind == 17) { Get(); usesOptionalParen = true; @@ -2232,7 +2221,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); } else if (StartOf(23)) { if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } - } else SynErr(200); + } else SynErr(186); while (la.kind == 54 || la.kind == 55) { isFree = false; if (la.kind == 54) { @@ -2242,7 +2231,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(55); Expression(out e, false, true); ens.Add(new MaybeFreeExpression(e, isFree)); - Expect(10); + OldSemi(); tok = t; } if (la.kind == 15) { @@ -2348,10 +2337,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 15) { BlockStmt(out body, out bodyStart, out endTok); } else if (la.kind == 10) { - while (!(la.kind == 0 || la.kind == 10)) {SynErr(201); Get();} + while (!(la.kind == 0 || la.kind == 10)) {SynErr(187); Get();} Get(); endTok = t; - } else SynErr(202); + } else SynErr(188); s = new ModifyStmt(tok, endTok, mod, attrs, body); if (ellipsisToken != null) { s = new SkeletonStatement(s, ellipsisToken, null); @@ -2371,7 +2360,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 57) { Get(); returnTok = t; isYield = true; - } else SynErr(203); + } else SynErr(189); if (StartOf(26)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); @@ -2473,7 +2462,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(17)) { Expression(out e, false, true); r = new ExprRhs(e); - } else SynErr(204); + } else SynErr(190); while (la.kind == 15) { Attribute(ref attrs); } @@ -2495,7 +2484,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 69 || la.kind == 82) { Suffix(ref e); } - } else SynErr(205); + } else SynErr(191); } void Expressions(List/*!*/ args) { @@ -2544,7 +2533,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(17)) { Expression(out ee, true, true); e = ee; - } else SynErr(206); + } else SynErr(192); } void LoopSpec(out List invariants, out List decreases, out List mod, ref Attributes decAttrs, ref Attributes modAttrs) { @@ -2557,20 +2546,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (StartOf(28)) { if (la.kind == 54 || la.kind == 88) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(207); Get();} - Expect(10); + OldSemi(); invariants.Add(invariant); } else if (la.kind == 56) { - while (!(la.kind == 0 || la.kind == 56)) {SynErr(208); Get();} + while (!(la.kind == 0 || la.kind == 56)) {SynErr(193); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 10)) {SynErr(209); Get();} - Expect(10); + OldSemi(); } else { - while (!(la.kind == 0 || la.kind == 53)) {SynErr(210); Get();} + while (!(la.kind == 0 || la.kind == 53)) {SynErr(194); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -2585,15 +2572,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 10)) {SynErr(211); Get();} - Expect(10); + OldSemi(); } } } void Invariant(out MaybeFreeExpression/*!*/ invariant) { bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; - while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(212); Get();} + while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(195); Get();} if (la.kind == 54) { Get(); isFree = true; @@ -2734,7 +2720,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp; break; } - default: SynErr(213); break; + default: SynErr(196); break; } if (k == null) { op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp); @@ -2771,7 +2757,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 104) { Get(); - } else SynErr(214); + } else SynErr(197); } void ImpliesOp() { @@ -2779,7 +2765,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 106) { Get(); - } else SynErr(215); + } else SynErr(198); } void ExpliesOp() { @@ -2787,7 +2773,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 108) { Get(); - } else SynErr(216); + } else SynErr(199); } void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) { @@ -2972,7 +2958,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 110) { Get(); - } else SynErr(217); + } else SynErr(200); } void OrOp() { @@ -2980,7 +2966,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 112) { Get(); - } else SynErr(218); + } else SynErr(201); } void Term(out Expression e0, bool allowSemi, bool allowLambda) { @@ -3085,7 +3071,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(219); break; + default: SynErr(202); break; } } @@ -3107,7 +3093,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 116) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(220); + } else SynErr(203); } void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3165,7 +3151,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MapComprehensionExpr(x, out e, allowSemi); } else if (StartOf(32)) { SemErr("map must be followed by literal in brackets or comprehension."); - } else SynErr(221); + } else SynErr(204); break; } case 2: case 3: case 4: case 6: case 7: case 9: case 17: case 61: case 62: case 120: case 121: case 122: case 123: case 124: case 125: { @@ -3175,7 +3161,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } break; } - default: SynErr(222); break; + default: SynErr(205); break; } } @@ -3190,7 +3176,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 118) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(223); + } else SynErr(206); } void NegOp() { @@ -3198,7 +3184,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 119) { Get(); - } else SynErr(224); + } else SynErr(207); } void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3245,7 +3231,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda); break; } - default: SynErr(225); break; + default: SynErr(208); break; } } @@ -3387,7 +3373,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(226); + } else SynErr(209); } else if (la.kind == 127) { Get(); anyDots = true; @@ -3395,7 +3381,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true, true); e1 = ee; } - } else SynErr(227); + } else SynErr(210); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -3436,7 +3422,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(83); - } else SynErr(228); + } else SynErr(211); ApplySuffix(ref e); } @@ -3473,7 +3459,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SeqDisplayExpr(x, elements); Expect(83); - } else SynErr(229); + } else SynErr(212); } void MultiSetExpr(out Expression e) { @@ -3499,7 +3485,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); } else if (StartOf(32)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(230); + } else SynErr(213); } void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) { @@ -3627,7 +3613,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda); break; } - default: SynErr(231); break; + default: SynErr(214); break; } } @@ -3656,7 +3642,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero; } - } else SynErr(232); + } else SynErr(215); } void Dec(out Basetypes.BigDec d) { @@ -3766,7 +3752,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 12) { Get(); oneShot = true; - } else SynErr(233); + } else SynErr(216); } void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) { @@ -3799,7 +3785,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 132) { Get(); - } else SynErr(234); + } else SynErr(217); } void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3822,7 +3808,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(16); } else if (StartOf(32)) { if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } - } else SynErr(235); + } else SynErr(218); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -3840,7 +3826,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 129 || la.kind == 130) { Exists(); x = t; - } else SynErr(236); + } else SynErr(219); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi, allowLambda); @@ -3888,7 +3874,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 95) { CalcStmt(out s); - } else SynErr(237); + } else SynErr(220); } void LetExpr(out Expression e, bool allowSemi, bool allowLambda) { @@ -3928,7 +3914,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(238); + } else SynErr(221); Expression(out e, false, true); letRHSs.Add(e); while (la.kind == 38) { @@ -3979,7 +3965,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); pat = new CasePattern(bv.tok, bv); - } else SynErr(239); + } else SynErr(222); if (pat == null) { pat = new CasePattern(t, "_ParseError", new List()); } @@ -4016,7 +4002,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 128) { Get(); - } else SynErr(240); + } else SynErr(223); } void Exists() { @@ -4024,7 +4010,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 130) { Get(); - } else SynErr(241); + } else SynErr(224); } void AttributeBody(ref Attributes attrs) { @@ -4258,107 +4244,90 @@ public class Errors { case 138: s = "invalid DatatypeDecl"; break; case 139: s = "this symbol not expected in DatatypeDecl"; break; case 140: s = "invalid NewtypeDecl"; break; - case 141: s = "this symbol not expected in NewtypeDecl"; break; - case 142: s = "invalid OtherTypeDecl"; break; - case 143: s = "this symbol not expected in OtherTypeDecl"; break; - case 144: s = "this symbol not expected in IteratorDecl"; break; - case 145: s = "invalid IteratorDecl"; break; - case 146: s = "this symbol not expected in TraitDecl"; break; - case 147: s = "invalid ClassMemberDecl"; break; - case 148: s = "invalid IdentOrDigitsSuffix"; break; - case 149: s = "this symbol not expected in FieldDecl"; break; - case 150: s = "this symbol not expected in FieldDecl"; break; + case 141: s = "invalid OtherTypeDecl"; break; + case 142: s = "this symbol not expected in OtherTypeDecl"; break; + case 143: s = "this symbol not expected in IteratorDecl"; break; + case 144: s = "invalid IteratorDecl"; break; + case 145: s = "this symbol not expected in TraitDecl"; break; + case 146: s = "invalid ClassMemberDecl"; break; + case 147: s = "invalid IdentOrDigitsSuffix"; break; + case 148: s = "this symbol not expected in FieldDecl"; break; + case 149: s = "invalid FunctionDecl"; break; + case 150: s = "invalid FunctionDecl"; break; case 151: s = "invalid FunctionDecl"; break; case 152: s = "invalid FunctionDecl"; break; - case 153: s = "invalid FunctionDecl"; break; - case 154: s = "invalid FunctionDecl"; break; - case 155: s = "this symbol not expected in MethodDecl"; break; - case 156: s = "invalid MethodDecl"; break; - case 157: s = "invalid MethodDecl"; break; - case 158: s = "invalid FIdentType"; break; - case 159: s = "invalid TypeIdentOptional"; break; - case 160: s = "invalid TypeAndToken"; break; - case 161: s = "this symbol not expected in IteratorSpec"; break; - case 162: s = "this symbol not expected in IteratorSpec"; break; - case 163: s = "this symbol not expected in IteratorSpec"; break; - case 164: s = "this symbol not expected in IteratorSpec"; break; - case 165: s = "this symbol not expected in IteratorSpec"; break; - case 166: s = "invalid IteratorSpec"; break; - case 167: s = "this symbol not expected in IteratorSpec"; break; - case 168: s = "invalid IteratorSpec"; break; - case 169: s = "this symbol not expected in MethodSpec"; break; - case 170: s = "this symbol not expected in MethodSpec"; break; - case 171: s = "this symbol not expected in MethodSpec"; break; - case 172: s = "this symbol not expected in MethodSpec"; break; - case 173: s = "invalid MethodSpec"; break; - case 174: s = "this symbol not expected in MethodSpec"; break; - case 175: s = "invalid MethodSpec"; break; - case 176: s = "invalid FrameExpression"; break; - case 177: s = "invalid ReferenceType"; break; - case 178: s = "this symbol not expected in FunctionSpec"; break; - case 179: s = "this symbol not expected in FunctionSpec"; break; - case 180: s = "this symbol not expected in FunctionSpec"; break; - case 181: s = "this symbol not expected in FunctionSpec"; break; - case 182: s = "this symbol not expected in FunctionSpec"; break; - case 183: s = "invalid FunctionSpec"; break; - case 184: s = "invalid PossiblyWildFrameExpression"; break; - case 185: s = "invalid PossiblyWildExpression"; break; - case 186: s = "this symbol not expected in OneStmt"; break; - case 187: s = "invalid OneStmt"; break; - case 188: s = "this symbol not expected in OneStmt"; break; - case 189: s = "invalid OneStmt"; break; - case 190: s = "invalid AssertStmt"; break; - case 191: s = "invalid AssumeStmt"; break; - case 192: s = "invalid UpdateStmt"; break; - case 193: s = "invalid UpdateStmt"; break; - case 194: s = "invalid IfStmt"; break; - case 195: s = "invalid IfStmt"; break; - case 196: s = "invalid WhileStmt"; break; - case 197: s = "invalid WhileStmt"; break; - case 198: s = "invalid MatchStmt"; break; - case 199: s = "invalid ForallStmt"; break; - case 200: s = "invalid ForallStmt"; break; - case 201: s = "this symbol not expected in ModifyStmt"; break; - case 202: s = "invalid ModifyStmt"; break; - case 203: s = "invalid ReturnStmt"; break; - case 204: s = "invalid Rhs"; break; - case 205: s = "invalid Lhs"; 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 = "this symbol not expected in LoopSpec"; break; - case 210: s = "this symbol not expected in LoopSpec"; break; - case 211: s = "this symbol not expected in LoopSpec"; break; - case 212: s = "this symbol not expected in Invariant"; 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 RelOp"; break; - case 220: s = "invalid AddOp"; break; - case 221: s = "invalid UnaryExpression"; break; - case 222: s = "invalid UnaryExpression"; break; - case 223: s = "invalid MulOp"; break; - case 224: s = "invalid NegOp"; break; - case 225: s = "invalid EndlessExpression"; break; - case 226: s = "invalid Suffix"; break; - case 227: s = "invalid Suffix"; break; - case 228: s = "invalid Suffix"; break; - case 229: s = "invalid DisplayExpr"; break; - case 230: s = "invalid MultiSetExpr"; break; - case 231: s = "invalid ConstAtomExpression"; break; - case 232: s = "invalid Nat"; break; - case 233: s = "invalid LambdaArrow"; break; - case 234: s = "invalid QSep"; break; - case 235: s = "invalid MatchExpression"; break; - case 236: s = "invalid QuantifierGuts"; break; - case 237: s = "invalid StmtInExpr"; break; - case 238: s = "invalid LetExpr"; break; - case 239: s = "invalid CasePattern"; break; - case 240: s = "invalid Forall"; break; - case 241: s = "invalid Exists"; break; + case 153: s = "this symbol not expected in MethodDecl"; break; + case 154: s = "invalid MethodDecl"; break; + case 155: s = "invalid MethodDecl"; break; + case 156: s = "invalid FIdentType"; break; + case 157: s = "this symbol not expected in OldSemi"; break; + case 158: s = "invalid TypeIdentOptional"; break; + case 159: s = "invalid TypeAndToken"; break; + case 160: s = "this symbol not expected in IteratorSpec"; break; + case 161: s = "invalid IteratorSpec"; break; + case 162: s = "invalid IteratorSpec"; break; + case 163: s = "this symbol not expected in MethodSpec"; break; + case 164: s = "invalid MethodSpec"; break; + case 165: s = "invalid MethodSpec"; break; + case 166: s = "invalid FrameExpression"; break; + case 167: s = "invalid ReferenceType"; break; + case 168: s = "this symbol not expected in FunctionSpec"; break; + case 169: s = "invalid FunctionSpec"; break; + case 170: s = "invalid PossiblyWildFrameExpression"; break; + case 171: s = "invalid PossiblyWildExpression"; break; + case 172: s = "this symbol not expected in OneStmt"; break; + case 173: s = "invalid OneStmt"; break; + case 174: s = "this symbol not expected in OneStmt"; break; + case 175: s = "invalid OneStmt"; break; + case 176: s = "invalid AssertStmt"; break; + case 177: s = "invalid AssumeStmt"; break; + case 178: s = "invalid UpdateStmt"; break; + case 179: s = "invalid UpdateStmt"; break; + case 180: s = "invalid IfStmt"; break; + case 181: s = "invalid IfStmt"; break; + case 182: s = "invalid WhileStmt"; break; + case 183: s = "invalid WhileStmt"; break; + case 184: s = "invalid MatchStmt"; break; + case 185: s = "invalid ForallStmt"; break; + case 186: s = "invalid ForallStmt"; break; + case 187: s = "this symbol not expected in ModifyStmt"; break; + case 188: s = "invalid ModifyStmt"; break; + case 189: s = "invalid ReturnStmt"; break; + case 190: s = "invalid Rhs"; break; + case 191: s = "invalid Lhs"; break; + case 192: s = "invalid Guard"; break; + case 193: s = "this symbol not expected in LoopSpec"; break; + case 194: s = "this symbol not expected in LoopSpec"; break; + case 195: s = "this symbol not expected in Invariant"; break; + case 196: s = "invalid CalcOp"; break; + case 197: s = "invalid EquivOp"; break; + case 198: s = "invalid ImpliesOp"; break; + case 199: s = "invalid ExpliesOp"; break; + case 200: s = "invalid AndOp"; break; + case 201: s = "invalid OrOp"; break; + case 202: s = "invalid RelOp"; break; + case 203: s = "invalid AddOp"; break; + case 204: s = "invalid UnaryExpression"; break; + case 205: s = "invalid UnaryExpression"; break; + case 206: s = "invalid MulOp"; break; + case 207: s = "invalid NegOp"; break; + case 208: s = "invalid EndlessExpression"; break; + case 209: s = "invalid Suffix"; break; + case 210: s = "invalid Suffix"; break; + case 211: s = "invalid Suffix"; break; + case 212: s = "invalid DisplayExpr"; break; + case 213: s = "invalid MultiSetExpr"; break; + case 214: s = "invalid ConstAtomExpression"; break; + case 215: s = "invalid Nat"; break; + case 216: s = "invalid LambdaArrow"; break; + case 217: s = "invalid QSep"; break; + case 218: s = "invalid MatchExpression"; break; + case 219: s = "invalid QuantifierGuts"; break; + case 220: s = "invalid StmtInExpr"; break; + case 221: s = "invalid LetExpr"; break; + case 222: s = "invalid CasePattern"; break; + case 223: s = "invalid Forall"; break; + case 224: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy index 1c1d7299..b11fc0d1 100644 --- a/Test/dafny4/BinarySearch.dfy +++ b/Test/dafny4/BinarySearch.dfy @@ -4,15 +4,15 @@ // Binary search using standard integers method BinarySearch(a: array, key: int) returns (r: int) - requires a != null; - requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; - ensures 0 <= r ==> r < a.Length && a[r] == key; - ensures r < 0 ==> key !in a[..]; + requires a != null + requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j] + ensures 0 <= r ==> r < a.Length && a[r] == key + ensures r < 0 ==> key !in a[..] { var lo, hi := 0, a.Length; while lo < hi - invariant 0 <= lo <= hi <= a.Length; - invariant key !in a[..lo] && key !in a[hi..]; + invariant 0 <= lo <= hi <= a.Length + invariant key !in a[..lo] && key !in a[hi..] { var mid := (lo + hi) / 2; if key < a[mid] { @@ -31,15 +31,15 @@ method BinarySearch(a: array, key: int) returns (r: int) newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000 method BinarySearchInt32_bad(a: array, key: int) returns (r: int32) - requires a != null && a.Length < 0x8000_0000; - requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; - ensures 0 <= r ==> r < int32(a.Length) && a[r] == key; - ensures r < 0 ==> key !in a[..]; + requires a != null && a.Length < 0x8000_0000 + requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j] + ensures 0 <= r ==> r < int32(a.Length) && a[r] == key + ensures r < 0 ==> key !in a[..] { var lo, hi := 0, int32(a.Length); while lo < hi - invariant 0 <= lo <= hi <= int32(a.Length); - invariant key !in a[..lo] && key !in a[hi..]; + invariant 0 <= lo <= hi <= int32(a.Length) + invariant key !in a[..lo] && key !in a[hi..] { var mid := (lo + hi) / 2; // error: possible overflow if key < a[mid] { @@ -54,15 +54,15 @@ method BinarySearchInt32_bad(a: array, key: int) returns (r: int32) } method BinarySearchInt32_good(a: array, key: int) returns (r: int32) - requires a != null && a.Length < 0x8000_0000; - requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; - ensures 0 <= r ==> r < int32(a.Length) && a[r] == key; - ensures r < 0 ==> key !in a[..]; + requires a != null && a.Length < 0x8000_0000 + requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j] + ensures 0 <= r ==> r < int32(a.Length) && a[r] == key + ensures r < 0 ==> key !in a[..] { var lo, hi := 0, int32(a.Length); while lo < hi - invariant 0 <= lo <= hi <= int32(a.Length); - invariant key !in a[..lo] && key !in a[hi..]; + invariant 0 <= lo <= hi <= int32(a.Length) + invariant key !in a[..lo] && key !in a[hi..] { var mid := lo + (hi - lo) / 2; // this is how to do it if key < a[mid] { -- cgit v1.2.3 From bd58ad0dcd2e3745cb74701f494be547189f8d1c Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 25 Oct 2014 01:03:43 -0700 Subject: Marked "free" as soon-to-be-deprecated --- Source/Dafny/Dafny.atg | 16 ++++++++++++---- Source/Dafny/Parser.cs | 16 ++++++++++++---- Test/dafny0/SmallTests.dfy | 8 -------- Test/dafny0/SmallTests.dfy.expect | 30 +++++++++++++++--------------- 4 files changed, 39 insertions(+), 31 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2134ba6d..84f09ee0 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -777,7 +777,9 @@ MethodSpec<.List/*!*/ req, List/ { "," FrameExpression (. mod.Add(fe); .) } ] OldSemi - | [ "free" (. isFree = true; .) + | [ "free" (. isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + .) ] ( "requires" Expression OldSemi (. req.Add(new MaybeFreeExpression(e, isFree)); .) | "ensures" @@ -804,7 +806,9 @@ IteratorSpec<.List/*!*/ reads, List/ { "," FrameExpression (. mod.Add(fe); .) } ] OldSemi - | [ "free" (. isFree = true; .) + | [ "free" (. isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + .) ] [ "yield" (. isYield = true; .) ] @@ -1463,7 +1467,9 @@ LoopSpec<.out List invariants, out List = (. bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; .) SYNC - ["free" (. isFree = true; .) + ["free" (. isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + .) ] "invariant" { IF(IsAttribute()) Attribute } Expression (. invariant = new MaybeFreeExpression(e, isFree, attrs); .) @@ -1609,7 +1615,9 @@ ForallStmt | (. if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } .) ) { (. isFree = false; .) - [ "free" (. isFree = true; .) + [ "free" (. isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + .) ] "ensures" Expression (. ens.Add(new MaybeFreeExpression(e, isFree)); .) OldSemi (. tok = t; .) diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 20f9332d..2358fc79 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1465,7 +1465,9 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } else if (StartOf(14)) { if (la.kind == 54) { Get(); - isFree = true; + isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + } if (la.kind == 57) { Get(); @@ -1543,7 +1545,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 14 || la.kind == 54 || la.kind == 55) { if (la.kind == 54) { Get(); - isFree = true; + isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + } if (la.kind == 14) { Get(); @@ -2226,7 +2230,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo isFree = false; if (la.kind == 54) { Get(); - isFree = true; + isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + } Expect(55); Expression(out e, false, true); @@ -2582,7 +2588,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(195); Get();} if (la.kind == 54) { Get(); - isFree = true; + isFree = true; + errors.Warning(t, "the 'free' keyword is soon to be deprecated"); + } Expect(88); while (IsAttribute()) { diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index d6658671..0482e4ec 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -432,10 +432,6 @@ class AttributeTests { ensures {:boolAttr false} true; ensures {:intAttr 0} true; ensures {:intAttr 1} true; - free ensures {:boolAttr true} true; - free ensures {:boolAttr false} true; - free ensures {:intAttr 0} true; - free ensures {:intAttr 1} true; modifies {:boolAttr true} this`f; modifies {:boolAttr false} this`f; modifies {:intAttr 0} this`f; @@ -459,10 +455,6 @@ class AttributeTests { invariant {:boolAttr false} true; invariant {:intAttr 0} true; invariant {:intAttr 1} true; - free invariant {:boolAttr true} true; - free invariant {:boolAttr false} true; - free invariant {:intAttr 0} true; - free invariant {:intAttr 1} true; modifies {:boolAttr true} this`f; modifies {:boolAttr false} this`f; modifies {:intAttr 0} this`f; diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 1e71ec8b..87cc4a84 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -94,14 +94,14 @@ SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decrease Execution trace: (0,0): anon0 (0,0): anon3_Else -SmallTests.dfy(689,14): Error: assertion violation +SmallTests.dfy(681,14): Error: assertion violation Execution trace: (0,0): anon0 - SmallTests.dfy(686,5): anon7_LoopHead + SmallTests.dfy(678,5): anon7_LoopHead (0,0): anon7_LoopBody - SmallTests.dfy(686,5): anon8_Else + SmallTests.dfy(678,5): anon8_Else (0,0): anon9_Then -SmallTests.dfy(710,14): Error: assertion violation +SmallTests.dfy(702,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon7_Then @@ -133,12 +133,12 @@ SmallTests.dfy(400,41): Related location: This is the postcondition that might n Execution trace: (0,0): anon0 (0,0): anon6_Else -SmallTests.dfy(560,12): Error: assertion violation +SmallTests.dfy(552,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then (0,0): anon2 -SmallTests.dfy(574,20): Error: left-hand sides 0 and 1 may refer to the same location +SmallTests.dfy(566,20): Error: left-hand sides 0 and 1 may refer to the same location Execution trace: (0,0): anon0 (0,0): anon27_Then @@ -150,11 +150,11 @@ Execution trace: (0,0): anon31_Then (0,0): anon32_Then (0,0): anon12 -SmallTests.dfy(576,15): Error: left-hand sides 1 and 2 may refer to the same location +SmallTests.dfy(568,15): Error: left-hand sides 1 and 2 may refer to the same location Execution trace: (0,0): anon0 (0,0): anon27_Then - SmallTests.dfy(569,18): anon28_Else + SmallTests.dfy(561,18): anon28_Else (0,0): anon4 (0,0): anon29_Else (0,0): anon30_Then @@ -165,16 +165,16 @@ Execution trace: (0,0): anon37_Then (0,0): anon22 (0,0): anon38_Then -SmallTests.dfy(583,25): Error: target object may be null +SmallTests.dfy(575,25): Error: target object may be null Execution trace: (0,0): anon0 -SmallTests.dfy(596,10): Error: assertion violation +SmallTests.dfy(588,10): Error: assertion violation Execution trace: (0,0): anon0 -SmallTests.dfy(620,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(612,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 -SmallTests.dfy(643,10): Error: assertion violation +SmallTests.dfy(635,10): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon8_Then @@ -182,17 +182,17 @@ Execution trace: (0,0): anon4 (0,0): anon10_Then (0,0): anon7 -SmallTests.dfy(657,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(649,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then (0,0): anon3 -SmallTests.dfy(659,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(651,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 (0,0): anon5_Else -SmallTests.dfy(672,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(664,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 -- cgit v1.2.3 From 6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 28 Oct 2014 00:11:20 -0700 Subject: Fixed a bug in the Substituter for datatype update expressions. --- Source/Dafny/DafnyAst.cs | 22 +++++++++++++++++++--- Source/Dafny/Resolver.cs | 6 +++--- Source/Dafny/Translator.cs | 14 +++++--------- Test/dafny0/DatatypeUpdate.dfy | 7 +++++++ Test/dafny0/DatatypeUpdate.dfy.expect | 2 +- 5 files changed, 35 insertions(+), 16 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index cbbd2c2e..fa7fde12 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4709,7 +4709,9 @@ namespace Microsoft.Dafny { } /// - /// Returns the non-null subexpressions of the Expression. + /// Returns the non-null subexpressions of the Expression. To be called after the expression has been resolved; this + /// means, for example, that any concrete syntax that resolves to some other expression will return the subexpressions + /// of the resolved expression. /// public virtual IEnumerable SubExpressions { get { yield break; } @@ -5469,11 +5471,26 @@ namespace Microsoft.Dafny { } } + /// + /// Represents an expression of the form A[B := C], where, syntactically, A, B, and C are expressions. + /// Successfully resolved, the expression stands for one of the following: + /// * if A is a sequence, then B is an integer-based index into the sequence and C's type is the sequence element type + /// * if A is a map(T,U), then B is a key of type T and C is a value of type U + /// * if A is a multiset, then B's type is the multiset element type and C is an integer-based numeric + /// * if A is a datatype, then B is the name of a destructor of A's type and C's type is the type of that destructor -- in + /// this case, the resolver will set the ResolvedUpdateExpr to an expression that constructs an appropriate datatype value + /// public class SeqUpdateExpr : Expression { public readonly Expression Seq; public readonly Expression Index; public readonly Expression Value; - public Expression ResolvedUpdateExpr; // May be filled in during resolution + public Expression ResolvedUpdateExpr; // filled in during resolution, if the SeqUpdateExpr corresponds to a datatype update + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Seq != null); + Contract.Invariant(Index != null); + Contract.Invariant(Value != null); + } public SeqUpdateExpr(IToken tok, Expression seq, Expression index, Expression val) : base(tok) { @@ -5484,7 +5501,6 @@ namespace Microsoft.Dafny { Seq = seq; Index = index; Value = val; - ResolvedUpdateExpr = null; } public override IEnumerable SubExpressions { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a2ffec6e..a44491de 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6459,7 +6459,7 @@ namespace Microsoft.Dafny // Build the arguments to the datatype constructor, using the updated value in the appropriate slot List ctor_args = new List(); foreach (Formal d in ctor.Formals) { - if (d.Name == destructor.Name) { + if (d == destructor.CorrespondingFormal) { ctor_args.Add(e.Value); } else { ctor_args.Add(new ExprDotName(expr.tok, tmpVarIdExpr, d.Name)); @@ -8652,8 +8652,8 @@ namespace Microsoft.Dafny } else if (expr is SeqUpdateExpr) { SeqUpdateExpr e = (SeqUpdateExpr)expr; return UsesSpecFeatures(e.Seq) || - (e.Index != null && UsesSpecFeatures(e.Index)) || - (e.Value != null && UsesSpecFeatures(e.Value)); + UsesSpecFeatures(e.Index) || + UsesSpecFeatures(e.Value); } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; if (cce.NonNull(e.Function).IsGhost) { diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index df5b65a0..402a070c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -13022,18 +13022,14 @@ namespace Microsoft.Dafny { } } else if (expr is SeqUpdateExpr) { - SeqUpdateExpr sse = (SeqUpdateExpr)expr; - if (sse.ResolvedUpdateExpr != null) - { - newExpr = Substitute(sse.ResolvedUpdateExpr); - } - else - { + var sse = (SeqUpdateExpr)expr; + if (sse.ResolvedUpdateExpr != null) { + return Substitute(sse.ResolvedUpdateExpr); + } else { Expression seq = Substitute(sse.Seq); Expression index = Substitute(sse.Index); Expression val = Substitute(sse.Value); - if (seq != sse.Seq || index != sse.Index || val != sse.Value) - { + if (seq != sse.Seq || index != sse.Index || val != sse.Value) { newExpr = new SeqUpdateExpr(sse.tok, seq, index, val); } } diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy index 09f07dd3..7869fba3 100644 --- a/Test/dafny0/DatatypeUpdate.dfy +++ b/Test/dafny0/DatatypeUpdate.dfy @@ -21,3 +21,10 @@ method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi: assert abc[myint := abc.myint - 2] == foo[myint := x]; } + +// regression test (for a previous bug in the Translator.Substituter): +datatype Dt = Ctor(x: int, y: bool) +function F(d: Dt): Dt +{ + d[x := 5] +} diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect index 069e7767..52595bf9 100644 --- a/Test/dafny0/DatatypeUpdate.dfy.expect +++ b/Test/dafny0/DatatypeUpdate.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 2 verified, 0 errors +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3 From 655b8311917e38cc2b359bad46def21de7852508 Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 28 Oct 2014 17:44:39 -0700 Subject: Disallow automatic completion of type arguments to the LHS of datatype declarations --- Source/Dafny/Resolver.cs | 5 ++--- Test/dafny0/ResolutionErrors.dfy | 19 +++++++++++++++++++ Test/dafny0/ResolutionErrors.dfy.expect | 4 +++- Test/dafny0/TypeParameters.dfy | 2 +- Test/hofs/Fold.dfy | 2 +- 5 files changed, 26 insertions(+), 6 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a44491de..01ef0a4b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3399,12 +3399,11 @@ namespace Microsoft.Dafny Contract.Requires(ctor != null); Contract.Requires(ctor.EnclosingDatatype != null); Contract.Requires(dtTypeArguments != null); - ResolveTypeOption option = dtTypeArguments.Count == 0 ? new ResolveTypeOption(ctor) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); foreach (Formal p in ctor.Formals) { // In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to // involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint // to obtain a non-null object. - ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), option, dtTypeArguments); + ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), ResolveTypeOptionEnum.AllowPrefix, dtTypeArguments); } } @@ -3894,7 +3893,7 @@ namespace Microsoft.Dafny t.ResolvedClass = dd; } else { // d is a class or datatype, and it may have type parameters - what = "class/datatype"; + what = isArrow ? "function type" : "class/datatype"; t.ResolvedClass = d; } if (option.Opt == ResolveTypeOptionEnum.DontInfer) { diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 79e7ac57..e324393d 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1240,3 +1240,22 @@ module NonInferredTypeVariables { */ } } + +// -------------- signature completion ------------------ + +module SignatureCompletion { + // datatype signatures do not allow auto-declared type parameters on the LHS + datatype Dt = Ctor(X -> Dt) // error: X is not a declared type + datatype Et = Ctor(X -> Et, Y) // error: X is not a declared type + + // For methods and functions, signatures can auto-declare type parameters + method My0(s: set, x: A -> B) + method My1(x: A -> B, s: set) + method My2(s: set, x: A -> B) + method My3(x: A -> B, s: set) + + function F0(s: set, x: A -> B): int + function F1(x: A -> B, s: set): int + function F2(s: set, x: A -> B): int + function F3(x: A -> B, s: set): int +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 1b802687..3b768c84 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -83,6 +83,8 @@ ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecifie ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) +ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts @@ -180,4 +182,4 @@ ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set) ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -182 resolution/type errors detected in ResolutionErrors.dfy +184 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 900b6110..aa3d7671 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -335,7 +335,7 @@ module ArrayTypeMagic { return b[..]; } - datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree) + datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree) datatype AnotherACT = Leaf(array3) | Node(AnotherACT, AnotherACT) datatype OneMoreACT = Leaf(array3) | Node(OneMoreACT, OneMoreACT) diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy index 7ce99e56..50b5569b 100644 --- a/Test/hofs/Fold.dfy +++ b/Test/hofs/Fold.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -datatype List = Nil | Cons(A,List); +datatype List = Nil | Cons(A,List); datatype Expr = Add(List) | Mul(List) | Lit(int); -- cgit v1.2.3 From 8a1cd890191d8e92f0d478445740d9ee24086429 Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 28 Oct 2014 23:19:34 -0700 Subject: Fixed type-inference bug that could create cycles in proxy type graph --- Source/Dafny/Resolver.cs | 49 ++++++++++++++++++++++++++++------------ Test/dafny0/TypeTests.dfy | 25 ++++++++++++++++++++ Test/dafny0/TypeTests.dfy.expect | 5 +++- 3 files changed, 64 insertions(+), 15 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 01ef0a4b..fe7d80d5 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4162,11 +4162,34 @@ namespace Microsoft.Dafny if (t is NatType) { proxy.T = Type.Int; } else { - proxy.T = t; + return AssignProxyAfterCycleCheck(proxy, t); } return true; } + bool AssignProxyAfterCycleCheck(TypeProxy proxy, Type t) { + Contract.Requires(proxy != null && proxy.T == null); + Contract.Requires(t != null); + if (TypeArgumentsIncludeProxy(t, proxy)) { + return false; + } else { + proxy.T = t; + return true; + } + } + + bool TypeArgumentsIncludeProxy(Type t, TypeProxy proxy) { + Contract.Requires(t != null); + Contract.Requires(proxy != null); + foreach (var ta in t.TypeArgs) { + var a = ta.Normalize(); + if (a == proxy || TypeArgumentsIncludeProxy(a, proxy)) { + return true; + } + } + return false; + } + bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b) { Contract.Requires(a != null); Contract.Requires(b != null); @@ -4195,9 +4218,8 @@ namespace Microsoft.Dafny // Note, we're calling ResolvedArrayType here, which in turn calls ResolveType on ib.Arg. However, we // don't need to worry about what ICodeContext we're passing in, because ib.Arg should already have been // resolved. - a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg, new DontUseICallable()); - b.T = a.T; - return UnifyTypes(ib.Arg, ib.Range); + var c = ResolvedArrayType(Token.NoToken, 1, ib.Arg, new DontUseICallable()); + return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c) && UnifyTypes(ib.Arg, ib.Range); } else { return false; } @@ -4212,8 +4234,8 @@ namespace Microsoft.Dafny b.T = a; // a is a stronger constraint than b } else { // a says set,seq and b says numeric,set; the intersection is set - a.T = new SetType(((CollectionTypeProxy)a).Arg); - b.T = a.T; + var c = new SetType(((CollectionTypeProxy)a).Arg); + return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } return true; } else if (b is IndexableTypeProxy) { @@ -4256,8 +4278,9 @@ namespace Microsoft.Dafny a.T = b; // b has the stronger requirement } else { Type c = !i && !r && h && !q && !s ? new CharType() : (Type)new OperationTypeProxy(i, r, h, q, s); - a.T = c; - b.T = c; + // the calls to AssignProxyAfterCycleCheck are needed only when c is a non-proxy type, but it doesn't + // hurt to do them in both cases + return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } return true; } else { @@ -4267,14 +4290,12 @@ namespace Microsoft.Dafny // So, the intersection could include multiset and seq. if (pa.AllowSetVarieties && !pa.AllowSeq) { // strengthen a and b to a multiset type - b.T = new MultiSetType(ib.Arg); - a.T = b.T; - return true; + var c = new MultiSetType(ib.Arg); + return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } else if (pa.AllowSeq && !pa.AllowSetVarieties) { // strengthen a and b to a sequence type - b.T = new SeqType(ib.Arg); - a.T = b.T; - return true; + var c = new SeqType(ib.Arg); + return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } else if (!pa.AllowSeq && !pa.AllowSetVarieties) { // over-constrained return false; diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 6086fcf1..141e48cb 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -144,3 +144,28 @@ ghost method GhostM() returns (x: int) { x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason) } + +// ------------------ cycles that could arise from proxy assignments --------- + +module ProxyCycles { + datatype Dt = Ctor(X -> Dt) + method M0() + { + var dt: Dt; + var f := x => x; + dt := Ctor(f); // error: cannot infer a type for f + } + method M1() + { + var dt: Dt; + var f := x => x; + dt := Ctor(f); // error: cannot infer a type for f + } + + function method F(x: X): set + method N() + { + var x; + x := F(x); // error: cannot infer type for x + } +} diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 5d78fe16..55fc916c 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,3 +1,6 @@ +TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt) +TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt) +TypeTests.dfy(169,6): Error: RHS (of type set) not assignable to LHS (of type ?) TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D) TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C) TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int) @@ -31,4 +34,4 @@ TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed -33 resolution/type errors detected in TypeTests.dfy +36 resolution/type errors detected in TypeTests.dfy -- cgit v1.2.3 From 50d02a2fd7f19664bdde27f698d5ff061472118d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 29 Oct 2014 14:29:47 -0700 Subject: Fix bug in translation of 'new' for arrays --- Source/Dafny/Translator.cs | 2 +- Test/dafny0/Array.dfy | 32 +++++++++++++++++++++++++++++--- Test/dafny0/Array.dfy.expect | 10 +++++++++- 3 files changed, 39 insertions(+), 5 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 402a070c..76da73cd 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -9512,7 +9512,7 @@ namespace Microsoft.Dafny { // assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS; Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null); Bpl.Expr rightType; - rightType = etran.GoodRef_(tok, nw, tRhs.EType, true); + rightType = etran.GoodRef_(tok, nw, tRhs.Type, true); builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType))); if (tRhs.ArrayDimensions != null) { int i = 0; diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index f6477708..391ca5f7 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -42,12 +42,12 @@ class A { assert zz2 != zz0; // holds because zz2 is newly allocated var o: object := zz0; assert this != o; // holds because zz0 has a different type - /****** This would be a good thing to be able to verify, but the current encoding is not up to the task + if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) { o := zz1[1]; assert zz0[1] == o ==> o == null; // holds because zz0 and zz1 have different element types } - ******/ + assert zz2[20] == null; // error: no reason that this must hold } @@ -152,7 +152,7 @@ class A { ensures fresh(b) && Q1(b[..]); } -type B; +class B { } // ------------------------------- @@ -301,3 +301,29 @@ method AllocationBusiness2(a: array2, i: int, j: int) var c := new MyClass; assert c !in a[i,j].Repr; // the proof requires allocation axioms for multi-dim arrays } + +// ------- a regression test, testing that dtype is set correctly after allocation ------ + +module DtypeRegression { + predicate array_equal(a: array, b: array) + requires a != null && b != null; + reads a, b; + { + a[..] == b[..] + } + + method duplicate_array(input: array, len: int) returns (output: array) + requires input != null && len == input.Length; + ensures output != null && array_equal(input, output); + { + output := new int[len]; + var i := 0; + while i < len + invariant 0 <= i <= len; + invariant forall j :: 0 <= j < i ==> output[j] == input[j]; + { + output[i] := input[i]; + i := i + 1; + } + } +} diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect index 081fd258..bf4da25f 100644 --- a/Test/dafny0/Array.dfy.expect +++ b/Test/dafny0/Array.dfy.expect @@ -13,6 +13,14 @@ Execution trace: Array.dfy(51,20): Error: assertion violation Execution trace: (0,0): anon0 + (0,0): anon12_Then + (0,0): anon13_Then + (0,0): anon14_Then + (0,0): anon6 + (0,0): anon15_Then + (0,0): anon16_Then + (0,0): anon9 + (0,0): anon11 Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 @@ -104,4 +112,4 @@ Execution trace: (0,0): anon2 (0,0): anon6_Then -Dafny program verifier finished with 46 verified, 20 errors +Dafny program verifier finished with 49 verified, 20 errors -- cgit v1.2.3 From c612305e78f057b9d1e91a0d154989cb866a7906 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 29 Oct 2014 23:16:58 -0700 Subject: Resolve attributes of a forall statement only after bound variables have been added to the scope. Resolve the attributes of local variables. Don't resolve attributes of PredicateStmt's more than once. --- Source/Dafny/Resolver.cs | 9 +++++++-- Test/dafny0/SmallTests.dfy | 17 +++++++++++++---- Test/dafny0/SmallTests.dfy.expect | 30 +++++++++++++++--------------- 3 files changed, 35 insertions(+), 21 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index fe7d80d5..f9cd899f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4354,10 +4354,11 @@ namespace Microsoft.Dafny public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); - ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true)); + if (!(stmt is ForallStmt)) { // forall statements do their own attribute resolution below + ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true)); + } if (stmt is PredicateStmt) { PredicateStmt s = (PredicateStmt)stmt; - ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, false)); s.IsGhost = true; ResolveExpression(s.Expr, new ResolveOpts(codeContext, true)); Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression @@ -4514,6 +4515,10 @@ namespace Microsoft.Dafny Error(local.Tok, "Duplicate local-variable name: {0}", local.Name); } } + // With the new locals in scope, it's now time to resolve the attributes on all the locals + foreach (var local in s.Locals) { + ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true)); + } // Resolve the AssignSuchThatStmt, if any if (s.Update is AssignSuchThatStmt) { ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext); diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 0482e4ec..7d8628a9 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -497,6 +497,15 @@ class AttributeTests { } else { return new AttributeTests.C() {:intAttr 0}; } + + // forall statements resolve their attributes once the bound variables have been + // added to the scope + var y: bool, x: real; + var aa := new real[120]; + forall y: int, x, z {:trgr x == y} {:tri z == z} | x < y // the range will infer the type of x + ensures z && 0 <= x < aa.Length ==> aa[x] == 0.0; // ensures clause will infer type of z + { + } } } @@ -504,10 +513,10 @@ class AttributeTests { static method TestAttributesVarDecls() { - var {:foo} foo := null; - var {:bar} bar := 0; - var {:foo} {:bar} foobar : set := {}; - var {:baz} baz, {:foobaz} foobaz := true, false; + var {:foo foo} foo := null; + var {:bar bar} bar := 0; + var {:foo foobar} {:bar foobar} foobar : set := {}; + var {:baz baz && foobaz} baz, {:foobaz foobaz != baz} foobaz := true, false; } // ----------------------- Pretty printing of !(!expr) -------- diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 87cc4a84..824ad991 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -94,14 +94,14 @@ SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decrease Execution trace: (0,0): anon0 (0,0): anon3_Else -SmallTests.dfy(681,14): Error: assertion violation +SmallTests.dfy(690,14): Error: assertion violation Execution trace: (0,0): anon0 - SmallTests.dfy(678,5): anon7_LoopHead + SmallTests.dfy(687,5): anon7_LoopHead (0,0): anon7_LoopBody - SmallTests.dfy(678,5): anon8_Else + SmallTests.dfy(687,5): anon8_Else (0,0): anon9_Then -SmallTests.dfy(702,14): Error: assertion violation +SmallTests.dfy(711,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon7_Then @@ -133,12 +133,12 @@ SmallTests.dfy(400,41): Related location: This is the postcondition that might n Execution trace: (0,0): anon0 (0,0): anon6_Else -SmallTests.dfy(552,12): Error: assertion violation +SmallTests.dfy(561,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then (0,0): anon2 -SmallTests.dfy(566,20): Error: left-hand sides 0 and 1 may refer to the same location +SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location Execution trace: (0,0): anon0 (0,0): anon27_Then @@ -150,11 +150,11 @@ Execution trace: (0,0): anon31_Then (0,0): anon32_Then (0,0): anon12 -SmallTests.dfy(568,15): Error: left-hand sides 1 and 2 may refer to the same location +SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location Execution trace: (0,0): anon0 (0,0): anon27_Then - SmallTests.dfy(561,18): anon28_Else + SmallTests.dfy(570,18): anon28_Else (0,0): anon4 (0,0): anon29_Else (0,0): anon30_Then @@ -165,16 +165,16 @@ Execution trace: (0,0): anon37_Then (0,0): anon22 (0,0): anon38_Then -SmallTests.dfy(575,25): Error: target object may be null +SmallTests.dfy(584,25): Error: target object may be null Execution trace: (0,0): anon0 -SmallTests.dfy(588,10): Error: assertion violation +SmallTests.dfy(597,10): Error: assertion violation Execution trace: (0,0): anon0 -SmallTests.dfy(612,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 -SmallTests.dfy(635,10): Error: assertion violation +SmallTests.dfy(644,10): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon8_Then @@ -182,17 +182,17 @@ Execution trace: (0,0): anon4 (0,0): anon10_Then (0,0): anon7 -SmallTests.dfy(649,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(658,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then (0,0): anon3 -SmallTests.dfy(651,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(660,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 (0,0): anon5_Else -SmallTests.dfy(664,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate +SmallTests.dfy(673,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate Execution trace: (0,0): anon0 -- cgit v1.2.3 From 9f41b35b514eba87a037cbada83f0c294eafb936 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 30 Oct 2014 15:12:31 -0700 Subject: Allow assignment LHSs in a forall statement to be the same, so long as the they are assigned the same RHS value. Don't include havoc assignments in LHS-duplicate checks. --- Source/Dafny/Resolver.cs | 9 +---- Source/Dafny/Translator.cs | 65 +++++++++++++++++++++------------ Test/dafny0/LhsDuplicates.dfy | 70 ++++++++++++++++++++++++++++++++++++ Test/dafny0/LhsDuplicates.dfy.expect | 28 +++++++++++++++ 4 files changed, 141 insertions(+), 31 deletions(-) create mode 100644 Test/dafny0/LhsDuplicates.dfy create mode 100644 Test/dafny0/LhsDuplicates.dfy.expect (limited to 'Test') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f9cd899f..818bdcc4 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -5111,6 +5111,7 @@ namespace Microsoft.Dafny var update = s as UpdateStmt; var lhsNameSet = new HashSet(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification) + var i = 0; foreach (var lhs in s.Lhss) { var ec = ErrorCount; ResolveExpression(lhs, new ResolveOpts(codeContext, true)); @@ -5121,14 +5122,6 @@ namespace Microsoft.Dafny if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) { Error(lhs, "cannot assign to a range of array elements (try the 'forall' statement)"); } - var ie = lhs.Resolved as IdentifierExpr; - if (ie != null) { - if (lhsNameSet.Contains(ie.Name)) { - Error(update, "duplicate variable in left-hand side of call statement: {0}", ie.Name); - } else { - lhsNameSet.Add(ie.Name); - } - } } } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 76da73cd..0a83499c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -6964,7 +6964,7 @@ namespace Microsoft.Dafny { // ProcessLhss has laid down framing conditions and the ProcessUpdateAssignRhss will check subranges (nats), // but we need to generate the distinctness condition (two LHS are equal only when the RHS is also // equal). We need both the LHS and the RHS to do this, which is why we need to do it here. - CheckLhssDistinctness(finalRhss, lhss, builder, etran, lhsObjs, lhsFields, lhsNames); + CheckLhssDistinctness(finalRhss, s.Rhss, lhss, builder, etran, lhsObjs, lhsFields, lhsNames); // Now actually perform the assignments to the LHS. for (int i = 0; i < lhss.Count; i++) { lhsBuilder[i](finalRhss[i], builder, etran); @@ -7491,9 +7491,9 @@ namespace Microsoft.Dafny { // assume Range[x,y := x',y']; // assume !(x == x' && y == y'); // (a) - // assert E(x,y) != E(x',y'); + // assert E(x,y) != E(x',y') || G(x,y) == G(x',y'); // (b) - // assert !( A(x,y)==A(x',y') && I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... ); + // assert !( A(x,y)==A(x',y') && I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... ) || G(x,y) == G(x',y'); // // assume false; // @@ -7566,24 +7566,31 @@ namespace Microsoft.Dafny { } // check for duplicate LHSs - var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran); - var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime); - range = Substitute(s.Range, null, substMapPrime); - definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); - // assume !(x == x' && y == y'); - Bpl.Expr eqs = Bpl.Expr.True; - foreach (var bv in s.BoundVars) { - var x = substMap[bv]; - var xPrime = substMapPrime[bv]; - // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too? - eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime))); - } - definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs))); - Bpl.Expr objPrime, FPrime; - GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime); - definedness.Add(Assert(s0.Tok, - Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)), - "left-hand sides for different forall-statement bound variables may refer to the same location")); + if (s0.Rhs is ExprRhs) { // if Rhs denotes a havoc, then no duplicate check is performed + var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran); + var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime); + range = Substitute(s.Range, null, substMapPrime); + definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); + // assume !(x == x' && y == y'); + Bpl.Expr eqs = Bpl.Expr.True; + foreach (var bv in s.BoundVars) { + var x = substMap[bv]; + var xPrime = substMapPrime[bv]; + // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too? + eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime))); + } + definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs))); + Bpl.Expr objPrime, FPrime; + GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime); + var Rhs = ((ExprRhs)s0.Rhs).Expr; + var rhs = etran.TrExpr(Substitute(Rhs, null, substMap)); + var rhsPrime = etran.TrExpr(Substitute(Rhs, null, substMapPrime)); + definedness.Add(Assert(s0.Tok, + Bpl.Expr.Or( + Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)), + Bpl.Expr.Eq(rhs, rhsPrime)), + "left-hand sides for different forall-statement bound variables may refer to the same location")); + } definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); @@ -9230,9 +9237,14 @@ namespace Microsoft.Dafny { } - private void CheckLhssDistinctness(List rhs, List lhss, StmtListBuilder builder, ExpressionTranslator etran, + private void CheckLhssDistinctness(List rhs, List rhsOriginal, List lhss, + StmtListBuilder builder, ExpressionTranslator etran, Bpl.Expr[] objs, Bpl.Expr[] fields, string[] names) { - Contract.Requires(cce.NonNullElements(lhss)); + Contract.Requires(rhs != null); + Contract.Requires(rhsOriginal != null); + Contract.Requires(lhss != null); + Contract.Requires(rhs.Count == rhsOriginal.Count); + Contract.Requires(lhss.Count == rhsOriginal.Count); Contract.Requires(builder != null); Contract.Requires(etran != null); Contract.Requires(predef != null); @@ -9240,10 +9252,14 @@ namespace Microsoft.Dafny { for (int i = 0; i < lhss.Count; i++) { var lhs = lhss[i]; Contract.Assume(!(lhs is ConcreteSyntaxExpression)); + if (rhsOriginal[i] is HavocRhs) { + continue; + } IToken tok = lhs.tok; if (lhs is IdentifierExpr) { for (int j = 0; j < i; j++) { + if (rhsOriginal[j] is HavocRhs) { continue; } var prev = lhss[j] as IdentifierExpr; if (prev != null && names[i] == names[j]) { builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.True, Bpl.Expr.Eq(rhs[i], rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must be assigned the same value", j, i))); @@ -9253,6 +9269,7 @@ namespace Microsoft.Dafny { var fse = (MemberSelectExpr)lhs; // check that this LHS is not the same as any previous LHSs for (int j = 0; j < i; j++) { + if (rhsOriginal[j] is HavocRhs) { continue; } var prev = lhss[j] as MemberSelectExpr; var field = fse.Member as Field; Contract.Assert(field != null); @@ -9265,6 +9282,7 @@ namespace Microsoft.Dafny { SeqSelectExpr sel = (SeqSelectExpr)lhs; // check that this LHS is not the same as any previous LHSs for (int j = 0; j < i; j++) { + if (rhsOriginal[j] is HavocRhs) { continue; } var prev = lhss[j] as SeqSelectExpr; if (prev != null) { builder.Add(Assert(tok, @@ -9276,6 +9294,7 @@ namespace Microsoft.Dafny { MultiSelectExpr mse = (MultiSelectExpr)lhs; // check that this LHS is not the same as any previous LHSs for (int j = 0; j < i; j++) { + if (rhsOriginal[j] is HavocRhs) { continue; } var prev = lhss[j] as MultiSelectExpr; if (prev != null) { builder.Add(Assert(tok, diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy new file mode 100644 index 00000000..6a84c5a5 --- /dev/null +++ b/Test/dafny0/LhsDuplicates.dfy @@ -0,0 +1,70 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class MyClass { + var f: T; +} + +method M() +{ + var a, b := new T[100], new T[100]; + forall i | 0 <= i < 100 { + a[3] := *; // RHS is * -- this is okay + } + forall i | 0 <= i < 100 { + a[0] := b[0]; // RHSs are the same -- this is okay + } + forall i | 0 <= i < 100 { + a[0] := b[i]; // error: LHS's may be the same (while RHSs are different) + } +} + +method N(a: MyClass, b: MyClass) + requires a != null && b != null; + modifies a, b; +{ + var q := [a, b]; + forall i | 0 <= i < 2 { + q[0].f := *; // RHS is * -- this is okay + } + forall i | 0 <= i < 2 { + q[0].f := q[0].f; // RHSs are the same -- this is okay + } + forall i | 0 <= i < 2 { + q[0].f := q[i].f; // error: LHS's may be the same (while RHSs are different) + } +} + +method P(t0: T, t1: T, t2: T) { + var a: T, b: T; + a, a, a := *, t0, *; // only one non-* RHS per variable -- this is okay + a, a, b, a, b := *, t1, t2, *, *; // only one non-* RHS per variable -- this is okay + a, a, b, a, b := *, t1, t2, t0, *; // error: duplicate LHS -- t0 and t1 may be different +} + +method Q(c0: MyClass, c1: MyClass) + requires c0 != null && c1 != null; + modifies c0, c1; +{ + c0.f, c1.f := c0.f, c0.f; // okay -- RHSs are the same + c0.f, c0.f, c0.f, c0.f := *, *, c1.f, *; // okay -- only one RHS is non-* + c0.f, c0.f, c0.f, c0.f := c0.f, *, c1.f, *; // error -- duplicate LHR +} + +method R(i: nat, j: nat) + requires i < 10 && j < 10; +{ + var a := new T[10]; + a[i], a[j] := a[5], a[5]; // okay -- RHSs are the same + a[i], a[i], a[i], a[i] := *, *, a[5], *; // okay -- only one RHS is non-* + a[i], a[i], a[i], a[j] := *, a[i], a[j], a[i]; // error -- possible duplicate LHS +} + +method S(i: nat, j: nat) + requires i < 10 && j < 20; +{ + var a := new T[10,20]; + a[i,j], a[i,i] := a[5,7], a[5,7]; // okay -- RHSs are the same + a[i,j], a[i,j], a[i,j], a[i,j] := *, *, a[5,7], *; // okay -- only one RHS is non-* + a[i,j], a[i,j], a[i,j], a[i,i] := *, a[i,i], a[i,j], a[i,i]; // error -- possible duplicate LHS +} diff --git a/Test/dafny0/LhsDuplicates.dfy.expect b/Test/dafny0/LhsDuplicates.dfy.expect new file mode 100644 index 00000000..a864390f --- /dev/null +++ b/Test/dafny0/LhsDuplicates.dfy.expect @@ -0,0 +1,28 @@ +LhsDuplicates.dfy(18,10): Error: left-hand sides for different forall-statement bound variables may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon16_Else + (0,0): anon18_Else + (0,0): anon21_Then + (0,0): anon13 +LhsDuplicates.dfy(34,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon16_Else + (0,0): anon18_Else + (0,0): anon21_Then + (0,0): anon13 +LhsDuplicates.dfy(42,12): Error: when left-hand sides 1 and 3 refer to the same location, they must be assigned the same value +Execution trace: + (0,0): anon0 +LhsDuplicates.dfy(51,18): Error: when left-hand sides 0 and 2 refer to the same location, they must be assigned the same value +Execution trace: + (0,0): anon0 +LhsDuplicates.dfy(60,16): Error: when left-hand sides 1 and 2 may refer to the same location, they must be assigned the same value +Execution trace: + (0,0): anon0 +LhsDuplicates.dfy(69,20): Error: when left-hand sides 1 and 2 refer to the same location, they must be assigned the same value +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 6 verified, 6 errors -- cgit v1.2.3 From daba15309feaed1ea06b6b2d9e3205c933010098 Mon Sep 17 00:00:00 2001 From: leino Date: Fri, 31 Oct 2014 22:41:44 -0700 Subject: Improved power of axioms Seq#FromArray --- Binaries/DafnyPrelude.bpl | 29 +++++++++--- Test/dafny0/SeqFromArray.dfy | 90 +++++++++++++++++++++++++++++++++++++ Test/dafny0/SeqFromArray.dfy.expect | 5 +++ 3 files changed, 119 insertions(+), 5 deletions(-) create mode 100644 Test/dafny0/SeqFromArray.dfy create mode 100644 Test/dafny0/SeqFromArray.dfy.expect (limited to 'Test') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 91d8a01a..eea23383 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -872,7 +872,10 @@ axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) && (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s))); -axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25} +axiom (forall s: Seq T, n: int, j: int :: + {:weight 25} + { Seq#Index(Seq#Take(s,n), j) } + { Seq#Index(s, j), Seq#Take(s,n) } 0 <= j && j < n && j < Seq#Length(s) ==> Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j)); @@ -881,9 +884,16 @@ axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) && (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0)); -axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25} +axiom (forall s: Seq T, n: int, j: int :: + {:weight 25} + { Seq#Index(Seq#Drop(s,n), j) } 0 <= n && 0 <= j && j < Seq#Length(s)-n ==> Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n)); +axiom (forall s: Seq T, n: int, k: int :: + {:weight 25} + { Seq#Index(s, k), Seq#Drop(s,n) } + 0 <= n && n <= k && k < Seq#Length(s) ==> + Seq#Index(Seq#Drop(s,n), k-n) == Seq#Index(s, k)); axiom (forall s, t: Seq T :: { Seq#Append(s, t) } @@ -894,9 +904,18 @@ function Seq#FromArray(h: Heap, a: ref): Seq Box; axiom (forall h: Heap, a: ref :: { Seq#Length(Seq#FromArray(h,a)) } Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a)); -axiom (forall h: Heap, a: ref, i: int :: - { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } - 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))); +axiom (forall h: Heap, a: ref :: + { Seq#FromArray(h, a) } + (forall i: int :: + // it's important to include both triggers, so that assertions about the + // the relation between the array and the sequence can be proved in either + // direction + { read(h, a, IndexField(i)) } + { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } + 0 <= i && + i < Seq#Length(Seq#FromArray(h, a)) // this will trigger the previous axiom to get a connection with _System.array.Length(a) + ==> + Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); axiom (forall h0, h1: Heap, a: ref :: { Seq#FromArray(h1, a), $HeapSucc(h0, h1) } $IsGoodHeap(h0) && $IsGoodHeap(h1) && $HeapSucc(h0, h1) && diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy new file mode 100644 index 00000000..d4c98424 --- /dev/null +++ b/Test/dafny0/SeqFromArray.dfy @@ -0,0 +1,90 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Main() { } + +method H(a: array, c: array, n: nat, j: nat) + requires a != null && c != null + requires j < n == a.Length == c.Length +{ + var A := a[..]; + var C := c[..]; + + if { + case A[j] == C[j] => + assert a[j] == c[j]; + case forall i :: 0 <= i < n ==> A[i] == C[i] => + assert a[j] == c[j]; + case forall i :: 0 <= i < n ==> A[i] == C[i] => + assert forall i :: 0 <= i < n ==> a[i] == c[i]; + case A == C => + assert forall i :: 0 <= i < n ==> A[i] == C[i]; + case A == C => + assert forall i :: 0 <= i < n ==> a[i] == c[i]; + case true => + } +} + +method K(a: array, c: array, n: nat) + requires a != null && c != null + requires n <= a.Length && n <= c.Length +{ + var A := a[..n]; + var C := c[..n]; + if { + case A == C => + assert forall i :: 0 <= i < n ==> A[i] == C[i]; + case A == C => + assert forall i :: 0 <= i < n ==> a[i] == c[i]; + case true => + } +} + +method L(a: array, c: array, n: nat) + requires a != null && c != null + requires n <= a.Length == c.Length +{ + var A := a[n..]; + var C := c[n..]; + var h := a.Length - n; + if { + case A == C => + assert forall i :: 0 <= i < h ==> A[i] == C[i]; + case A == C => + assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i]; + case true => + } +} + +method M(a: array, c: array, m: nat, n: nat, k: nat, l: nat) + requires a != null && c != null + requires k + m <= a.Length; + requires l + n <= c.Length +{ + if { + case true => + var A := a[k..k+m]; + var C := c[l..l+n]; + if A == C { + if * { + assert m == n; + } else if * { + assert forall i :: 0 <= i < n ==> A[i] == C[i]; + } else if * { + assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k]; + } else if * { + assert forall i :: 0 <= i < n ==> A[i] == a[k+i]; + } else if * { + assert forall i :: 0 <= i < n ==> C[i] == c[l+i]; + } else if * { + assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i]; + } + } + case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] => + assert a[k..k+m] == c[l+k..l+k+m]; + case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] => + assert a[..m] == c[l..l+m]; + case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] => + assert a[k..] == c[l+k..l+a.Length]; + } +} diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect new file mode 100644 index 00000000..af845d3e --- /dev/null +++ b/Test/dafny0/SeqFromArray.dfy.expect @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 10 verified, 0 errors +Program compiled successfully +Running... + -- cgit v1.2.3 From 6e5fb70941531435489c1dc533d7caea9120a3d5 Mon Sep 17 00:00:00 2001 From: chmaria Date: Sat, 1 Nov 2014 13:59:31 +0100 Subject: Added initial support for dirty while statements. --- Source/Dafny/Compiler.cs | 10 +- Source/Dafny/Dafny.atg | 13 +- Source/Dafny/DafnyAst.cs | 27 ++- Source/Dafny/Parser.cs | 180 +++++++++--------- Source/Dafny/Printer.cs | 34 ++-- Source/Dafny/Resolver.cs | 69 ++++--- Source/Dafny/Scanner.cs | 12 +- Source/Dafny/Translator.cs | 390 +++++++++++++++++++------------------- Test/dafny0/DirtyLoops.dfy | 17 +- Test/dafny0/DirtyLoops.dfy.expect | 2 +- 10 files changed, 405 insertions(+), 349 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 9d2cad2f..0c670062 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1120,6 +1120,11 @@ namespace Microsoft.Dafny { if (s.Body == null) { compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line); } + } else if (stmt is WhileStmt) { + var s = (WhileStmt)stmt; + if (s.Body == null) { + compiler.Error("a while statement without a body cannot be compiled (line {0})", stmt.Tok.line); + } } } } @@ -1388,6 +1393,9 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) { WhileStmt s = (WhileStmt)stmt; + if (s.Body == null) { + return; + } if (s.Guard == null) { Indent(indent); wr.WriteLine("while (false) { }"); @@ -2515,7 +2523,7 @@ namespace Microsoft.Dafny { var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i); wr.Write("Dafny.Helpers.Let<"); wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type)); - wr.Write(">("); + wr.Write(">("); TrExpr(e.RHSs[i]); wr.Write(", " + rhsName + " => "); neededCloseParens++; diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 18ac5e16..690f8403 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1407,6 +1407,7 @@ WhileStmt IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken; List alternatives; stmt = dummyStmt; // to please the compiler + bool isDirtyLoop = true; .) "while" (. x = t; .) ( @@ -1419,22 +1420,24 @@ WhileStmt | "..." (. guardEllipsis = t; .) ) LoopSpec - ( BlockStmt (. endTok = body.EndTok; .) - | "..." (. bodyEllipsis = t; endTok = t; .) - ) + [ BlockStmt (. endTok = body.EndTok; isDirtyLoop = false; .) + | "..." (. bodyEllipsis = t; endTok = t; isDirtyLoop = false; .) + ] (. if (guardEllipsis != null || bodyEllipsis != null) { if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); } - if (body == null) { + if (body == null && !isDirtyLoop) { body = new BlockStmt(x, endTok, new List()); } stmt = new WhileStmt(x, endTok, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body); stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis); } else { // The following statement protects against crashes in case of parsing errors - body = body ?? new BlockStmt(x, endTok, new List()); + if (body == null && !isDirtyLoop) { + body = new BlockStmt(x, endTok, new List()); + } stmt = new WhileStmt(x, endTok, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index fa7fde12..5b0e168e 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -714,7 +714,7 @@ namespace Microsoft.Dafny { s += Result.TypeName(context); return s; } - + public override bool SupportsEquality { get { return false; @@ -3995,10 +3995,6 @@ namespace Microsoft.Dafny { { public readonly Expression Guard; public readonly BlockStmt Body; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Body != null); - } public WhileStmt(IToken tok, IToken endTok, Expression guard, List invariants, Specification decreases, Specification mod, @@ -4006,14 +4002,15 @@ namespace Microsoft.Dafny { : base(tok, endTok, invariants, decreases, mod) { Contract.Requires(tok != null); Contract.Requires(endTok != null); - Contract.Requires(body != null); this.Guard = guard; this.Body = body; } public override IEnumerable SubStatements { get { - yield return Body; + if (Body != null) { + yield return Body; + } } } public override IEnumerable SubExpressions { @@ -5361,7 +5358,7 @@ namespace Microsoft.Dafny { public readonly Expression Obj; public readonly string MemberName; public MemberDecl Member; // filled in by resolution, will be a Field or Function - public List TypeApplication; + public List TypeApplication; // If it is a function, it must have all its polymorphic variables applied [ContractInvariantMethod] @@ -5539,7 +5536,7 @@ namespace Microsoft.Dafny { } } - public ApplyExpr(IToken tok, IToken openParen, Expression receiver, List args) + public ApplyExpr(IToken tok, IToken openParen, Expression receiver, List args) : base(tok) { OpenParen = openParen; @@ -6206,7 +6203,7 @@ namespace Microsoft.Dafny { } } public String Refresh(String s, ref int counter) { - return s + "#" + counter++ + FullName; + return s + "#" + counter++ + FullName; } public TypeParameter Refresh(TypeParameter p, ref int counter) { var cp = new TypeParameter(p.tok, counter++ + "#" + p.Name, p.EqualitySupport); @@ -6312,13 +6309,13 @@ namespace Microsoft.Dafny { public readonly List Reads; public string MkName(string nm) { - return "$l" + lamUniques++ + "#" + nm; + return "$l" + lamUniques++ + "#" + nm; } public LambdaExpr(IToken tok, bool oneShot, List bvars, Expression requires, List reads, Expression body) - : base(tok, bvars, requires, body, null) + : base(tok, bvars, requires, body, null) { - Contract.Requires(reads != null); + Contract.Requires(reads != null); Reads = reads; OneShot = oneShot; } @@ -6739,13 +6736,13 @@ namespace Microsoft.Dafny { public class TypeExpr : ParensExpression { public readonly Type T; - public TypeExpr(IToken tok, Expression e, Type t) + public TypeExpr(IToken tok, Expression e, Type t) : base(tok, e) { Contract.Requires(t != null); T = t; } - + public static Expression MaybeTypeExpr(Expression e, Type t) { if (t == null) { return e; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index db32e726..f990f9ff 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2115,6 +2115,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken; List alternatives; stmt = dummyStmt; // to please the compiler + bool isDirtyLoop = true; Expect(87); x = t; @@ -2131,29 +2132,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo guardEllipsis = t; } LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs); - if (la.kind == 15) { - BlockStmt(out body, out bodyStart, out bodyEnd); - endTok = body.EndTok; - } else if (la.kind == 45) { - Get(); - bodyEllipsis = t; endTok = t; - } else SynErr(182); + if (la.kind == 15 || la.kind == 45) { + if (la.kind == 15) { + BlockStmt(out body, out bodyStart, out bodyEnd); + endTok = body.EndTok; isDirtyLoop = false; + } else { + Get(); + bodyEllipsis = t; endTok = t; isDirtyLoop = false; + } + } if (guardEllipsis != null || bodyEllipsis != null) { if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); } - if (body == null) { + if (body == null && !isDirtyLoop) { body = new BlockStmt(x, endTok, new List()); } stmt = new WhileStmt(x, endTok, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body); stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis); } else { // The following statement protects against crashes in case of parsing errors - body = body ?? new BlockStmt(x, endTok, new List()); + if (body == null && !isDirtyLoop) { + body = new BlockStmt(x, endTok, new List()); + } stmt = new WhileStmt(x, endTok, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } - } else SynErr(183); + } else SynErr(182); } void MatchStmt(out Statement/*!*/ s) { @@ -2177,7 +2182,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(16); } else if (StartOf(22)) { if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } - } else SynErr(184); + } else SynErr(183); s = new MatchStmt(x, t, e, cases, usesOptionalBrace); } @@ -2203,7 +2208,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(185); + } else SynErr(184); if (la.kind == 17) { Get(); usesOptionalParen = true; @@ -2221,7 +2226,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); } else if (StartOf(23)) { if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } - } else SynErr(186); + } else SynErr(185); while (la.kind == 54 || la.kind == 55) { isFree = false; if (la.kind == 54) { @@ -2339,10 +2344,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 15) { BlockStmt(out body, out bodyStart, out endTok); } else if (la.kind == 10) { - while (!(la.kind == 0 || la.kind == 10)) {SynErr(187); Get();} + while (!(la.kind == 0 || la.kind == 10)) {SynErr(186); Get();} Get(); endTok = t; - } else SynErr(188); + } else SynErr(187); s = new ModifyStmt(tok, endTok, mod, attrs, body); if (ellipsisToken != null) { s = new SkeletonStatement(s, ellipsisToken, null); @@ -2362,7 +2367,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 57) { Get(); returnTok = t; isYield = true; - } else SynErr(189); + } else SynErr(188); if (StartOf(26)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); @@ -2464,7 +2469,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(17)) { Expression(out e, false, true); r = new ExprRhs(e); - } else SynErr(190); + } else SynErr(189); while (la.kind == 15) { Attribute(ref attrs); } @@ -2486,7 +2491,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 69 || la.kind == 82) { Suffix(ref e); } - } else SynErr(191); + } else SynErr(190); } void Expressions(List/*!*/ args) { @@ -2535,7 +2540,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(17)) { Expression(out ee, true, true); e = ee; - } else SynErr(192); + } else SynErr(191); } void LoopSpec(out List invariants, out List decreases, out List mod, ref Attributes decAttrs, ref Attributes modAttrs) { @@ -2551,7 +2556,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo OldSemi(); invariants.Add(invariant); } else if (la.kind == 56) { - while (!(la.kind == 0 || la.kind == 56)) {SynErr(193); Get();} + while (!(la.kind == 0 || la.kind == 56)) {SynErr(192); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); @@ -2559,7 +2564,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, true); OldSemi(); } else { - while (!(la.kind == 0 || la.kind == 53)) {SynErr(194); Get();} + while (!(la.kind == 0 || la.kind == 53)) {SynErr(193); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -2581,7 +2586,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) { bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; - while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(195); Get();} + while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(194); Get();} if (la.kind == 54) { Get(); isFree = true; @@ -2724,7 +2729,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp; break; } - default: SynErr(196); break; + default: SynErr(195); break; } if (k == null) { op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp); @@ -2761,7 +2766,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 104) { Get(); - } else SynErr(197); + } else SynErr(196); } void ImpliesOp() { @@ -2769,7 +2774,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 106) { Get(); - } else SynErr(198); + } else SynErr(197); } void ExpliesOp() { @@ -2777,7 +2782,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 108) { Get(); - } else SynErr(199); + } else SynErr(198); } void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) { @@ -2962,7 +2967,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 110) { Get(); - } else SynErr(200); + } else SynErr(199); } void OrOp() { @@ -2970,7 +2975,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 112) { Get(); - } else SynErr(201); + } else SynErr(200); } void Term(out Expression e0, bool allowSemi, bool allowLambda) { @@ -3075,7 +3080,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(202); break; + default: SynErr(201); break; } } @@ -3097,7 +3102,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 116) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(203); + } else SynErr(202); } void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3155,7 +3160,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MapComprehensionExpr(x, out e, allowSemi); } else if (StartOf(32)) { SemErr("map must be followed by literal in brackets or comprehension."); - } else SynErr(204); + } else SynErr(203); break; } case 2: case 3: case 4: case 6: case 7: case 9: case 17: case 61: case 62: case 120: case 121: case 122: case 123: case 124: case 125: { @@ -3165,7 +3170,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } break; } - default: SynErr(205); break; + default: SynErr(204); break; } } @@ -3180,7 +3185,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 118) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(206); + } else SynErr(205); } void NegOp() { @@ -3188,7 +3193,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 119) { Get(); - } else SynErr(207); + } else SynErr(206); } void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3235,7 +3240,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda); break; } - default: SynErr(208); break; + default: SynErr(207); break; } } @@ -3377,7 +3382,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(209); + } else SynErr(208); } else if (la.kind == 127) { Get(); anyDots = true; @@ -3385,7 +3390,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true, true); e1 = ee; } - } else SynErr(210); + } else SynErr(209); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -3426,7 +3431,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(83); - } else SynErr(211); + } else SynErr(210); ApplySuffix(ref e); } @@ -3463,7 +3468,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SeqDisplayExpr(x, elements); Expect(83); - } else SynErr(212); + } else SynErr(211); } void MultiSetExpr(out Expression e) { @@ -3489,7 +3494,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); } else if (StartOf(32)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(213); + } else SynErr(212); } void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) { @@ -3617,7 +3622,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda); break; } - default: SynErr(214); break; + default: SynErr(213); break; } } @@ -3646,7 +3651,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero; } - } else SynErr(215); + } else SynErr(214); } void Dec(out Basetypes.BigDec d) { @@ -3756,7 +3761,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 12) { Get(); oneShot = true; - } else SynErr(216); + } else SynErr(215); } void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) { @@ -3789,7 +3794,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 132) { Get(); - } else SynErr(217); + } else SynErr(216); } void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3812,7 +3817,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(16); } else if (StartOf(32)) { if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } - } else SynErr(218); + } else SynErr(217); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -3830,7 +3835,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 129 || la.kind == 130) { Exists(); x = t; - } else SynErr(219); + } else SynErr(218); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi, allowLambda); @@ -3878,7 +3883,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 95) { CalcStmt(out s); - } else SynErr(220); + } else SynErr(219); } void LetExpr(out Expression e, bool allowSemi, bool allowLambda) { @@ -3918,7 +3923,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(221); + } else SynErr(220); Expression(out e, false, true); letRHSs.Add(e); while (la.kind == 38) { @@ -3969,7 +3974,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); pat = new CasePattern(bv.tok, bv); - } else SynErr(222); + } else SynErr(221); if (pat == null) { pat = new CasePattern(t, "_ParseError", new List()); } @@ -4006,7 +4011,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 128) { Get(); - } else SynErr(223); + } else SynErr(222); } void Exists() { @@ -4014,7 +4019,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 130) { Get(); - } else SynErr(224); + } else SynErr(223); } void AttributeBody(ref Attributes attrs) { @@ -4290,48 +4295,47 @@ public class Errors { case 180: s = "invalid IfStmt"; break; case 181: s = "invalid IfStmt"; break; case 182: s = "invalid WhileStmt"; break; - case 183: s = "invalid WhileStmt"; break; - case 184: s = "invalid MatchStmt"; break; + case 183: s = "invalid MatchStmt"; break; + case 184: s = "invalid ForallStmt"; break; case 185: s = "invalid ForallStmt"; break; - case 186: s = "invalid ForallStmt"; break; - case 187: s = "this symbol not expected in ModifyStmt"; break; - case 188: s = "invalid ModifyStmt"; break; - case 189: s = "invalid ReturnStmt"; break; - case 190: s = "invalid Rhs"; break; - case 191: s = "invalid Lhs"; break; - case 192: s = "invalid Guard"; break; + case 186: s = "this symbol not expected in ModifyStmt"; break; + case 187: s = "invalid ModifyStmt"; break; + case 188: s = "invalid ReturnStmt"; break; + case 189: s = "invalid Rhs"; break; + case 190: s = "invalid Lhs"; break; + case 191: s = "invalid Guard"; break; + case 192: s = "this symbol not expected in LoopSpec"; break; case 193: s = "this symbol not expected in LoopSpec"; break; - case 194: s = "this symbol not expected in LoopSpec"; break; - case 195: s = "this symbol not expected in Invariant"; break; - case 196: s = "invalid CalcOp"; break; - case 197: s = "invalid EquivOp"; break; - case 198: s = "invalid ImpliesOp"; break; - case 199: s = "invalid ExpliesOp"; break; - case 200: s = "invalid AndOp"; break; - case 201: s = "invalid OrOp"; break; - case 202: s = "invalid RelOp"; break; - case 203: s = "invalid AddOp"; break; + case 194: s = "this symbol not expected in Invariant"; break; + case 195: s = "invalid CalcOp"; break; + case 196: s = "invalid EquivOp"; break; + case 197: s = "invalid ImpliesOp"; break; + case 198: s = "invalid ExpliesOp"; break; + case 199: s = "invalid AndOp"; break; + case 200: s = "invalid OrOp"; break; + case 201: s = "invalid RelOp"; break; + case 202: s = "invalid AddOp"; break; + case 203: s = "invalid UnaryExpression"; break; case 204: s = "invalid UnaryExpression"; break; - case 205: s = "invalid UnaryExpression"; break; - case 206: s = "invalid MulOp"; break; - case 207: s = "invalid NegOp"; break; - case 208: s = "invalid EndlessExpression"; break; + case 205: s = "invalid MulOp"; break; + case 206: s = "invalid NegOp"; break; + case 207: s = "invalid EndlessExpression"; break; + case 208: s = "invalid Suffix"; break; case 209: s = "invalid Suffix"; break; case 210: s = "invalid Suffix"; break; - case 211: s = "invalid Suffix"; break; - case 212: s = "invalid DisplayExpr"; break; - case 213: s = "invalid MultiSetExpr"; break; - case 214: s = "invalid ConstAtomExpression"; break; - case 215: s = "invalid Nat"; break; - case 216: s = "invalid LambdaArrow"; break; - case 217: s = "invalid QSep"; break; - case 218: s = "invalid MatchExpression"; break; - case 219: s = "invalid QuantifierGuts"; break; - case 220: s = "invalid StmtInExpr"; break; - case 221: s = "invalid LetExpr"; break; - case 222: s = "invalid CasePattern"; break; - case 223: s = "invalid Forall"; break; - case 224: s = "invalid Exists"; break; + case 211: s = "invalid DisplayExpr"; break; + case 212: s = "invalid MultiSetExpr"; break; + case 213: s = "invalid ConstAtomExpression"; break; + case 214: s = "invalid Nat"; break; + case 215: s = "invalid LambdaArrow"; break; + case 216: s = "invalid QSep"; break; + case 217: s = "invalid MatchExpression"; break; + case 218: s = "invalid QuantifierGuts"; break; + case 219: s = "invalid StmtInExpr"; break; + case 220: s = "invalid LetExpr"; break; + case 221: s = "invalid CasePattern"; break; + case 222: s = "invalid Forall"; break; + case 223: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 3b1c018c..9e569ef1 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -595,7 +595,7 @@ namespace Microsoft.Dafny { } } - internal void PrintDecreasesSpec(Specification decs, int indent) { + internal void PrintDecreasesSpec(Specification decs, int indent, bool newLine = true) { Contract.Requires(decs != null); if (printMode == DafnyOptions.PrintModes.NoGhost) { return; } if (decs.Expressions != null && decs.Expressions.Count != 0) { @@ -607,11 +607,15 @@ namespace Microsoft.Dafny { } wr.Write(" "); PrintExpressionList(decs.Expressions, true); - wr.WriteLine(";"); + if (newLine) { + wr.WriteLine(";"); + } else { + wr.Write(";"); + } } } - internal void PrintFrameSpecLine(string kind, List ee, int indent, Attributes attrs) { + internal void PrintFrameSpecLine(string kind, List ee, int indent, Attributes attrs, bool newLine = true) { Contract.Requires(kind != null); Contract.Requires(cce.NonNullElements(ee)); if (ee != null && ee.Count != 0) { @@ -622,7 +626,11 @@ namespace Microsoft.Dafny { } wr.Write(" "); PrintFrameExpressionList(ee); - wr.WriteLine(";"); + if (newLine) { + wr.WriteLine(";"); + } else { + wr.Write(";"); + } } } @@ -1047,15 +1055,15 @@ namespace Microsoft.Dafny { wr.WriteLine(); } - PrintSpec("invariant", s.Invariants, indent + IndentAmount); - PrintDecreasesSpec(s.Decreases, indent + IndentAmount); + PrintSpec("invariant", s.Invariants, indent + IndentAmount, s.Body != null || omitBody || (s.Decreases.Expressions != null && s.Decreases.Expressions.Count != 0) || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0)); + PrintDecreasesSpec(s.Decreases, indent + IndentAmount, s.Body != null || omitBody || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0)); if (s.Mod.Expressions != null) { - PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null); + PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null, s.Body != null || omitBody); } Indent(indent); if (omitBody) { wr.WriteLine("...;"); - } else { + } else if (s.Body != null) { PrintStatement(s.Body, indent); } } @@ -1414,7 +1422,7 @@ namespace Microsoft.Dafny { var e = (ApplyExpr)expr; // determine if parens are needed int opBindingStrength = 0x70; - bool parensNeeded = + bool parensNeeded = opBindingStrength < contextBindingStrength || (fragileContext && opBindingStrength == contextBindingStrength); @@ -1424,7 +1432,7 @@ namespace Microsoft.Dafny { wr.Write("("); PrintExpressionList(e.Args, false); wr.Write(")"); - + if (parensNeeded) { wr.Write(")"); } } else if (expr is FunctionCallExpr) { @@ -1453,7 +1461,7 @@ namespace Microsoft.Dafny { PrintActualArguments(e.Args, e.Name); } if (parensNeeded) { wr.Write(")"); } - + } else if (expr is OldExpr) { wr.Write("old("); PrintExpression(((OldExpr)expr).E, false); @@ -1660,7 +1668,7 @@ namespace Microsoft.Dafny { bool parensNeeded = !isRightmost; if (parensNeeded) { wr.Write("("); } wr.Write(e is ForallExpr ? "forall" : "exists"); - PrintTypeParams(e.TypeArgs); // new! + PrintTypeParams(e.TypeArgs); // new! wr.Write(" "); PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range); wr.Write(" :: "); @@ -1716,7 +1724,7 @@ namespace Microsoft.Dafny { wr.Write(" :: "); PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon); if (parensNeeded) { wr.Write(")"); } - + } else if (expr is LambdaExpr) { var e = (LambdaExpr)expr; wr.Write("("); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 818bdcc4..757995f2 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -151,7 +151,7 @@ namespace Microsoft.Dafny readonly Graph dependencies = new Graph(); private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; - private RefinementTransformer refinementTransformer = null; + private RefinementTransformer refinementTransformer = null; public Resolver(Program prog) { Contract.Requires(prog != null); @@ -502,17 +502,17 @@ namespace Microsoft.Dafny var obj = new IdentifierExpr(e.tok, oVar.Name) { Type = oVar.Type, Var = oVar }; bvars.Add(oVar); - return + return new SetComprehension(e.tok, bvars, new BinaryExpr(e.tok, BinaryExpr.Opcode.In, obj, - new ApplyExpr(e.tok, e.tok, e, bexprs) + new ApplyExpr(e.tok, e.tok, e, bexprs) { Type = new SetType(new ObjectType()) - }) + }) { ResolvedOp = BinaryExpr.ResolvedOpcode.InSet, Type = Type.Bool - }, obj) + }, obj) { Type = new SetType(new ObjectType()) }; @@ -1212,7 +1212,7 @@ namespace Microsoft.Dafny int prevErrorCount = ErrorCount; // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations - // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields. This is needed for the + // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields. This is needed for the // resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field // of any newtypes involved. DiscoverBounds is called on quantifiers (but only in non-ghost contexts) and set comprehensions (in all // contexts). The constraints of newtypes are ghost, so DiscoverBounds is not going to be called on any quantifiers they may contain. @@ -1497,7 +1497,7 @@ namespace Microsoft.Dafny if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; done = true; - break; + break; } } foreach (var p in m.Outs) { @@ -2027,7 +2027,10 @@ namespace Microsoft.Dafny return status; } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; - var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); + var status = TailRecursionStatus.NotTailRecursive; + if (s.Body != null) { + status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); + } if (status != TailRecursionStatus.CanBeFollowedByAnything) { if (status == TailRecursionStatus.NotTailRecursive) { // an error has already been reported @@ -2295,7 +2298,10 @@ namespace Microsoft.Dafny if (s.Guard != null) { Visit(s.Guard, st); } - Visit(s.Body, st); + // don't recurse on the body, if it's a dirty loop + if (s.Body != null) { + Visit(s.Body, st); + } return false; } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; @@ -2364,7 +2370,7 @@ namespace Microsoft.Dafny Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0)); } else if (!t1.SupportsEquality) { Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1)); - } + } break; default: switch (e.ResolvedOp) { @@ -3888,7 +3894,7 @@ namespace Microsoft.Dafny // detect self-loops here, since they don't show up in the graph's SSC methods Error(dd.tok, "recursive dependency involving a newtype: {0} -> {0}", dd.Name); } - } + } what = "newtype"; t.ResolvedClass = dd; } else { @@ -4750,13 +4756,15 @@ namespace Microsoft.Dafny } } s.IsGhost = bodyMustBeSpecOnly; - loopStack.Add(s); // push - if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map - inSpecOnlyContext.Add(s, specContextOnly); - } + if (s.Body != null) { + loopStack.Add(s); // push + if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map + inSpecOnlyContext.Add(s, specContextOnly); + } - ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext); - loopStack.RemoveAt(loopStack.Count - 1); // pop + ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext); + loopStack.RemoveAt(loopStack.Count - 1); // pop + } } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; @@ -5111,7 +5119,6 @@ namespace Microsoft.Dafny var update = s as UpdateStmt; var lhsNameSet = new HashSet(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification) - var i = 0; foreach (var lhs in s.Lhss) { var ec = ErrorCount; ResolveExpression(lhs, new ResolveOpts(codeContext, true)); @@ -5627,7 +5634,9 @@ namespace Microsoft.Dafny } else if (stmt is WhileStmt) { WhileStmt s = (WhileStmt)stmt; - CheckForallStatementBodyRestrictions(s.Body, kind); + if (s.Body != null) { + CheckForallStatementBodyRestrictions(s.Body, kind); + } } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; @@ -5746,7 +5755,9 @@ namespace Microsoft.Dafny if (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { Error(s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause"); } - CheckHintRestrictions(s.Body); + if (s.Body != null) { + CheckHintRestrictions(s.Body); + } } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; @@ -5910,7 +5921,7 @@ namespace Microsoft.Dafny Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count); // follows from the fact that ctype was resolved #if TWO_SEARCHES MemberDecl member = cd.Members.Find(md => md.Name == memberName); - if (member == null && + if (member == null && (!classMembers.ContainsKey(cd) || !classMembers[cd].TryGetValue(memberName, out member))) { #else MemberDecl member; @@ -6317,7 +6328,7 @@ namespace Microsoft.Dafny if (resolved == null) { // error has already been reported by ResolvePredicateOrField } else { - // the following will cause e.Obj to be resolved again, but that's still correct + // the following will cause e.Obj to be resolved again, but that's still correct e.ResolvedExpression = resolved; ResolveExpression(e.ResolvedExpression, opts); e.Type = e.ResolvedExpression.Type; @@ -6347,7 +6358,7 @@ namespace Microsoft.Dafny } foreach (var tp in fn.TypeArgs) { Type prox = new InferredTypeProxy(); - subst[tp] = prox; + subst[tp] = prox; e.TypeApplication.Add(prox); } e.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule); @@ -6479,7 +6490,7 @@ namespace Microsoft.Dafny foreach (Formal d in ctor.Formals) { if (d == destructor.CorrespondingFormal) { ctor_args.Add(e.Value); - } else { + } else { ctor_args.Add(new ExprDotName(expr.tok, tmpVarIdExpr, d.Name)); } } @@ -7449,7 +7460,7 @@ namespace Microsoft.Dafny if (field != null) { if (field.Type.IsArrowType || field.Type.IsTypeParameter) { return new ApplyExpr(tok, openParen, new ExprDotName(tok, receiver, fn), args); - } + } } return new FunctionCallExpr(tok, fn, receiver, openParen, args); } @@ -7875,12 +7886,12 @@ namespace Microsoft.Dafny ResolveExpression(arg, opts); } } - } + } return r; } /// - /// Resolves "obj . suffixName" to a member select expression, + /// Resolves "obj . suffixName" to a member select expression, /// Expects "obj" already to have been resolved. /// On success, returns the result of the resolution--as an un-resolved expression. /// On failure, returns null (in which case an error has been reported to the user). @@ -8380,7 +8391,7 @@ namespace Microsoft.Dafny s.UnionWith(t); } return s; - + } else if (expr is LambdaExpr) { var e = (LambdaExpr)expr; var s = FreeVariables(e.Term); @@ -8753,7 +8764,7 @@ namespace Microsoft.Dafny Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } - + /// /// This method adds to "coConclusions" all copredicate calls and codatatype equalities that occur diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index ca72e221..06493434 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -299,7 +299,7 @@ public class Scanner { } // [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() { Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -308,7 +308,7 @@ public class Scanner { try { Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); - Filename = fileName; + Filename = useBaseName? GetBaseName(fileName): fileName; Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); @@ -316,7 +316,7 @@ public class Scanner { } // [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() { Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -324,10 +324,14 @@ public class Scanner { t = new Token(); // dummy because t is a non-null field buffer = new Buffer(s, true); this.errorHandler = errorHandler; - this.Filename = fileName; + this.Filename = useBaseName? GetBaseName(fileName) : fileName; Init(); } + string GetBaseName(string fileName) { + return System.IO.Path.GetFileName(fileName); // Return basename + } + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 0a83499c..ecc2ff56 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -276,7 +276,7 @@ namespace Microsoft.Dafny { Bpl.Constant c = (Bpl.Constant)d; if (c.Name == "alloc") { allocField = c; - } + } } else if (d is Bpl.GlobalVariable) { Bpl.GlobalVariable v = (Bpl.GlobalVariable)d; if (v.Name == "$Heap") { @@ -373,7 +373,7 @@ namespace Microsoft.Dafny { public Bpl.Program Translate(Program p) { Contract.Requires(p != null); Contract.Ensures(Contract.Result() != null); - + program = p; if (sink == null || predef == null) { @@ -473,7 +473,7 @@ namespace Microsoft.Dafny { } //adding TraitParent function and axioms - //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink: + //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink: // const unique NoTraitAtAll: ClassName; // function TraitParent(ClassName): ClassName; // axiom TraitParent(class.A) == class.J; @@ -618,7 +618,7 @@ namespace Microsoft.Dafny { int i; // Add: function #dt.ctor(tyVars, paramTypes) returns (DatatypeType); - + List argTypes = new List(); foreach (Formal arg in ctor.Formals) { Bpl.Variable a = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), true); @@ -642,7 +642,7 @@ namespace Microsoft.Dafny { sink.AddTopLevelDeclaration(cid); { - // Add: axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor); + // Add: axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor); CreateBoundVariables(ctor.Formals, out bvs, out args); Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs); @@ -668,8 +668,8 @@ namespace Microsoft.Dafny { } } - - + + { // Add: axiom (forall d: DatatypeType :: dt.ctor?(d) ==> (exists params :: d == #dt.ctor(params)); CreateBoundVariables(ctor.Formals, out bvs, out args); @@ -688,11 +688,11 @@ namespace Microsoft.Dafny { /* (forall x0 : C0, ..., xn : Cn, G : Ty • { $Is(C(x0,...,xn), T(G)) } - $Is(C(x0,...,xn), T(G)) <==> + $Is(C(x0,...,xn), T(G)) <==> $Is[Box](x0, C0(G)) && ... && $Is[Box](xn, Cn(G))); (forall x0 : C0, ..., xn : Cn, G : Ty • { $IsAlloc(C(G, x0,...,xn), T(G)) } - $IsAlloc(C(G, x0,...,xn), T(G)) ==> + $IsAlloc(C(G, x0,...,xn), T(G)) ==> $IsAlloc[Box](x0, C0(G)) && ... && $IsAlloc[Box](xn, Cn(G))); */ List tyexprs; @@ -737,14 +737,14 @@ namespace Microsoft.Dafny { foreach (Bpl.Expr arg in args) { litargs.Add(Lit(arg)); } - Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs); + Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs); Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args), predef.DatatypeType); Bpl.Expr q = BplForall(bvs, BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs)); sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Constructor literal")); - } + } // Injectivity axioms for normal arguments - i = 0; + i = 0; foreach (Formal arg in ctor.Formals) { // function ##dt.ctor#i(DatatypeType) returns (Ti); var sf = ctor.Destructors[i]; @@ -752,7 +752,7 @@ namespace Microsoft.Dafny { fn = GetReadonlyField(sf); sink.AddTopLevelDeclaration(fn); // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i); - CreateBoundVariables(ctor.Formals, out bvs, out args); + CreateBoundVariables(ctor.Formals, out bvs, out args); var inner = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); var outer = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), inner); var q = BplForall(bvs, BplTrigger(inner), Bpl.Expr.Eq(outer, args[i])); @@ -792,7 +792,7 @@ namespace Microsoft.Dafny { q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs))); sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q)); // axiom (forall params, SeqRank(arg) < DtRank(#dt.ctor(params))); - CreateBoundVariables(ctor.Formals, out bvs, out args); + CreateBoundVariables(ctor.Formals, out bvs, out args); lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]); rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs); @@ -829,7 +829,7 @@ namespace Microsoft.Dafny { } } - i++; + i++; } } @@ -905,8 +905,8 @@ namespace Microsoft.Dafny { }; Action, List>, List, List, List, Bpl.Variable, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr>> CoAxHelper = (add_k, K) => { - Func> renew = s => - Map(codecl.TypeArgs, tp => + Func> renew = s => + Map(codecl.TypeArgs, tp => new TypeParameter(tp.tok, tp.Name + "#" + s, tp.PositionalIndex, tp.Parent)); List typaramsL = renew("l"), typaramsR = renew("r"); List lexprs; var lvars = MkTyParamBinders(typaramsL, out lexprs); @@ -924,9 +924,9 @@ namespace Microsoft.Dafny { } else { kVar = null; k = null; kGtZero = Bpl.Expr.True; } - var ly = BplBoundVar("ly", predef.LayerType, vars); + var ly = BplBoundVar("ly", predef.LayerType, vars); var d0 = BplBoundVar("d0", predef.DatatypeType, vars); - var d1 = BplBoundVar("d1", predef.DatatypeType, vars); + var d1 = BplBoundVar("d1", predef.DatatypeType, vars); K(tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1); }; @@ -950,8 +950,8 @@ namespace Microsoft.Dafny { sink.AddTopLevelDeclaration(fn); } - // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType :: - // { Eq(G0, .., Gn, S(ly), k, d0, d1) } + // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType :: + // { Eq(G0, .., Gn, S(ly), k, d0, d1) } // Is(d0, T(G0, .., Gn)) && Is(d1, T(G0, ... Gn)) ==> // (Eq(G0, .., Gn, S(ly), k, d0, d1) // <==> @@ -969,8 +969,8 @@ namespace Microsoft.Dafny { sink.AddTopLevelDeclaration(new Bpl.Axiom(dt.tok, ax, "Layered co-equality axiom")); }); - // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType :: - // { Eq(G0, .., Gn, S(ly), k, d0, d1) } + // axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType :: + // { Eq(G0, .., Gn, S(ly), k, d0, d1) } // 0 < k ==> // (Eq(G0, .., Gn, S(ly), k, d0, d1) <==> // Eq(G0, .., Gn, ly, k, d0, d)) @@ -1059,7 +1059,7 @@ namespace Microsoft.Dafny { // produce with conjucts=false (default): // (A.Nil? && B.Nil?) || // (A.Cons? && B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail)) - // + // // with conjuncts=true: // (A.Nil? ==> B.Nil?) && // (A.Cons? ==> (B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail))) @@ -1081,7 +1081,7 @@ namespace Microsoft.Dafny { var lexprs = Map(ty.TypeArgs, tt => Resolver.SubstType(tt, lsu)); var rexprs = Map(ty.TypeArgs, tt => Resolver.SubstType(tt, rsu)); q = CoEqualCall(codecl, lexprs, rexprs, k, l, a, b); - } else { + } else { // ordinary equality; let the usual translation machinery figure out the translation var equal = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new BoogieWrapper(a, ty), new BoogieWrapper(b, ty)); equal.ResolvedOp = Resolver.ResolveOp(equal.Op, ty); // resolve here @@ -1093,7 +1093,7 @@ namespace Microsoft.Dafny { if (conjuncts) { yield return Bpl.Expr.Binary(new NestedToken(tok, ctor.tok), BinaryOperator.Opcode.Imp, aq, BplAnd(bq, chunk)); } else { - yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk)); + yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk)); } } } @@ -1121,7 +1121,7 @@ namespace Microsoft.Dafny { tok = A.tok; } List args = Concat(largs, rargs); - if (k != null) { + if (k != null) { args.Add(k); } args.AddRange(new List { l, A, B }); @@ -1296,7 +1296,7 @@ namespace Microsoft.Dafny { var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List { arg_ref }, res); sink.AddTopLevelDeclaration(implement_intr); } - //this adds: axiom implements$J(class.C); + //this adds: axiom implements$J(class.C); else if (c is ClassDecl) { if (c.Trait != null) @@ -1312,7 +1312,7 @@ namespace Microsoft.Dafny { sink.AddTopLevelDeclaration(implements_axiom); } } - + foreach (MemberDecl member in c.Members) { currentDeclaration = member; if (member is Field) { @@ -1405,7 +1405,7 @@ namespace Microsoft.Dafny { if (f.Body != null && !IsOpaqueFunction(f)) { AddFunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, f.Body.Resolved); AddFunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, f.Body.Resolved); - } + } // for body-less functions, at least generate its #requires function if (f.Body == null) { var b = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, null, null); @@ -1562,7 +1562,7 @@ namespace Microsoft.Dafny { validCall.Function = iter.Member_Valid; // resolve here validCall.Type = Type.Bool; // resolve here - validCall.TypeArgumentSubstitutions = new Dictionary(); + validCall.TypeArgumentSubstitutions = new Dictionary(); foreach (var p in iter.TypeArgs) { validCall.TypeArgumentSubstitutions[p] = new UserDefinedType(p); } // resolved here. @@ -1871,8 +1871,8 @@ namespace Microsoft.Dafny { // the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny // allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is // sound after that, then it would also have been sound just before the allocation. - // - List tyargs; + // + List tyargs; var formals = MkTyParamBinders(GetTypeParams(f), out tyargs); var args = new List(); Bpl.BoundVariable layer; @@ -1921,7 +1921,7 @@ namespace Microsoft.Dafny { var ly = new Bpl.IdentifierExpr(f.tok, layer); funcArgs.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, ly)); } - funcArgs.AddRange(args); + funcArgs.AddRange(args); funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), funcArgs); } @@ -2016,7 +2016,7 @@ namespace Microsoft.Dafny { // where GOOD_PARAMETERS means: // $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types && // Pre($Heap,formals) - // + // // NOTE: this is lifted out to a #requires function for intra module calls, // and used in the function pseudo-handles for top level functions. // For body-less functions, this is emitted when body is null. @@ -2041,8 +2041,8 @@ namespace Microsoft.Dafny { // quantify over the type arguments, and add them first to the arguments List args = new List(); - List tyargs; - var formals = MkTyParamBinders(GetTypeParams(f), out tyargs); + List tyargs; + var formals = MkTyParamBinders(GetTypeParams(f), out tyargs); Bpl.BoundVariable layer; if (f.IsRecursive) { @@ -2105,16 +2105,16 @@ namespace Microsoft.Dafny { // Add the precondition function and its axiom (which is equivalent to the ante) if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) { - var precondF = new Bpl.Function(f.tok, - RequiresName(f), new List(), - formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)), + var precondF = new Bpl.Function(f.tok, + RequiresName(f), new List(), + formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)), BplFormalVar(null, Bpl.Type.Bool, false)); sink.AddTopLevelDeclaration(precondF); - var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, + var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x)))); sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante)))); // you could use it to check that it always works, but it makes VSI-Benchmarks/b3.dfy time out: - // ante = appl; + // ante = appl; if (body == null) { return null; } @@ -2195,8 +2195,8 @@ namespace Microsoft.Dafny { Expression PrefixSubstitution(PrefixPredicate pp, Expression body) { Contract.Requires(pp != null); - var typeMap = Util.Dict(pp.Co.TypeArgs, Map(pp.TypeArgs, x => new UserDefinedType(x))); - + var typeMap = Util.Dict(pp.Co.TypeArgs, Map(pp.TypeArgs, x => new UserDefinedType(x))); + var paramMap = new Dictionary(); for (int i = 0; i < pp.Co.Formals.Count; i++) { var replacement = pp.Formals[i + 1]; // the +1 is to skip pp's _k parameter @@ -2294,7 +2294,7 @@ namespace Microsoft.Dafny { var tok = pp.tok; var etran = new ExpressionTranslator(this, predef, tok); - List tyexprs; + List tyexprs; var tyvars = MkTyParamBinders(pp.TypeArgs, out tyexprs); var bvs = new List(tyvars); @@ -2356,9 +2356,9 @@ namespace Microsoft.Dafny { kWhere = wh; } else { bvs.Add(bv); - if (wh != null) { + if (wh != null) { // add well-typedness conjunct to antecedent - ante = Bpl.Expr.And(ante, wh); + ante = Bpl.Expr.And(ante, wh); } } } @@ -2375,7 +2375,7 @@ namespace Microsoft.Dafny { var allK = new Bpl.ForallExpr(tok, new List { k }, tr, BplImp(kWhere, prefixAppl)); tr = new Bpl.Trigger(tok, true, new List { coAppl }); var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), allK)); - sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, allS), + sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, allS), "1st prefix predicate axiom for " + pp.FullSanitizedName)); // forall args :: { P(args) } args-have-appropriate-values && (forall k :: 0 ATMOST k ==> P#[k](args)) ==> P(args) @@ -2406,7 +2406,7 @@ namespace Microsoft.Dafny { /// ==> $IsAlloc(h[o, f], TT(PP), h)) /// && $Is(h[o, f], TT(PP), h); /// - /// This can be optimised later to: + /// This can be optimised later to: /// axiom (forall o: ref, h: Heap :: /// { h[o, f] } /// $IsHeap(h) && o != null && Tag(dtype(o)) = TagClass @@ -2446,7 +2446,7 @@ namespace Microsoft.Dafny { List tyexprs; var tyvars = MkTyParamBinders(GetTypeParams(c), out tyexprs); - Bpl.Expr o_ty = ClassTyCon(c, tyexprs); + Bpl.Expr o_ty = ClassTyCon(c, tyexprs); // Bpl.Expr is_o = MkIs(o, o_ty); // $Is(o, ..) // Changed to use dtype(o) == o_ty instead: @@ -2458,7 +2458,7 @@ namespace Microsoft.Dafny { Bpl.Expr is_hf, isalloc_hf; if (is_array) { - is_hf = MkIs(oDotF, tyexprs[0], true); + is_hf = MkIs(oDotF, tyexprs[0], true); isalloc_hf = MkIsAlloc(oDotF, tyexprs[0], h, true); } else { is_hf = MkIs(oDotF, f.Type); // $Is(h[o, f], ..) @@ -2497,7 +2497,7 @@ namespace Microsoft.Dafny { tr = new Bpl.Trigger(c.tok, true, t_es); } Bpl.Expr ax = BplForall(Concat(Concat(tyvars, ixvars), new List { hVar, oVar }), tr, body); - sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, ax, + sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, ax, c + "." + f + ": Allocation axiom")); } @@ -2593,7 +2593,7 @@ namespace Microsoft.Dafny { return expr; } } - + void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc) { Contract.Requires(m != null); @@ -2616,7 +2616,7 @@ namespace Microsoft.Dafny { List localVariables = new List(); GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables); - Bpl.StmtList stmts; + Bpl.StmtList stmts; if (!wellformednessProc) { if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoLemma)) { var posts = new List(); @@ -2661,8 +2661,8 @@ namespace Microsoft.Dafny { } else { substMap.Add(iv, ie); } - } - + } + // Generate a CallStmt for the recursive call Expression recursiveCallReceiver; @@ -3551,7 +3551,7 @@ namespace Microsoft.Dafny { ExpressionTranslator /*!*/ etran, Bpl.StmtListBuilder /*!*/ builder, string errorMessage, - Bpl.QKeyValue kv) + Bpl.QKeyValue kv) { CheckFrameSubset(tok, calleeFrame, receiverReplacement, substMap, etran, (t, e, s, q) => builder.Add(Assert(t, e, s, q)), errorMessage, kv); @@ -3559,7 +3559,7 @@ namespace Microsoft.Dafny { void CheckFrameSubset(IToken tok, List calleeFrame, Expression receiverReplacement, Dictionary substMap, - ExpressionTranslator/*!*/ etran, + ExpressionTranslator/*!*/ etran, Action MakeAssert, string errorMessage, Bpl.QKeyValue kv) @@ -3692,10 +3692,10 @@ namespace Microsoft.Dafny { sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax)); } else { #else - // This is the general case + // This is the general case Bpl.Expr h0; var h0Var = BplBoundVar("$h0", predef.HeapType, out h0); - Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1); - + Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1); + var etran0 = new ExpressionTranslator(this, predef, h0); var etran1 = new ExpressionTranslator(this, predef, h1); @@ -3705,7 +3705,7 @@ namespace Microsoft.Dafny { Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha"); Bpl.Expr o; var oVar = BplBoundVar("$o", predef.RefType, out o); - Bpl.Expr field; var fieldVar = BplBoundVar("$f", predef.FieldName(f.tok, alpha), out field); + Bpl.Expr field; var fieldVar = BplBoundVar("$f", predef.FieldName(f.tok, alpha), out field); Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null); Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o))); Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field), ReadHeap(f.tok, h1, o, field)); @@ -3722,7 +3722,7 @@ namespace Microsoft.Dafny { var f0argsCanCall = new List(tyexprs); var f1argsCanCall = new List(tyexprs); if (f.IsRecursive) { - Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s); + Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s); bvars.Add(sV); f0args.Add(s); f1args.Add(s); // but don't add to f0argsCanCall or f1argsCanCall } @@ -3755,14 +3755,14 @@ namespace Microsoft.Dafny { } var canCall = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool)); wellFormed = Bpl.Expr.And(wellFormed, Bpl.Expr.And( - Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f0argsCanCall), fwf0), + Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f0argsCanCall), fwf0), Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f1argsCanCall), fwf1))); - + /* DR: I conjecture that this should be enough, as the requires is preserved when the frame is: - wellFormed = Bpl.Expr.And(wellFormed, + wellFormed = Bpl.Expr.And(wellFormed, Bpl.Expr.Or(new Bpl.NAryExpr(f.tok, canCall, f0argsCanCall), fwf0)); */ @@ -3987,8 +3987,8 @@ namespace Microsoft.Dafny { Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args); DefineFrame(f.tok, f.Reads, bodyCheckBuilder - , new List() /* dummy local variable list, since frame axiom variable (and its definition) - * is already added. The only reason why we add the frame axiom definition + , new List() /* dummy local variable list, since frame axiom variable (and its definition) + * is already added. The only reason why we add the frame axiom definition * again is to make boogie gives the same trace as before the change that * makes reads clauses also guard the requires */ , null); @@ -4000,11 +4000,11 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); // var b$reads_guards_requires#0 : bool - locals.AddRange(wfo.Locals); + locals.AddRange(wfo.Locals); // This ugly way seems to be the way to add things at the start of a builder: StmtList sl = builder.Collect(f.tok); // b$reads_guards_requires#0 := true ... - sl.BigBlocks[0].simpleCmds.InsertRange(0, wfo.AssignLocals); + sl.BigBlocks[0].simpleCmds.InsertRange(0, wfo.AssignLocals); Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name, typeParams, Concat(typeInParams, implInParams), new List(), @@ -4205,7 +4205,7 @@ namespace Microsoft.Dafny { } else if (expr is ApplyExpr) { ApplyExpr e = (ApplyExpr)expr; return BplAnd( - Cons(CanCallAssumption(e.Function, etran), + Cons(CanCallAssumption(e.Function, etran), e.Args.ConvertAll(ee => CanCallAssumption(ee, etran)))); } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; @@ -4701,8 +4701,8 @@ namespace Microsoft.Dafny { var args = Concat( Map(tt.TypeArgs, TypeToTy), - Cons(etran.TrExpr(e.Function), - Cons(etran.HeapExpr, + Cons(etran.TrExpr(e.Function), + Cons(etran.HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))); // check precond @@ -4715,7 +4715,7 @@ namespace Microsoft.Dafny { FunctionCall(e.tok, Reads(arity), TrType(objset), args), objset); var reads = new FrameExpression(e.tok, wrap, null); - CheckFrameSubset(expr.tok, new List{ reads }, null, null, + CheckFrameSubset(expr.tok, new List{ reads }, null, null, etran, options.AssertSink(this, builder), "insufficient reads clause to invoke function", options.AssertKv); } @@ -4863,7 +4863,7 @@ namespace Microsoft.Dafny { // Cannot use the datatype's formals, so we substitute the inferred type args: var su = new Dictionary(); foreach (var p in dtv.Ctor.EnclosingDatatype.TypeArgs.Zip(dtv.InferredTypeArgs)) { - su[p.Item1] = p.Item2; + su[p.Item1] = p.Item2; } Type ty = Resolver.SubstType(formal.Type, su); CheckSubrange(arg.tok, etran.TrExpr(arg), ty, builder); @@ -5049,7 +5049,7 @@ namespace Microsoft.Dafny { // new options now contains the delayed reads checks locals.AddRange(newOptions.Locals); - // assign locals to true, but at a scope above + // assign locals to true, but at a scope above Contract.Assert(newBuilder != builder); foreach (var a in newOptions.AssignLocals) { builder.Add(a); @@ -5306,7 +5306,7 @@ namespace Microsoft.Dafny { var args = new List(); var vars = MkTyParamBinders(GetTypeParams(f), out args); var formals = MkTyParamFormals(GetTypeParams(f), false); - var tyargs = new List(); + var tyargs = new List(); foreach (var fm in f.Formals) { tyargs.Add(TypeToTy(fm.Type)); } @@ -5356,7 +5356,7 @@ namespace Microsoft.Dafny { int arity = f.Formals.Count; { - // Apply(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) + // Apply(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) // = [Box] F(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN) var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(args)); @@ -5369,7 +5369,7 @@ namespace Microsoft.Dafny { } { - // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) + // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) // = F#Requires(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN) // || Scramble(...) @@ -5389,7 +5389,7 @@ namespace Microsoft.Dafny { } { - // Reads(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)[Box(o)] + // Reads(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)[Box(o)] // = $Frame_F(args...)[o] // // && Scramble(...) @@ -5439,7 +5439,7 @@ namespace Microsoft.Dafny { // function HandleN([Heap, Box, ..., Box] Box, [Heap, Box, ..., Box] Bool) : HandleType var res = BplFormalVar(null, predef.HandleType, true); var arg = new List { - BplFormalVar(null, apply_ty, true), + BplFormalVar(null, apply_ty, true), BplFormalVar(null, requires_ty, true), BplFormalVar(null, reads_ty, true) }; @@ -5463,11 +5463,11 @@ namespace Microsoft.Dafny { SelectorFunction(Reads(arity), objset_ty); { - // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box + // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box // :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN] // // no precondition for these, but: - // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN] + // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN] // for reads, we could: ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't Action SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => { Contract.Assert((precond == null) == (precondTy == null)); @@ -5511,11 +5511,11 @@ namespace Microsoft.Dafny { SelectorSemantics(Requires(arity), Bpl.Type.Bool, "r", requires_ty, null, null); SelectorSemantics(Reads(arity), objset_ty, "rd", reads_ty, null, null); - // function {:inline true} - // FuncN._requires(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool + // function {:inline true} + // FuncN._requires(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool // { RequiresN(f, H, x...x) } - // function {:inline true} - // FuncN._requires#canCall(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool + // function {:inline true} + // FuncN._requires#canCall(G...G G: Ty, H:Heap, f:Handle, x ... x :Box): bool // { true } // + similar for Reads Action UserSelectorFunction = (fname, f) => { @@ -5552,15 +5552,15 @@ namespace Microsoft.Dafny { HeapSucc(h0, h1) && GoodHeap(h0) && GoodHeap(h1) && Is&IsAllocBox(bxI, tI, h0) // in h0, not hN && Is&IsAlloc(f, Func(t1,..,tN, tN+1), h0) // in h0, not hN - && + && (forall o : ref:: - o != null && h0[o, alloc] && h1[o, alloc] && + o != null && h0[o, alloc] && h1[o, alloc] && Reads(h,hN,bxs)[Box(o)] // for hN in h0 and h1 ==> h0[o,field] == h1[o,field]) - ==> Reads(..h0..) == Reads(..h1..) + ==> Reads(..h0..) == Reads(..h1..) AND Requires(f,h0,bxs) == Requires(f,h1,bxs) // which is needed for the next AND Apply(f,h0,bxs) == Apply(f,h0,bxs) - + */ { var bvars = new List(); @@ -5579,9 +5579,9 @@ namespace Microsoft.Dafny { var isness = BplAnd( Snoc(Map(Enumerable.Range(0, arity), i => - BplAnd(MkIs(boxes[i], types[i], true), + BplAnd(MkIs(boxes[i], types[i], true), MkIsAlloc(boxes[i], types[i], h0, true))), - BplAnd(MkIs(f, ClassTyCon(ad, types)), + BplAnd(MkIs(f, ClassTyCon(ad, types)), MkIsAlloc(f, ClassTyCon(ad, types), h0)))); Action AddFrameForFunction = (hN, fname) => { @@ -5614,7 +5614,7 @@ namespace Microsoft.Dafny { Bpl.Expr.Eq(fn(h0), fn(h1)))))); }; - AddFrameForFunction(h0, Reads(ad.Arity)); + AddFrameForFunction(h0, Reads(ad.Arity)); AddFrameForFunction(h1, Reads(ad.Arity)); AddFrameForFunction(h0, Requires(ad.Arity)); AddFrameForFunction(h1, Requires(ad.Arity)); @@ -5627,10 +5627,10 @@ namespace Microsoft.Dafny { forall t0..tN+1 : Ty, h : Heap, f : Handle, bx1 .. bxN : Box, GoodHeap(h) - && Is&IsAllocBox(bxI, tI, h) - && Is&IsAlloc(f, Func(t1,..,tN, tN+1), h) + && Is&IsAllocBox(bxI, tI, h) + && Is&IsAlloc(f, Func(t1,..,tN, tN+1), h) ==> Is&IsAllocBox(Apply(f,h0,bxs))) - + */ { var bvars = new List(); @@ -5645,9 +5645,9 @@ namespace Microsoft.Dafny { var isness = BplAnd( Snoc(Map(Enumerable.Range(0, arity), i => - BplAnd(MkIs(boxes[i], types[i], true), + BplAnd(MkIs(boxes[i], types[i], true), MkIsAlloc(boxes[i], types[i], h, true))), - BplAnd(MkIs(f, ClassTyCon(ad, types)), + BplAnd(MkIs(f, ClassTyCon(ad, types)), MkIsAlloc(f, ClassTyCon(ad, types), h)))); var applied = FunctionCall(tok, Apply(ad.Arity), predef.BoxType, Concat(types, Cons(f, Cons(h, boxes)))); @@ -5690,7 +5690,7 @@ namespace Microsoft.Dafny { }; // Create the Tag and calling Tag on this type constructor - /* + /* const unique TagList: TyTag; axiom (forall t0: Ty :: { List(t0) } Tag(List(t0)) == TagList); */ @@ -5705,7 +5705,7 @@ namespace Microsoft.Dafny { }); // Create the injectivity axiom and its function - /* + /* function List_0(Ty) : Ty; axiom (forall t0: Ty :: { List(t0) } List_0(List(t0)) == t0); */ @@ -5724,8 +5724,8 @@ namespace Microsoft.Dafny { // Boxing axiom (important for the properties of unbox) /* - axiom (forall T: Ty, bx: Box :: - { $IsBox(bx, List(T)) } + axiom (forall T: Ty, bx: Box :: + { $IsBox(bx, List(T)) } $IsBox(bx, List(T)) ==> $Box($Unbox(bx): DatatypeType) == bx && $Is($Unbox(bx): DatatypeType, List(T))); @@ -5745,7 +5745,7 @@ namespace Microsoft.Dafny { }); return name; - } + } Bpl.Constant GetClass(TopLevelDecl cl) { @@ -5806,17 +5806,17 @@ namespace Microsoft.Dafny { return fc; } - + Bpl.Function GetReadonlyField(Field f) { Contract.Requires(f != null && !f.IsMutable); Contract.Requires(sink != null && predef != null); Contract.Ensures(Contract.Result() != null); - + Bpl.Function ff; - if (fieldFunctions.TryGetValue(f, out ff)) { + if (fieldFunctions.TryGetValue(f, out ff)) { Contract.Assert(ff != null); - } else { + } else { if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { // link directly to the function in the prelude. fieldFunctions.Add(f, predef.ArrayLength); return predef.ArrayLength; @@ -5945,7 +5945,7 @@ namespace Microsoft.Dafny { /// /// This method is expected to be called at most once for each parameter combination, and in particular /// at most once for each value of "kind". - /// + /// Bpl.Procedure AddMethod(Method m, MethodTranslationKind kind) { Contract.Requires(m != null); @@ -5963,7 +5963,7 @@ namespace Microsoft.Dafny { List inParams, outParams; GenerateMethodParameters(m.tok, m, kind, etran, out inParams, out outParams); - var req = new List(); + var req = new List(); var mod = new List(); var ens = new List(); // FREE PRECONDITIONS @@ -6348,7 +6348,7 @@ namespace Microsoft.Dafny { private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, MethodTranslationKind kind, bool includeReceiver, bool includeInParams, bool includeOutParams, ExpressionTranslator etran, out List inParams, out List outParams) { inParams = new List(); - outParams = new List(); + outParams = new List(); // Add type parameters first, always! inParams.AddRange(MkTyParamFormals(GetTypeParams(m))); if (includeReceiver) { @@ -6358,8 +6358,8 @@ namespace Microsoft.Dafny { etran.GoodRef(tok, new Bpl.IdentifierExpr(tok, "this", predef.RefType), receiverType)); Bpl.Formal thVar = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", predef.RefType, wh), true); inParams.Add(thVar); - } - if (includeInParams) { + } + if (includeInParams) { foreach (Formal p in m.Ins) { Bpl.Type varType = TrType(p.Type); Bpl.Expr wh = GetExtendedWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(currentDeclaration), varType), p.Type, etran); @@ -7023,9 +7023,11 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) { AddComment(builder, stmt, "while statement"); var s = (WhileStmt)stmt; - TrLoop(s, s.Guard, - delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrStmt(s.Body, bld, locals, e); }, - builder, locals, etran); + BodyTranslator bodyTr = null; + if (s.Body != null) { + bodyTr = delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrStmt(s.Body, bld, locals, e); }; + } + TrLoop(s, s.Guard, bodyTr, builder, locals, etran); } else if (stmt is AlternativeLoopStmt) { AddComment(builder, stmt, "alternative loop statement"); @@ -8138,7 +8140,6 @@ namespace Microsoft.Dafny { void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr, Bpl.StmtListBuilder builder, List locals, ExpressionTranslator etran) { Contract.Requires(s != null); - Contract.Requires(bodyTr != null); Contract.Requires(builder != null); Contract.Requires(locals != null); Contract.Requires(etran != null); @@ -8253,31 +8254,36 @@ namespace Microsoft.Dafny { guardBreak.Add(new Bpl.BreakCmd(s.Tok, null)); loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, guard, guardBreak.Collect(s.Tok), null, null)); - // termination checking - if (Contract.Exists(theDecreases, e => e is WildcardExpr)) { - // omit termination checking for this loop - bodyTr(loopBodyBuilder, updatedFrameEtran); - } else { - List oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$"); - // time for the actual loop body - bodyTr(loopBodyBuilder, updatedFrameEtran); - // check definedness of decreases expressions - var toks = new List(); - var types = new List(); - var decrs = new List(); - foreach (Expression e in theDecreases) { - toks.Add(e.tok); - types.Add(e.Type.NormalizeExpand()); - decrs.Add(etran.TrExpr(e)); - } - Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false); - string msg; - if (s.InferredDecreases) { - msg = "cannot prove termination; try supplying a decreases clause for the loop"; + if (bodyTr != null) { + // termination checking + if (Contract.Exists(theDecreases, e => e is WildcardExpr)) { + // omit termination checking for this loop + bodyTr(loopBodyBuilder, updatedFrameEtran); } else { - msg = "decreases expression might not decrease"; + List oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$"); + // time for the actual loop body + bodyTr(loopBodyBuilder, updatedFrameEtran); + // check definedness of decreases expressions + var toks = new List(); + var types = new List(); + var decrs = new List(); + foreach (Expression e in theDecreases) { + toks.Add(e.tok); + types.Add(e.Type.NormalizeExpand()); + decrs.Add(etran.TrExpr(e)); + } + Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false); + string msg; + if (s.InferredDecreases) { + msg = "cannot prove termination; try supplying a decreases clause for the loop"; + } else { + msg = "decreases expression might not decrease"; + } + loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg)); } - loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg)); + } else { + loopBodyBuilder.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + // todo(maria): havoc stuff } // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check // of invariant-maintenance can use the appropriate canCall predicates. @@ -8474,7 +8480,7 @@ namespace Microsoft.Dafny { ins.AddRange(trTypeArgs(tySubst, tyArgs)); // Translate receiver argument, if any - Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type); + Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type); if (!method.IsStatic) { if (bReceiver == null && !(dafnyReceiver is ThisExpr)) { CheckNonNull(dafnyReceiver.tok, dafnyReceiver, builder, etran, null); @@ -8511,7 +8517,7 @@ namespace Microsoft.Dafny { } TrStmt_CheckWellformed(actual, builder, locals, etran, true); builder.Add(new CommentCmd("ProcessCallStmt: CheckSubrange")); - // Check the subrange without boxing + // Check the subrange without boxing var beforeBox = etran.TrExpr(actual); CheckSubrange(actual.tok, beforeBox, Resolver.SubstType(formal.Type, tySubst), builder); bActual = CondApplyBox(actual.tok, beforeBox, actual.Type, formal.Type); @@ -8937,9 +8943,9 @@ namespace Microsoft.Dafny { } /// - /// Therefore, these properties are applied to method in-parameters. + /// Therefore, these properties are applied to method in-parameters. /// For now, this only allows you to case split on incoming data type values. - /// This used to add IsGood[Multi]Set_Extendend, but that is always + /// This used to add IsGood[Multi]Set_Extendend, but that is always /// added for sets & multisets now in the prelude. /// Bpl.Expr GetExtendedWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran) { @@ -8975,9 +8981,9 @@ namespace Microsoft.Dafny { } else if (type is SeqType) { return FunctionCall(Token.NoToken, "TSeq", predef.Ty, TypeToTy(((CollectionType)type).Arg)); } else if (type is MapType) { - return FunctionCall(Token.NoToken, "TMap", predef.Ty, + return FunctionCall(Token.NoToken, "TMap", predef.Ty, TypeToTy(((MapType)type).Domain), - TypeToTy(((MapType)type).Range)); + TypeToTy(((MapType)type).Range)); } else if (type is BoolType) { return new Bpl.IdentifierExpr(Token.NoToken, "TBool", predef.Ty); } else if (type is CharType) { @@ -8997,7 +9003,7 @@ namespace Microsoft.Dafny { } else if (type is UserDefinedType) { // Classes, (co-)datatypes var args = type.TypeArgs.ConvertAll(TypeToTy); - return ClassTyCon(((UserDefinedType)type), args); + return ClassTyCon(((UserDefinedType)type), args); } else if (type is ParamTypeProxy) { return trTypeParam(((ParamTypeProxy)type).orig, null); } else { @@ -9014,7 +9020,7 @@ namespace Microsoft.Dafny { return "#$" + x.Name; } } - + Bpl.Expr trTypeParam(TypeParameter x, List tyArguments) { Contract.Requires(x != null); var nm = nameTypeParam(x); @@ -9043,8 +9049,8 @@ namespace Microsoft.Dafny { if (d is ClassDecl) { return Concat(GetTypeParams(d.Module), d.TypeArgs); } else if (d is DatatypeDecl) { - return Concat(GetTypeParams(d.Module), d.TypeArgs); - } else if (d is ModuleDefinition) { + return Concat(GetTypeParams(d.Module), d.TypeArgs); + } else if (d is ModuleDefinition) { return new List(); } else { Contract.Assert(false); @@ -9060,7 +9066,7 @@ namespace Microsoft.Dafny { } } - // Boxes, if necessary + // Boxes, if necessary Bpl.Expr MkIs(Bpl.Expr x, Type t) { return MkIs(x, TypeToTy(t), ModeledAsBoxType(t)); } @@ -9496,7 +9502,7 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true); - Bpl.Expr bRhs = etran.TrExpr(e.Expr); + Bpl.Expr bRhs = etran.TrExpr(e.Expr); CheckSubrange(tok, bRhs, checkSubrangeType, builder); bRhs = CondApplyBox(tok, bRhs, e.Expr.Type, lhsType); @@ -9592,7 +9598,7 @@ namespace Microsoft.Dafny { if (tp.NormalizeExpand() is NatType) { return MkIs(bRhs, tp); } else { - return Bpl.Expr.True; + return Bpl.Expr.True; } } @@ -9766,7 +9772,7 @@ namespace Microsoft.Dafny { public readonly bool UsesHeap; public readonly bool UsesOldHeap; public readonly Type ThisType; // null if 'this' is not used - public LetSuchThatExprInfo(IToken tok, int uniqueLetId, + public LetSuchThatExprInfo(IToken tok, int uniqueLetId, List freeVariables, List freeTypeVars, bool usesHeap, bool usesOldHeap, Type thisType, Declaration currentDeclaration) { Tok = tok; @@ -9793,7 +9799,7 @@ namespace Microsoft.Dafny { Tok = template.Tok; LetId = template.LetId; // reuse the ID, which ensures we get the same $let functions FTVs = template.FTVs; - FTV_Types = template.FTV_Types.ConvertAll(t => Resolver.SubstType(t, typeMap)); + FTV_Types = template.FTV_Types.ConvertAll(t => Resolver.SubstType(t, typeMap)); FVs = template.FVs; FV_Exprs = template.FV_Exprs.ConvertAll(e => translator.Substitute(e, null, substMap, typeMap)); UsesHeap = template.UsesHeap; @@ -9933,7 +9939,7 @@ namespace Microsoft.Dafny { public readonly string FunctionName; public readonly bool UsesHeap; public readonly bool UsesOldHeap; - public readonly List TyArgs; // Note: also has a bunch of type arguments + public readonly List TyArgs; // Note: also has a bunch of type arguments public readonly List Args; public BoogieFunctionCall(IToken tok, string functionName, bool usesHeap, bool usesOldHeap, List args, List tyArgs) : base(tok) @@ -9964,7 +9970,7 @@ namespace Microsoft.Dafny { public readonly string This; public readonly string modifiesFrame; // the name of the context's frame variable. readonly Function applyLimited_CurrentFunction; - public readonly Bpl.Expr layerInterCluster; + public readonly Bpl.Expr layerInterCluster; public readonly Bpl.Expr layerIntraCluster = null; // a value of null says to do the same as for inter-cluster calls public int Statistics_CustomLayerFunctionCount = 0; public readonly bool ProducingCoCertificates = false; @@ -10066,7 +10072,7 @@ namespace Microsoft.Dafny { Contract.Requires(thisVar != null); } - public ExpressionTranslator(ExpressionTranslator etran, Bpl.Expr heap) + public ExpressionTranslator(ExpressionTranslator etran, Bpl.Expr heap) : this(etran.translator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.modifiesFrame) { Contract.Requires(etran != null); @@ -10098,7 +10104,7 @@ namespace Microsoft.Dafny { } } - public ExpressionTranslator WithLayer(Bpl.Expr layerArgument) + public ExpressionTranslator WithLayer(Bpl.Expr layerArgument) { Contract.Requires(layerArgument != null); Contract.Ensures(Contract.Result() != null); @@ -10490,7 +10496,7 @@ namespace Microsoft.Dafny { Func TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg), arg.Type); - var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType, + var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType, Concat(Map(tt.TypeArgs,translator.TypeToTy), Cons(TrExpr(e.Function), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg)))))); @@ -10773,7 +10779,7 @@ namespace Microsoft.Dafny { return translator.FunctionCall(expr.tok, "INTERNAL_mul_boogie", Bpl.Type.Int, e0, e1); } } - + case BinaryExpr.ResolvedOpcode.Div: if (isReal) { typ = Bpl.Type.Real; @@ -10971,7 +10977,7 @@ namespace Microsoft.Dafny { if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) { // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body var ly = BplBoundVar(e.Refresh("$ly", ref translator.otherTmpVarCount), predef.LayerType, bvars); - Expr layer = translator.LayerSucc(ly); + Expr layer = translator.LayerSucc(ly); bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layer, layer, modifiesFrame); } if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) { @@ -10995,7 +11001,7 @@ namespace Microsoft.Dafny { tt.Add(bodyEtran.TrExpr(arg)); } tr = new Bpl.Trigger(expr.tok, true, tt, tr); - } + } } if (e.Range != null) { antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); @@ -11131,8 +11137,8 @@ namespace Microsoft.Dafny { Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), et.IsAlloced(e.tok, o)); Bpl.Expr consequent = translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null); - Bpl.Expr rdbody = - new Bpl.LambdaExpr(e.tok, new List(), rdvars, null, + Bpl.Expr rdbody = + new Bpl.LambdaExpr(e.tok, new List(), rdvars, null, BplImp(ante, consequent)); return translator.Lit( @@ -11141,8 +11147,8 @@ namespace Microsoft.Dafny { translator.FunctionCall(e.tok, translator.Handle(e.BoundVars.Count), predef.BoxType, new Bpl.LambdaExpr(e.tok, new List(), bvars, null, ebody), new Bpl.LambdaExpr(e.tok, new List(), bvars, null, reqbody), - new Bpl.LambdaExpr(e.tok, new List(), bvars, null, rdbody))), - layerIntraCluster ?? layerInterCluster), + new Bpl.LambdaExpr(e.tok, new List(), bvars, null, rdbody))), + layerIntraCluster ?? layerInterCluster), predef.HandleType); } @@ -11253,12 +11259,12 @@ namespace Microsoft.Dafny { List args = new List(); - // first add type arguments + // first add type arguments var tyParams = GetTypeParams(e.Function); var tySubst = e.TypeArgumentSubstitutions; Contract.Assert(tyParams.Count == tySubst.Count); args.AddRange(translator.trTypeArgs(tySubst, tyParams)); - + if (layerArgument != null) { args.Add(layerArgument); } @@ -11438,7 +11444,7 @@ namespace Microsoft.Dafny { // --------------- help routines --------------- public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) { - return translator.IsAlloced(tok, HeapExpr, e); + return translator.IsAlloced(tok, HeapExpr, e); } public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) { @@ -11456,7 +11462,7 @@ namespace Microsoft.Dafny { Contract.Requires(e != null); Contract.Requires(ty != null); - Bpl.Expr tr_ty = translator.TypeToTy(ty); + Bpl.Expr tr_ty = translator.TypeToTy(ty); Bpl.Expr alloc = IsAlloced(tok, e); if (isNew) { @@ -11475,7 +11481,7 @@ namespace Microsoft.Dafny { LayerSucc, CharFromInt, CharToInt, - + Is, IsBox, IsAlloc, IsAllocBox, @@ -12042,12 +12048,12 @@ namespace Microsoft.Dafny { } Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IToken tok, Dictionary substMap = null) - { + { Bpl.Trigger tr = null; for (Attributes aa = attribs; aa != null; aa = aa.Prev) { if (aa.Name == "trigger") { List tt = new List(); - foreach (var arg in aa.Args) { + foreach (var arg in aa.Args) { if (substMap == null) { tt.Add(etran.TrExpr(arg)); } else { @@ -12163,8 +12169,8 @@ namespace Microsoft.Dafny { var A2 = etran2.TrExpr(e.E1); var B2 = etran2.TrExpr(e.E2); var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr); - // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+ - Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2); + // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+ + Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2); foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) { var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c)); splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); @@ -12284,7 +12290,7 @@ namespace Microsoft.Dafny { } // body - var trBody = etran.TrExpr(typeSpecializedBody); + var trBody = etran.TrExpr(typeSpecializedBody); trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type); // F#canCall(args) && F(args) && (b0 && b1 && b2) var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody)); @@ -12294,8 +12300,8 @@ namespace Microsoft.Dafny { } } - } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) - /* NB: only for type arg less quantifiers for now: */ + } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) + /* NB: only for type arg less quantifiers for now: */ && ((QuantifierExpr)expr).TypeArgs.Count == 0) { var e = (QuantifierExpr)expr; var inductionVariables = ApplyInduction(e); @@ -12377,7 +12383,7 @@ namespace Microsoft.Dafny { Bpl.Expr q; if (position) { if (Attributes.Contains(e.Attributes, "trigger")) { - Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok); + Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok); q = new Bpl.ForallExpr(kase.tok, bvars, tr, Bpl.Expr.Imp(ante, bdy)); } else { q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy)); @@ -12820,7 +12826,7 @@ namespace Microsoft.Dafny { } static void ComputeFreeTypeVariables(Type ty, ISet fvs) { - // Add type parameters, unless they are abstract type declarations: they are in scope + // Add type parameters, unless they are abstract type declarations: they are in scope if (ty.IsTypeParameter && ! ty.AsTypeParameter.IsAbstractTypeDeclaration) { fvs.Add(ty.AsTypeParameter); } @@ -13087,7 +13093,7 @@ namespace Microsoft.Dafny { DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs); newDtv.Ctor = dtv.Ctor; // resolve on the fly (and set newDtv.Type below, at end) newDtv.InferredTypeArgs = Map(dtv.InferredTypeArgs, tt => Resolver.SubstType(tt, typeMap)); - // ^ Set the correct type arguments to the constructor + // ^ Set the correct type arguments to the constructor newExpr = newDtv; } @@ -13473,7 +13479,7 @@ namespace Microsoft.Dafny { var s = (CallStmt)stmt; var rr = new CallStmt(s.Tok, s.EndTok, s.Lhs.ConvertAll(Substitute), Substitute(s.Receiver), s.MethodName, s.Args.ConvertAll(Substitute)); rr.Method = s.Method; - rr.TypeArgumentSubstitutions = new Dictionary(); + rr.TypeArgumentSubstitutions = new Dictionary(); foreach (var p in s.TypeArgumentSubstitutions) { rr.TypeArgumentSubstitutions[p.Key] = Resolver.SubstType(p.Value, typeMap); } @@ -13778,7 +13784,7 @@ namespace Microsoft.Dafny { Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); - if (a == Bpl.Expr.True) { + if (a == Bpl.Expr.True) { return b; } else if (b == Bpl.Expr.True) { return a; @@ -13812,7 +13818,7 @@ namespace Microsoft.Dafny { } /// - /// lhs should be a Bpl.IdentifierExpr. + /// lhs should be a Bpl.IdentifierExpr. /// Creates lhs := rhs; /// static Bpl.Cmd BplSimplestAssign(Bpl.Expr lhs, Bpl.Expr rhs) { @@ -13845,13 +13851,13 @@ namespace Microsoft.Dafny { } /* This function allows you to replace, for example: - + Bpl.BoundVariable iVar = new Bpl.BoundVariable(e.tok, new Bpl.TypedIdent(e.tok, "$i", Bpl.Type.Int)); Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(e.tok, iVar); - + with: - Bpl.Expr i; var iVar = BplBoundVar("$i", Bpl.Type.Int, out i); + Bpl.Expr i; var iVar = BplBoundVar("$i", Bpl.Type.Int, out i); */ static Bpl.BoundVariable BplBoundVar(string name, Bpl.Type ty, out Bpl.Expr e) { Contract.Requires(ty != null); @@ -13925,7 +13931,7 @@ namespace Microsoft.Dafny { // Utilities for lists and dicts... static List Singleton(A x) { - return Util.Singleton(x); + return Util.Singleton(x); } static List Cons(A x, List xs) { @@ -13933,7 +13939,7 @@ namespace Microsoft.Dafny { } static List Snoc(List xs, A x) { - return Util.Snoc(xs, x); + return Util.Snoc(xs, x); } static List Concat(List xs, List ys) { @@ -13941,9 +13947,9 @@ namespace Microsoft.Dafny { } static List Map(IEnumerable xs, Func f) { - return Util.Map(xs, f); + return Util.Map(xs, f); } - + public static void MapM(IEnumerable xs, Action K) { Contract.Requires(xs != null); diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index 6a49e733..5d356f0a 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -1,6 +1,21 @@ // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" -method M(S: set) { +method M0(S: set) { forall s | s in S ensures s < 0; } + +method M1(x: int) +{ + var i := x; + while (0 < i) + invariant i <= x; +} + +method M2(x: int) +{ + var i := x; + while (0 < i) + invariant i <= x; + decreases i; +} diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect index 5c12e1ef..060f3287 100644 --- a/Test/dafny0/DirtyLoops.dfy.expect +++ b/Test/dafny0/DirtyLoops.dfy.expect @@ -1,4 +1,4 @@ -Dafny program verifier finished with 2 verified, 0 errors +Dafny program verifier finished with 6 verified, 0 errors Dafny program verifier finished with 0 verified, 0 errors -- cgit v1.2.3 From 02e2b99ab18659ea2626e2be5fa369b7f1795334 Mon Sep 17 00:00:00 2001 From: chmaria Date: Sat, 1 Nov 2014 14:59:23 +0100 Subject: Minor fix in test dafny2/SnapshotableTrees.dfy. --- Test/dafny2/SnapshotableTrees.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test') diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy index 96d3707f..b64660b3 100644 --- a/Test/dafny2/SnapshotableTrees.dfy +++ b/Test/dafny2/SnapshotableTrees.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino, September 2011. @@ -266,7 +266,7 @@ class Node if (left == n.left) { r, pos := n, -1; } else { - // assert n.left != null ==> forall e :: e in n.left.Contents ==> e < n.data; + assert n.left != null ==> forall e :: e in n.left.Contents ==> e < n.data; // assert forall e :: e in left.Contents ==> e < n.data; r := new Node.Build(left, n.data, n.right); } -- cgit v1.2.3