diff options
| author |  wuestholz <unknown> | 2013-06-03 11:10:25 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-03 11:10:25 -0700 |
| commit | 285de81d5746bf53aa2296fa43c79949c5c2f1a0 (patch) | |
| tree | 6f833fb736530d54d6e65d9507831ea12032b6e3 | |
| parent | 2927e2cc553a6d82ca7c7afeb9cb5d96fed7aa6d (diff) | |
Did some refactoring of the Dafny drivers.
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 1 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 134 |
2 files changed, 74 insertions, 61 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index f3da0ec2..f1a9ae80 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -293,7 +293,6 @@ namespace Microsoft.Dafny }
-
static void ReportBplError(IToken tok, string message, bool error)
{
Contract.Requires(message != null);
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 095dd843..9e93eb1e 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -104,6 +104,80 @@ namespace DafnyLanguage }
}
+ public delegate void ErrorReporterDelegate(DafnyErrorInformation errInfo);
+
+ public class DafnyErrorInformation
+ {
+ public readonly Bpl.IToken Tok;
+ public readonly string Msg;
+ public readonly List<DafnyErrorAuxInfo> Aux = new List<DafnyErrorAuxInfo>();
+
+ public class DafnyErrorAuxInfo
+ {
+ public readonly Bpl.IToken Tok;
+ public readonly string Msg;
+ public DafnyErrorAuxInfo(Bpl.IToken tok, string msg)
+ {
+ Tok = tok;
+ Msg = CleanUp(msg);
+ }
+ }
+
+ public DafnyErrorInformation(Bpl.IToken tok, string msg)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Tok = tok;
+ Msg = CleanUp(msg);
+ AddNestingsAsAux(tok);
+ }
+ public void AddAuxInfo(Bpl.IToken tok, string msg)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Aux.Add(new DafnyErrorAuxInfo(tok, msg));
+ AddNestingsAsAux(tok);
+ }
+ void AddNestingsAsAux(Bpl.IToken tok)
+ {
+ while (tok is Dafny.NestedToken)
+ {
+ var nt = (Dafny.NestedToken)tok;
+ tok = nt.Inner;
+ Aux.Add(new DafnyErrorAuxInfo(tok, "Related location"));
+ }
+ }
+ public void AddAuxInfo(Bpl.QKeyValue attr)
+ {
+ while (attr != null)
+ {
+ if (attr.Key == "msg" && attr.Params.Count == 1 && attr.tok.line != 0 && attr.tok.col != 0)
+ {
+ var str = attr.Params[0] as string;
+ if (str != null)
+ {
+ AddAuxInfo(attr.tok, str);
+ }
+ }
+ attr = attr.Next;
+ }
+ }
+
+ public static string CleanUp(string msg)
+ {
+ if (msg.ToLower().StartsWith("error: "))
+ {
+ return msg.Substring(7);
+ }
+ else
+ {
+ return msg;
+ }
+ }
+ }
+
public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) {
Dafny.Translator translator = new Dafny.Translator();
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
@@ -362,65 +436,5 @@ namespace DafnyLanguage return PipelineOutcome.VerificationCompleted;
}
- public delegate void ErrorReporterDelegate(DafnyErrorInformation errInfo);
-
- public class DafnyErrorInformation
- {
- public readonly Bpl.IToken Tok;
- public readonly string Msg;
- public readonly List<DafnyErrorAuxInfo> Aux = new List<DafnyErrorAuxInfo>();
-
- public class DafnyErrorAuxInfo
- {
- public readonly Bpl.IToken Tok;
- public readonly string Msg;
- public DafnyErrorAuxInfo(Bpl.IToken tok, string msg) {
- Tok = tok;
- Msg = CleanUp(msg);
- }
- }
-
- public DafnyErrorInformation(Bpl.IToken tok, string msg) {
- Contract.Requires(tok != null);
- Contract.Requires(1 <= tok.line && 1 <= tok.col);
- Contract.Requires(msg != null);
- Tok = tok;
- Msg = CleanUp(msg);
- AddNestingsAsAux(tok);
- }
- public void AddAuxInfo(Bpl.IToken tok, string msg) {
- Contract.Requires(tok != null);
- Contract.Requires(1 <= tok.line && 1 <= tok.col);
- Contract.Requires(msg != null);
- Aux.Add(new DafnyErrorAuxInfo(tok, msg));
- AddNestingsAsAux(tok);
- }
- void AddNestingsAsAux(Bpl.IToken tok) {
- while (tok is Dafny.NestedToken) {
- var nt = (Dafny.NestedToken)tok;
- tok = nt.Inner;
- Aux.Add(new DafnyErrorAuxInfo(tok, "Related location"));
- }
- }
- public void AddAuxInfo(Bpl.QKeyValue attr) {
- while (attr != null) {
- if (attr.Key == "msg" && attr.Params.Count == 1 && attr.tok.line != 0 && attr.tok.col != 0) {
- var str = attr.Params[0] as string;
- if (str != null) {
- AddAuxInfo(attr.tok, str);
- }
- }
- attr = attr.Next;
- }
- }
-
- public static string CleanUp(string msg) {
- if (msg.ToLower().StartsWith("error: ")) {
- return msg.Substring(7);
- } else {
- return msg;
- }
- }
- }
}
}
|