From 1763ad8e4d6b631fe966b394ae2dbafa7d803627 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 23 Jul 2015 10:26:47 -0700
Subject: 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
---
 Source/Dafny/Resolver.cs                |  4 ++--
 Source/DafnyExtension/DafnyDriver.cs    |  7 +++++++
 Source/DafnyExtension/ResolverTagger.cs | 32 +++++++++++++++++---------------
 3 files changed, 26 insertions(+), 17 deletions(-)

(limited to 'Source')

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
-- 
cgit v1.2.3