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

1 files changed, 17 insertions, 15 deletions

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