diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 10:28:47 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 10:28:47 -0700 |
| commit | cfdaf4ccbea24636f2a94ca9d2f75b8699921d60 (patch) | |
| tree | 1e63b48b77f43980dbc41cfc5a6e7affd0e700ef | |
| parent | a8e619e3e23d5c426ef583411c3ddf223bc26fbe (diff) | |
Mark a few reporting functions as static
| -rw-r--r-- | Source/Dafny/Reporting.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index c3797574..77869d9f 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -122,15 +122,15 @@ namespace Microsoft.Dafny { Info(source, tok, String.Format(msg, args));
}
- public string ErrorToString(ErrorLevel header, IToken tok, string msg) {
+ public static string ErrorToString(ErrorLevel header, IToken tok, string msg) {
return ErrorToString_Internal(": " + header.ToString(), tok.filename, tok.line, tok.col, ": " + msg);
}
- public string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {
+ public static string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {
return ErrorToString_Internal(": " + header.ToString(), filename, oneBasedLine, oneBasedColumn, ": " + msg);
}
- public string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {
+ public static string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {
return String.Format("{0}({1},{2}){3}{4}", filename, oneBasedLine, oneBasedColumn - 1, header, msg ?? "");
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8146d2cf..e39b777d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3585,7 +3585,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);
var col = tok.col + (isEndToken ? tok.val.Length : 0);
- string description = reporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? "");
+ string description = ErrorReporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? "");
QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);
return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);
}
|