diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-08-21 00:24:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-08-21 00:24:08 -0700 |
| commit | b49eb7d6cf575542e34f0105c0fb8c6f3a4a1769 (patch) | |
| tree | 5349325b936244b8ca7dceb55204e7722661e086 /Util | |
| parent | e5faebfb048135e7bed2f569c290a0e4bbd26841 (diff) | |
Dafny and Boogie: get rid of 'static' fields in parser
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs index 16ed18f4..5fa7d91c 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs @@ -191,17 +191,22 @@ namespace DafnyLanguage // Run the verifier
var newErrors = new List<DafnyError>();
- bool success = DafnyDriver.Verify(program, errorInfo => {
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
- foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ try {
+ bool success = DafnyDriver.Verify(program, errorInfo => {
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ foreach (var aux in errorInfo.Aux) {
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ }
+ });
+ if (!success) {
+ newErrors.Clear();
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error"));
}
- });
- errorListHolder.PopulateErrorList(newErrors, true, snapshot);
- if (!success) {
+ } catch (Exception e) {
newErrors.Clear();
- newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error"));
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message));
}
+ errorListHolder.PopulateErrorList(newErrors, true, snapshot);
lock (this) {
bufferChangesPreVerificationStart.Clear();
|