Fix: Visual studio did not show warnings.

To check if the fix works, try declaring a static top level function.
Initial work on this patch by Rustan

3 files changed, 26 insertions, 17 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 26349ef5..44990d7d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -51,7 +51,7 @@ namespace Microsoft.Dafny
       Error(e.tok, msg, args);

     }

 

-    private bool reportWarnings = true;

+    protected bool reportWarnings = true;

     /// <summary>

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

     /// </summary>

@@ -60,7 +60,7 @@ namespace Microsoft.Dafny
       reportWarnings = b;

       return old;

     }

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

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

       Contract.Requires(tok != null);

       Contract.Requires(msg != null);

       if (reportWarnings) {

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 7f39fe34..8300213c 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -182,6 +182,13 @@ namespace DafnyLanguage
         dd.RecordError(tok.filename, tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);

         ErrorCount++;

       }

+

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

+        if (reportWarnings) {

+          string s = string.Format(msg, args);

+          dd.RecordError(tok.filename, tok.line - 1, tok.col - 1, ErrorCategory.ResolveWarning, s);

+        }

+      }

     }

 

     #endregion

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 1fdd3827..4237041f 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -68,26 +68,27 @@ namespace DafnyLanguage
     {

       Error = error;

     }

-    

-    private static string ConvertToErrorType(DafnyError err)

-    {

-      string ty;  // the COLORs below indicate what I see on my machine

-      switch (err.Category)

-      {

-        default:  // unexpected category

+

+    private static string ConvertToErrorType(DafnyError err) {

+      // the COLORs below indicate what I see on my machine

+      switch (err.Category) {

+        case ErrorCategory.ProcessError:

         case ErrorCategory.ParseError:

         case ErrorCategory.ParseWarning:

-          ty = "syntax error"; break;  // COLOR: red

+          return "syntax error";  // COLOR: red

         case ErrorCategory.ResolveError:

-          ty = "compiler error"; break;  // COLOR: blue

+          return "compiler error";  // COLOR: blue

+        case ErrorCategory.ResolveWarning:

+          return "compiler warning";  // COLOR: blue

+        case ErrorCategory.InternalError:

         case ErrorCategory.VerificationError:

-          ty = "error"; break;  // COLOR: red

+          return "error";  // COLOR: red

         case ErrorCategory.AuxInformation:

-          ty = "other error"; break;  // COLOR: purple red

-        case ErrorCategory.InternalError:

-          ty = "error"; break;  // COLOR: red

+          return "other error";  // COLOR: purple red

+        default:

+          Contract.Assert(false);

+          throw new InvalidOperationException();

       }

-      return ty;

     }

   }

 

@@ -412,6 +413,7 @@ namespace DafnyLanguage
         case ErrorCategory.InternalError:

           return TaskErrorCategory.Error;

         case ErrorCategory.ParseWarning:

+        case ErrorCategory.ResolveWarning:

           return TaskErrorCategory.Warning;

         case ErrorCategory.AuxInformation:

           return TaskErrorCategory.Message;

@@ -477,7 +479,7 @@ namespace DafnyLanguage
 

   public enum ErrorCategory

   {

-    ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError

+    ProcessError, ParseWarning, ParseError, ResolveWarning, ResolveError, VerificationError, AuxInformation, InternalError

   }

 

   public class DafnyError