diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-23 10:26:47 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-23 10:26:47 -0700 |
| commit | 1763ad8e4d6b631fe966b394ae2dbafa7d803627 (patch) | |
| tree | 18bf26b129696e1218284b0f62400a0efe92f395 /Source/DafnyExtension | |
| parent | fb4915bc1b95d182b08a45c85d92046489ed1078 (diff) | |
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
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 7 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 32 |
2 files changed, 24 insertions, 15 deletions
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
|