diff options
| author |  wuestholz <unknown> | 2013-06-10 10:09:58 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-10 10:09:58 -0700 |
| commit | 453c7e07915a29bd7d5250769cad5763ea6668b3 (patch) | |
| tree | 3e29fbcafece3b8507d53f6f8212dc9e86f400c5 /Source/DafnyExtension/ProgressMargin.cs | |
| parent | 5b726294d6604001ec162edb4e95d17c0f32b5eb (diff) | |
DafnyExtension: Improved the way errors (incl. locations) are kept up-to-date.
Diffstat (limited to 'Source/DafnyExtension/ProgressMargin.cs')
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs index 4eb150f5..d587d3dd 100644 --- a/Source/DafnyExtension/ProgressMargin.cs +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -275,21 +275,22 @@ namespace DafnyLanguage try {
bool success = DafnyDriver.Verify(program, snapshot, errorInfo =>
{
- ITextSnapshot ss = null;
+ ITextSnapshot s = snapshot;
if (errorInfo.RequestId != null)
{
- ss = DafnyDriver.RequestIdToSnapshot[errorInfo.RequestId];
+ Contract.Assert(DafnyDriver.RequestIdToSnapshot.ContainsKey(errorInfo.RequestId));
+ s = DafnyDriver.RequestIdToSnapshot[errorInfo.RequestId];
}
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, ss));
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, s));
foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg, ss));
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg, s));
}
});
if (!success) {
- newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error"));
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error", snapshot));
}
} catch (Exception e) {
- newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message));
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message, snapshot));
}
errorListHolder.PopulateErrorList(newErrors, true, snapshot);
|