From 1ac82df441e621fce2f38d53b5d17c69650d7358 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 21 Aug 2012 00:24:08 -0700 Subject: Dafny and Boogie: get rid of 'static' fields in parser --- .../DafnyExtension/DafnyExtension/ProgressMargin.cs | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) (limited to 'Util') 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(); - 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(); -- cgit v1.2.3