diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 4 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 7 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 32 |
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
|