Dafny: fixed bug in which _module scope declarations were not verified.

1 files changed, 7 insertions, 1 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index ca8f934e..3ccdeab1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -154,12 +154,18 @@ Dafny
     )

   }

   (. // find the default class in the default module, then append membersDefaultClass to its member list

+     DefaultClassDecl defaultClass;

      foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

-       DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+       defaultClass = topleveldecl as DefaultClassDecl;

        if (defaultClass != null) {

          defaultClass.Members.AddRange(membersDefaultClass);

          break;

        }

+     }

+     if (defaultClass == null) { // create the default class here, because it wasn't found

+       defaultClass = new DefaultClassDecl();

+       defaultModule.TopLevelDecls.Add(defaultClass);

+       defaultClass.Members.AddRange(membersDefaultClass);

      } .)

   EOF

   .