Report warnings only once. (This is the last step in fixing Issue #86.)

3 files changed, 43 insertions, 6 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 66fd7959..3e308e76 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -50,15 +50,27 @@ namespace Microsoft.Dafny
       Contract.Requires(msg != null);

       Error(e.tok, msg, args);

     }

+

+    private bool reportWarnings = true;

+    /// <summary>

+    /// Set whether or not to report warnings. Return the state of the previous behavior.

+    /// </summary>

+    public bool ReportWarnings(bool b) {

+      var old = reportWarnings;

+      reportWarnings = b;

+      return old;

+    }

     public void Warning(IToken tok, string msg, params object[] args) {

       Contract.Requires(tok != null);

       Contract.Requires(msg != null);

-      ConsoleColor col = Console.ForegroundColor;

-      Console.ForegroundColor = ConsoleColor.Yellow;

-      Console.WriteLine("{0}({1},{2}): Warning: {3}",

-          DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

-          string.Format(msg, args));

-      Console.ForegroundColor = col;

+      if (reportWarnings) {

+        ConsoleColor col = Console.ForegroundColor;

+        Console.ForegroundColor = ConsoleColor.Yellow;

+        Console.WriteLine("{0}({1},{2}): Warning: {3}",

+            DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

+            string.Format(msg, args));

+        Console.ForegroundColor = col;

+      }

     }

   }

 

@@ -366,6 +378,7 @@ namespace Microsoft.Dafny
             // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include);

             Contract.Assert(!useCompileSignatures);

             useCompileSignatures = true;  // set Resolver-global flag to indicate that Signatures should be followed to their CompiledSignature

+            var oldWarnings = ReportWarnings(false);  // turn off warning reporting for the clone

             var nw = new Cloner().CloneModuleDefinition(m, m.CompileName + "_Compile");

             var compileSig = RegisterTopLevelDecls(nw, true);

             compileSig.Refines = refinementTransformer.RefinedSig;

@@ -373,6 +386,7 @@ namespace Microsoft.Dafny
             ResolveModuleDefinition(nw, compileSig);

             prog.CompileModules.Add(nw);

             useCompileSignatures = false;  // reset the flag

+            ReportWarnings(oldWarnings);

           }

         } else if (decl is AliasModuleDecl) {

           var alias = (AliasModuleDecl)decl;

diff --git a/Test/dafny0/JustWarnings.dfy b/Test/dafny0/JustWarnings.dfy
new file mode 100644
index 00000000..86523f5b
--- /dev/null
+++ b/Test/dafny0/JustWarnings.dfy
@@ -0,0 +1,19 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file tests the behavior where the Resolver reports some warnings

+// but no errors.  In the case of errors, resolution does not continue

+// to clone modules and resolve them, but the cloning does proceed if there

+// are only warnings.  Dafny should report only one copy of these warnings,

+// and warnings are therefore turned off when processing the clones.  This

+// test file makes sure the warnings don't appear twice.

+

+method M(x: int)

+{

+  var x := 10;  // warning: this shadows the parameter 'x'

+}

+

+class C<T> {

+  var u: T

+  method P<T>(t: T)  // warning: this shadows the type parameter 'T'

+}

diff --git a/Test/dafny0/JustWarnings.dfy.expect b/Test/dafny0/JustWarnings.dfy.expect
new file mode 100644
index 00000000..5f0e66d8
--- /dev/null
+++ b/Test/dafny0/JustWarnings.dfy.expect
@@ -0,0 +1,4 @@
+JustWarnings.dfy(18,11): Warning: Shadowed type-parameter name: T

+JustWarnings.dfy(13,6): Warning: Shadowed local-variable name: x

+

+Dafny program verifier finished with 3 verified, 0 errors