IronDafny related changes:

- diabled error message related to ensures clauses requiring function bodies in the case of abstract modules.
- fixed bug in similar error message related to bodyless methods in abstract modules.

1 files changed, 8 insertions, 8 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f30542d0..c4f038d4 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -573,7 +573,7 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
         | NewtypeDecl<module, out td>                  (. module.TopLevelDecls.Add(td); .)

         | OtherTypeDecl<module, out td>                (. module.TopLevelDecls.Add(td); .)

         | IteratorDecl<module, out iter>               (. module.TopLevelDecls.Add(iter); .)

-        | ClassMemberDecl<namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, true>

+        | ClassMemberDecl<namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, DafnyOptions.O.IronDafny && isAbstract>

         }

       "}"                                  (. module.BodyEndTok = t;

                                               module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));

@@ -663,7 +663,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
     .)

 	.

 

-ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl.>

+ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl, bool isWithinAbstractModule.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Method/*!*/ m;

      Function/*!*/ f;

@@ -687,7 +687,7 @@ ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDe
          mmod.IsStatic = false;

        }

     .)

-    FunctionDecl<mmod, out f>                   (. mm.Add(f); .)

+    FunctionDecl<mmod, isWithinAbstractModule, out f>                   (. mm.Add(f); .)

   | (. if (moduleLevelDecl && staticToken != null) {

          errors.Warning(staticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");

          mmod.IsStatic = false;

@@ -697,7 +697,7 @@ ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDe
          mmod.IsProtected = false;

        }

     .)

-    MethodDecl<mmod, allowConstructors, permitAbstractDecl, out m>  (. mm.Add(m); .)

+    MethodDecl<mmod, allowConstructors, isWithinAbstractModule, out m>  (. mm.Add(m); .)

   )

   .

 DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>

@@ -949,7 +949,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
   ">"

   .

 /*------------------------------------------------------------------------*/

-MethodDecl<MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl, out Method/*!*/ m>

+MethodDecl<MemberModifiers mmod, bool allowConstructor, bool isWithinAbstractModule, out Method/*!*/ m>

 = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);

      IToken/*!*/ id = Token.NoToken;

      bool hasName = false;  IToken keywordToken;

@@ -1030,7 +1030,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl,
   [ BlockStmt<out body, out bodyStart, out bodyEnd>

   ]

   (.

-     if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {

+     if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {

         SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

      }

 

@@ -1253,7 +1253,7 @@ GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
   ">"

   .

 /*------------------------------------------------------------------------*/

-FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>

+FunctionDecl<MemberModifiers mmod, bool isWithinAbstractModule, out Function/*!*/ f>

 = (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);

      Attributes attrs = null;

      IToken/*!*/ id = Token.NoToken;  // to please compiler

@@ -1338,7 +1338,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   { FunctionSpec<reqs, reads, ens, decreases> }

   [ FunctionBody<out body, out bodyStart, out bodyEnd>

   ]

-  (. if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) {

+  (. if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) {

         SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

      }