Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and visually indicates a non-verified buffer

4 files changed, 469 insertions, 305 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index f5f41e2c..3298be4b 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -33,80 +33,6 @@ namespace DafnyLanguage
       _errors.Add(new DafnyError(line, col, cat, msg));

     }

 

-    void RecordProcessError(string msg) {

-      RecordError(0, 0, ErrorCategory.ProcessError, msg);

-    }

-

-    public void Process_ViaBatchFile() {

-      if (!File.Exists(@"C:\tmp\StartDafny.bat")) {

-        RecordProcessError(@"Can't find C:\tmp\StartDafny.bat");

-      }

-

-      // From: http://dotnetperls.com/process-redirect-standard-output

-      // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx)

-      //

-      // Setup the process with the ProcessStartInfo class.

-      //

-      ProcessStartInfo start = new ProcessStartInfo();

-      start.FileName = @"cmd.exe";

-      start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name.

-      start.UseShellExecute = false;

-      start.RedirectStandardInput = true;

-      start.RedirectStandardOutput = true;

-      start.CreateNoWindow = true;

-      //

-      // Start the process.

-      //

-      using (System.Diagnostics.Process process = System.Diagnostics.Process.Start(start)) {

-        //

-        // Push the file contents to the new process

-        //

-        StreamWriter myStreamWriter = process.StandardInput;

-        myStreamWriter.WriteLine(_programText);

-        myStreamWriter.Close();

-        //

-        // Read in all the text from the process with the StreamReader.

-        //

-        using (StreamReader reader = process.StandardOutput) {

-          for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) {

-            // the lines of interest have the form "filename(line,col): some_error_label: error_message"

-            // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"

-            string message;

-            int n = line.IndexOf("): ", 2);  // we start at 2, to avoid problems with "C:\..."

-            if (n == -1) {

-              continue;

-            } else {

-              int m = line.IndexOf(": ", n + 3);

-              if (m == -1) {

-                continue;

-              }

-              message = line.Substring(m + 2);

-            }

-            line = line.Substring(0, n);  // line now has the form "filename(line,col"

-

-            n = line.LastIndexOf(',');

-            if (n == -1) { continue; }

-            var colString = line.Substring(n + 1);

-            line = line.Substring(0, n);  // line now has the form "filename(line"

-

-            n = line.LastIndexOf('(');

-            if (n == -1) { continue; }

-            var lineString = line.Substring(n + 1);

-

-            try {

-              int errLine = Int32.Parse(lineString) - 1;

-              int errCol = Int32.Parse(colString) - 1;

-              RecordError(errLine, errCol, message.StartsWith("syntax error") ? ErrorCategory.ParseError : ErrorCategory.VerificationError, message);

-            } catch (System.FormatException) {

-              continue;

-            } catch (System.OverflowException) {

-              continue;

-            }

-          }

-        }

-      }

-    }

-

     static DafnyDriver() {

       Initialize();

     }

@@ -114,6 +40,8 @@ namespace DafnyLanguage
     static void Initialize() {

       if (Dafny.DafnyOptions.O == null) {

         Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());

+        Dafny.DafnyOptions.O.DafnyPrelude = "c:\\boogie\\Binaries\\DafnyPrelude.bpl";

+        Dafny.DafnyOptions.O.ApplyDefaultOptions();

       }

     }

 

@@ -174,77 +102,106 @@ namespace DafnyLanguage
       }

     }

 

-#if LATER

-    static bool Verify(Microsoft.Dafny.Program dafnyProgram) {

+    public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) {

       Dafny.Translator translator = new Dafny.Translator();

-      Program boogieProgram = translator.Translate(dafnyProgram);

+      Bpl.Program boogieProgram = translator.Translate(dafnyProgram);

 

       int errorCount, verified, inconclusives, timeOuts, outOfMemories;

-      PipelineOutcome oc = BoogiePipeline(boogieProgram, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

-      switch (oc) {

-        case PipelineOutcome.VerificationCompleted:

-        case PipelineOutcome.Done:  // (this says not to continue with compilation)

-          // WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

-          break;

-        default:

-          // error has already been reported to user

-          break;

-      }

-      return errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0;

+      PipelineOutcome oc = BoogiePipeline(boogieProgram, er, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+      bool allOk = errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0;

+      // TODO:  This would be the place to proceed to compile the program, if desired

+      return allOk;

     }

 

+    enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }

+

     /// <summary>

     /// Resolve, type check, infer invariants for, and verify the given Boogie program.

     /// The intention is that this Boogie program has been produced by translation from something

     /// else.  Hence, any resolution errors and type checking errors are due to errors in

     /// the translation.

     /// </summary>

-    static PipelineOutcome BoogiePipeline(Program/*!*/ program,

+    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ErrorReporterDelegate er,

         out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {

       Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

 

       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

-      PipelineOutcome oc = ResolveAndTypecheck(program);

-      switch (oc) {

-        case PipelineOutcome.Done:

-          return oc;

+      PipelineOutcome oc = BoogieResolveAndTypecheck(program);

+      if (oc == PipelineOutcome.ResolvedAndTypeChecked) {

+        EliminateDeadVariablesAndInline(program);

+        return BoogieInferAndVerify(program, er, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+      }

+      return oc;

+    }

 

-        case PipelineOutcome.ResolutionError:

-        case PipelineOutcome.TypeCheckingError:

-          // the Dafny-to-Boogie translation must have been bad; this is an internal error

-          return oc;

+    static void EliminateDeadVariablesAndInline(Bpl.Program program) {

+      Contract.Requires(program != null);

+      // Eliminate dead variables

+      Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

 

-        case PipelineOutcome.ResolvedAndTypeChecked:

-          return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+      // Collect mod sets

+      if (Bpl.CommandLineOptions.Clo.DoModSetAnalysis) {

+        Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

+      }

 

-        default:

-          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome

+      // Coalesce blocks

+      if (Bpl.CommandLineOptions.Clo.CoalesceBlocks) {

+        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);

       }

-    }

 

+      // Inline

+      var TopLevelDeclarations = program.TopLevelDeclarations;

 

-    enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }

+      if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None) {

+        bool inline = false;

+        foreach (var d in TopLevelDeclarations) {

+          if (d.FindExprAttribute("inline") != null) {

+            inline = true;

+          }

+        }

+        if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0) {

+          foreach (var d in TopLevelDeclarations) {

+            var impl = d as Bpl.Implementation;

+            if (impl != null) {

+              impl.OriginalBlocks = impl.Blocks;

+              impl.OriginalLocVars = impl.LocVars;

+            }

+          }

+          foreach (var d in TopLevelDeclarations) {

+            var impl = d as Bpl.Implementation;

+            if (impl != null && !impl.SkipVerification) {

+              Bpl.Inliner.ProcessImplementation(program, impl);

+            }

+          }

+          foreach (var d in TopLevelDeclarations) {

+            var impl = d as Bpl.Implementation;

+            if (impl != null) {

+              impl.OriginalBlocks = null;

+              impl.OriginalLocVars = null;

+            }

+          }

+        }

+      }

+    }

 

     /// <summary>

-    /// Resolves and type checks the given Boogie program.  Any errors are reported to the

-    /// console.  Returns:

+    /// Resolves and type checks the given Boogie program.

+    /// Returns:

     ///  - Done if no errors occurred, and command line specified no resolution or no type checking.

     ///  - ResolutionError if a resolution error occurred

     ///  - TypeCheckingError if a type checking error occurred

     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

     /// </summary>

-    static PipelineOutcome ResolveAndTypecheck(Program program) {

+    static PipelineOutcome BoogieResolveAndTypecheck(Bpl.Program program) {

       Contract.Requires(program != null);

       // ---------- Resolve ------------------------------------------------------------

-

       int errorCount = program.Resolve();

       if (errorCount != 0) {

         return PipelineOutcome.ResolutionError;

       }

 

       // ---------- Type check ------------------------------------------------------------

-

       errorCount = program.Typecheck();

       if (errorCount != 0) {

         return PipelineOutcome.TypeCheckingError;

@@ -257,12 +214,12 @@ namespace DafnyLanguage
     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

     ///  - Done if command line specified no verification

-    ///  - FatalError if a fatal error occurred, in which case an error has been printed to console

+    ///  - FatalError if a fatal error occurred

     ///  - VerificationCompleted if inference and verification completed, in which the out

     ///    parameters contain meaningful values

     /// </summary>

-    static PipelineOutcome InferAndVerify(Program program,

-                                           out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {

+    static PipelineOutcome BoogieInferAndVerify(Bpl.Program program, ErrorReporterDelegate er,

+                                                out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {

       Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

 

@@ -271,181 +228,192 @@ namespace DafnyLanguage
       // ---------- Infer invariants --------------------------------------------------------

 

       // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

-      Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

+      if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {

+        if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {

+          Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

+        } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) {

+          // run one of the old domains

+          Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

+        } else {

+          // use /infer:j as the default

+          Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;

+          Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

+        }

+      }

 

-      if (CommandLineOptions.Clo.ExpandLambdas) {

-        LambdaHelper.ExpandLambdas(program);

+      if (Bpl.CommandLineOptions.Clo.LoopUnrollCount != -1) {

+        program.UnrollLoops(Bpl.CommandLineOptions.Clo.LoopUnrollCount);

+      }

+

+      if (Bpl.CommandLineOptions.Clo.ExpandLambdas) {

+        Bpl.LambdaHelper.ExpandLambdas(program);

+        //PrintBplFile ("-", program, true);

       }

 

       // ---------- Verify ------------------------------------------------------------

 

-    #region Verify each implementation

+      if (!Bpl.CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }

+

+      #region Verify each implementation

 

       ConditionGeneration vcgen = null;

       try {

-        if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-          vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) {

+          vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

         } else {

-          vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+          vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

         }

-      } catch (ProverException e) {

-        ErrorWriteLine("Fatal Error: ProverException: {0}", e);

+      } catch (Bpl.ProverException) {

         return PipelineOutcome.FatalError;

       }

 

-      foreach (Declaration decl in program.TopLevelDeclarations) {

+      var decls = program.TopLevelDeclarations.ToArray();

+      foreach (var decl in decls) {

         Contract.Assert(decl != null);

-        Implementation impl = decl as Implementation;

-        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

-          List<Counterexample>/*?*/ errors;

-

-          DateTime start = new DateTime();  // to please compiler's definite assignment rules

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

-            start = DateTime.Now;

-            if (CommandLineOptions.Clo.Trace) {

-              Console.WriteLine();

-              Console.WriteLine("Verifying {0} ...", impl.Name);

-            }

-            if (CommandLineOptions.Clo.XmlSink != null) {

-              CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

-            }

-          }

+        Bpl.Implementation impl = decl as Bpl.Implementation;

+        if (impl != null && Bpl.CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification) {

+          List<Bpl.Counterexample>/*?*/ errors;

 

           ConditionGeneration.Outcome outcome;

+          int prevAssertionCount = vcgen.CumulativeAssertionCount;

           try {

-            outcome = vcgen.VerifyImplementation(impl, program, out errors);

-          } catch (VCGenException e) {

-            ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true);

+            outcome = vcgen.VerifyImplementation(impl, out errors);

+          } catch (VCGenException) {

             errors = null;

             outcome = VCGen.Outcome.Inconclusive;

-          } catch (UnexpectedProverOutputException upo) {

-            AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+          } catch (Bpl.UnexpectedProverOutputException) {

             errors = null;

             outcome = VCGen.Outcome.Inconclusive;

           }

 

-          string timeIndication = "";

-          DateTime end = DateTime.Now;

-          TimeSpan elapsed = end - start;

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

-            if (CommandLineOptions.Clo.Trace) {

-              timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

-            }

-          }

-

-

           switch (outcome) {

             default:

-              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome

+              Contract.Assert(false); throw new Exception();  // unexpected outcome

             case VCGen.Outcome.Correct:

-              Inform(String.Format("{0}verified", timeIndication));

               verified++;

               break;

             case VCGen.Outcome.TimedOut:

               timeOuts++;

-              Inform(String.Format("{0}timed out", timeIndication));

               break;

             case VCGen.Outcome.OutOfMemory:

               outOfMemories++;

-              Inform(String.Format("{0}out of memory", timeIndication));

               break;

             case VCGen.Outcome.Inconclusive:

               inconclusives++;

-              Inform(String.Format("{0}inconclusive", timeIndication));

               break;

             case VCGen.Outcome.Errors:

               Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

-                // BP1xxx: Parsing errors

-                // BP2xxx: Name resolution errors

-                // BP3xxx: Typechecking errors

-                // BP4xxx: Abstract interpretation errors (Is there such a thing?)

-                // BP5xxx: Verification errors

-

-                errors.Sort(new CounterexampleComparer());

-                foreach (Counterexample error in errors) {

-                  if (error is CallCounterexample) {

-                    CallCounterexample err = (CallCounterexample)error;

-                    ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true);

-                    ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false);

-                  } else if (error is ReturnCounterexample) {

-                    ReturnCounterexample err = (ReturnCounterexample)error;

-                    ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true);

-                    ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);

-                  } else // error is AssertCounterexample

-                  {

-                    AssertCounterexample err = (AssertCounterexample)error;

-                    if (err.FailingAssert is LoopInitAssertCmd) {

-                      ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true);

-                    } else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

-                      // this assertion is a loop invariant which is not maintained

-                      ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true);

-                    } else {

-                      string msg = err.FailingAssert.ErrorData as string;

-                      if (msg == null) {

-                        msg = "Error BP5001: This assertion might not hold.";

-                      }

-                      ReportBplError(err.FailingAssert, msg, true);

+

+              errors.Sort(new Bpl.CounterexampleComparer());

+              foreach (var error in errors) {

+                DafnyErrorInformation errorInfo;

+

+                if (error is Bpl.CallCounterexample) {

+                  var err = (Bpl.CallCounterexample)error;

+                  errorInfo = new DafnyErrorInformation(err.FailingCall.tok, err.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.");

+                  errorInfo.AddAuxInfo(err.FailingRequires.tok, err.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");

+

+                } else if (error is Bpl.ReturnCounterexample) {

+                  var err = (Bpl.ReturnCounterexample)error;

+                  errorInfo = new DafnyErrorInformation(err.FailingReturn.tok, "A postcondition might not hold on this return path.");

+                  errorInfo.AddAuxInfo(err.FailingEnsures.tok, err.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");

+                  errorInfo.AddAuxInfo(err.FailingEnsures.Attributes);

+

+                } else { // error is AssertCounterexample

+                  var err = (Bpl.AssertCounterexample)error;

+                  if (err.FailingAssert is Bpl.LoopInitAssertCmd) {

+                    errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not hold on entry.");

+                  } else if (err.FailingAssert is Bpl.LoopInvMaintainedAssertCmd) {

+                    // this assertion is a loop invariant which is not maintained

+                    errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not be maintained by the loop.");

+                  } else {

+                    string msg = err.FailingAssert.ErrorData as string;

+                    if (msg == null) {

+                      msg = "This assertion might not hold.";

                     }

+                    errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, msg);

+                    errorInfo.AddAuxInfo(err.FailingAssert.Attributes);

                   }

-                  if (CommandLineOptions.Clo.ErrorTrace > 0) {

-                    Console.WriteLine("Execution trace:");

-                    foreach (Block b in error.Trace) {

-                      Contract.Assert(b != null);

-                      if (b.tok == null) {

-                        Console.WriteLine("    <intermediate block>");

-                      } else {

-                        // for ErrorTrace == 1 restrict the output;

-                        // do not print tokens with -17:-4 as their location because they have been 

-                        // introduced in the translation and do not give any useful feedback to the user

-                        if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {

-                          Console.WriteLine("    {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);

-                        }

-                      }

+                }

+                if (Bpl.CommandLineOptions.Clo.ErrorTrace > 0) {

+                  foreach (Bpl.Block b in error.Trace) {

+                    // for ErrorTrace == 1 restrict the output;

+                    // do not print tokens with -17:-4 as their location because they have been

+                    // introduced in the translation and do not give any useful feedback to the user

+                    if (!(Bpl.CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4) &&

+                        b.tok.line != 0 && b.tok.col != 0) {

+                      errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label);

                     }

                   }

-                  errorCount++;

                 }

-              Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

+                // if (Bpl.CommandLineOptions.Clo.ModelViewFile != null) {

+                //   error.PrintModel();

+                // }

+                er(errorInfo);

+                errorCount++;

+              }

               break;

           }

-          if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) {

-            Console.Out.Flush();

-          }

         }

       }

       vcgen.Close();

-      cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

+      Bpl.CommandLineOptions.Clo.TheProverFactory.Close();

 

-    #endregion

+      #endregion

 

       return PipelineOutcome.VerificationCompleted;

     }

 

-    static void ReportBplError(Absy node, string message, bool error) {

-      Contract.Requires(node != null); Contract.Requires(message != null);

-      IToken tok = node.tok;

-      string s;

-      if (tok == null) {

-        s = message;

-      } else {

-        s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message);

+    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);

       }

-      if (error) {

-        ErrorWriteLine(s);

-      } else {

-        Console.WriteLine(s);

+      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));

+      }

+      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;

+        }

       }

-    }

 

-    /// <summary>

-    /// Inform the user about something and proceed with translation normally.

-    /// Print newline after the message.

-    /// </summary>

-    public static void Inform(string s) {

-      if (CommandLineOptions.Clo.Trace) {

-        Console.WriteLine(s);

+      public static string CleanUp(string msg) {

+        if (msg.ToLower().StartsWith("error: ")) {

+          return msg.Substring(7);

+        } else {

+          return msg;

+        }

       }

     }

-#endif

   }

 }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index 4e9dbdf8..e978f696 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -72,6 +72,9 @@
     <Reference Include="Provers.Z3">

       <HintPath>..\..\..\..\Binaries\Provers.Z3.dll</HintPath>

     </Reference>

+    <Reference Include="Provers.SMTLib">

+      <HintPath>..\..\..\..\Binaries\Provers.SMTLib.dll</HintPath>

+    </Reference>

     <Reference Include="VCExpr">

       <HintPath>..\..\..\..\Binaries\VCExpr.dll</HintPath>

     </Reference>

@@ -139,15 +142,28 @@
     <Compile Include="Properties\AssemblyInfo.cs" />

   </ItemGroup>

   <ItemGroup>

+    <Content Include="DafnyPrelude.bpl">

+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>

+      <IncludeInVSIX>true</IncludeInVSIX>

+    </Content>

     <None Include="source.extension.vsixmanifest">

       <SubType>Designer</SubType>

     </None>

+    <Content Include="UnivBackPred2.smt2">

+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>

+      <IncludeInVSIX>true</IncludeInVSIX>

+    </Content>

   </ItemGroup>

   <ItemGroup>

     <WCFMetadata Include="Service References\" />

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

   <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />

+  <PropertyGroup>

+    <PostBuildEvent>cd</PostBuildEvent>

+    <PostBuildEvent>

+    </PostBuildEvent>

+  </PropertyGroup>

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

        Other similar extension points exist, see Microsoft.Common.targets.

   <Target Name="BeforeBuild">

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index a4f232dd..c644daec 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -10,30 +10,30 @@ using Microsoft.VisualStudio.Text.Editor;
 using Microsoft.VisualStudio.Text.Formatting;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Text.Classification;

+using Microsoft.VisualStudio.Shell;

 using Microsoft.VisualStudio.Utilities;

 using System.Diagnostics.Contracts;

+using Dafny = Microsoft.Dafny;

+using Bpl = Microsoft.Boogie;

 

 

 namespace DafnyLanguage

 {

+  #region UI stuff

   internal class ProgressMarginGlyphFactory : IGlyphFactory

   {

-    const double m_glyphSize = 16.0;

-

     public UIElement GenerateGlyph(IWpfTextViewLine line, IGlyphTag tag) {

       var dtag = tag as ProgressGlyphTag;

       if (dtag == null) {

         return null;

       }

 

-      System.Windows.Shapes.Ellipse ellipse = new Ellipse();

-      ellipse.Fill = Brushes.LightBlue;

-      ellipse.StrokeThickness = 2;

-      ellipse.Stroke = dtag.V == 0 ? Brushes.DarkBlue : Brushes.BlanchedAlmond;

-      ellipse.Height = m_glyphSize;

-      ellipse.Width = m_glyphSize;

-

-      return ellipse;

+      System.Windows.Shapes.Rectangle sh = new Rectangle() {

+        Fill = dtag.Val == 0 ? Brushes.Goldenrod : Brushes.DarkOrange,

+        Height = 18.0,

+        Width = 3.0

+      };

+      return sh;

     }

   }

 

@@ -51,48 +51,133 @@ namespace DafnyLanguage
 

   internal class ProgressGlyphTag : IGlyphTag

   {

-    public int V;

-    public ProgressGlyphTag(int v) {

-      V = v;

+    public readonly int Val;

+    public ProgressGlyphTag(int val) {

+      Val = val;

+    }

+  }

+  #endregion

+

+  [Export(typeof(ITaggerProvider))]

+  [ContentType("dafny")]

+  [TagType(typeof(ProgressGlyphTag))]

+  class ProgressTaggerProvider : ITaggerProvider

+  {

+    [Import]

+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;

+

+    [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]

+    internal IServiceProvider _serviceProvider = null;

+

+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

+      ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);

+      // create a single tagger for each buffer.

+      Func<ITagger<T>> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator) as ITagger<T>; };

+      return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);

     }

   }

 

   internal class ProgressTagger : ITagger<ProgressGlyphTag>

   {

-    public ProgressTagger(ITextBuffer buffer) {

-      BufferIdleEventUtil.AddBufferIdleEventListener(buffer, ClearMarks);

+    ErrorListProvider _errorProvider;

+    ITextBuffer _buffer;

+

+    public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<DafnyResolverTag> tagAggregator) {

+      _buffer = buffer;

+      _errorProvider = new ErrorListProvider(serviceProvider);

+      BufferIdleEventUtil.AddBufferIdleEventListener(buffer, DoTheVerification);

+      tagAggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);

+      buffer.Changed += new EventHandler<TextContentChangedEventArgs>(buffer_Changed);

+      bufferChangesPostVerificationStart.Add(new SnapshotSpan(buffer.CurrentSnapshot, 0, buffer.CurrentSnapshot.Length));

     }

 

-    ITextVersion latestClearedVersion;

+    public void Dispose() {

+      BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, DoTheVerification);

+    }

 

-    public void ClearMarks(object sender, EventArgs args) {

-      var buffer = sender as ITextBuffer;

+    List<SnapshotSpan> bufferChangesPreVerificationStart = new List<SnapshotSpan>();  // buffer changes after the last completed verification and before the currently running verification

+    List<SnapshotSpan> bufferChangesPostVerificationStart = new List<SnapshotSpan>();  // buffer changes since the start of the currently running verification

+    void buffer_Changed(object sender, TextContentChangedEventArgs e) {

       var chng = TagsChanged;

-      if (buffer != null && chng != null) {

-        var snap = buffer.CurrentSnapshot;

-        latestClearedVersion = snap.Version;

-        chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));

+      if (chng != null) {

+        foreach (var change in e.Changes) {

+          var startLine = e.After.GetLineFromPosition(change.NewPosition);

+          var endLine = e.After.GetLineFromPosition(change.NewEnd);

+          bufferChangesPostVerificationStart.Add(new SnapshotSpan(startLine.Start, endLine.End));

+        }

       }

     }

 

-    IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {

-      if (spans.Count == 0) yield break;

-      if (spans[0].Snapshot.Version != latestClearedVersion) {

-        foreach (SnapshotSpan span in spans) {

-          yield return new TagSpan<ProgressGlyphTag>(new SnapshotSpan(span.Start, span.Length), new ProgressGlyphTag(1));

+    // Keep track of the most recent resolution results

+    ResolverTagger resolver;

+    Dafny.Program latestProgram;

+    ITextSnapshot latestSnapshot;

+    void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {

+      var r = sender as ResolverTagger;

+      if (r != null) {

+        // If r._program is null, then the current buffer contains a Dafny fragment that does not resolve.  If it is non-null,

+        // then r._program has been successfully resolved, so when things have been sufficiently idle, we're ready to verify it.

+        resolver = r;

+        latestProgram = r._program;

+        latestSnapshot = latestProgram != null ? r._snapshot : null;

+      }

+    }

+

+    ITextVersion latestClearedVersion;

+    public void DoTheVerification(object sender, EventArgs args) {

+      var buffer = sender as ITextBuffer;

+      if (buffer != null && latestProgram != null) {

+        bufferChangesPreVerificationStart.AddRange(bufferChangesPostVerificationStart);

+        bufferChangesPostVerificationStart.Clear();

+

+        // do the verification

+        var newErrors = new List<DafnyError>();

+        bool success = DafnyDriver.Verify(latestProgram, (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));

+          }

+        });

+

+        bufferChangesPreVerificationStart.Clear();  // note, depending on concurrency, there may now be more things in the ...Post... list

+        if (resolver != null) {

+          resolver.PopulateErrorList(newErrors, true, latestSnapshot);

+        }

+

+        // What the Error List now reports reflects the latest verification

+        var chng = TagsChanged;

+        if (chng != null) {

+          var snap = latestSnapshot;

+          latestClearedVersion = snap.Version;

+          chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));

         }

       }

     }

+

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

-  }

+    IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {

+      if (spans.Count == 0) yield break;

+      var targetSnapshot = spans[0].Snapshot;

 

-  [Export(typeof(ITaggerProvider))]

-  [ContentType("dafny")]

-  [TagType(typeof(ProgressGlyphTag))]

-  class ProgressTaggerProvider : ITaggerProvider

-  {

-    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

-      return new ProgressTagger(buffer) as ITagger<T>;

+      // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot

+      NormalizedSnapshotSpanCollection chs;

+      chs = new NormalizedSnapshotSpanCollection(Map(bufferChangesPreVerificationStart, span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));

+      foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {

+        yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(0));

+      }

+      chs = new NormalizedSnapshotSpanCollection(Map(bufferChangesPostVerificationStart, span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));

+      foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {

+        yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(1));

+      }

+    }

+

+    /// <summary>

+    /// (Why the firetruck isn't an extension method like this already in the standard library?)

+    /// </summary>

+    public static IEnumerable<TOut> Map<TIn, TOut>(IEnumerable<TIn> coll, System.Func<TIn, TOut> fn) {

+      foreach (var e in coll) {

+        yield return fn(e);

+      }

     }

   }

 }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
index 05a83b12..fcc31a3c 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
@@ -10,6 +10,7 @@ using System.Linq;
 using System.Text;

 using System.ComponentModel.Composition;

 using System.Windows.Threading;

+using Microsoft.VisualStudio;

 using Microsoft.VisualStudio.Shell;

 using Microsoft.VisualStudio.Shell.Interop;

 using Microsoft.VisualStudio.Text;

@@ -17,6 +18,7 @@ using Microsoft.VisualStudio.Text.Classification;
 using Microsoft.VisualStudio.Text.Editor;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Text.Projection;

+using Microsoft.VisualStudio.TextManager.Interop;

 using Microsoft.VisualStudio.Utilities;

 using System.Diagnostics.Contracts;

 using Dafny = Microsoft.Dafny;

@@ -69,7 +71,8 @@ namespace DafnyLanguage
     ITextBuffer _buffer;

     ITextDocument _document;

     public ITextSnapshot _snapshot;  // may be null

-    List<DafnyError> _errors = new List<DafnyError>();  // if nonempty, then _snapshot is the snapshot from which the errors were produced

+    List<DafnyError> _resolutionErrors = new List<DafnyError>();  // if nonempty, then _snapshot is the snapshot from which the errors were produced

+    List<DafnyError> _verificationErrors = new List<DafnyError>();

     ErrorListProvider _errorProvider;

     public Dafny.Program _program;  // non-null only if the snapshot contains a Dafny program that type checks

 

@@ -95,33 +98,42 @@ namespace DafnyLanguage
       BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ProcessFile);

     }

 

+    public IEnumerable<DafnyError> AllErrors() {

+      foreach (var err in _resolutionErrors) {

+        yield return err;

+      }

+      foreach (var err in _verificationErrors) {

+        yield return err;

+      }

+    }

+

     /// <summary>

     /// Find the Error tokens in the set of all tokens and create an ErrorTag for each

     /// </summary>

     public IEnumerable<ITagSpan<DafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

       if (spans.Count == 0) yield break;

-      foreach (var err in _errors) {

+      foreach (var err in AllErrors()) {

         if (err.Category != ErrorCategory.ProcessError) {

+          Contract.Assert(0 <= err.Line);

           var line = _snapshot.GetLineFromLineNumber(err.Line);

           Contract.Assert(err.Column <= line.Length);

           var length = line.Length - err.Column;

           if (5 < length) length = 5;

           var span = new SnapshotSpan(new SnapshotPoint(_snapshot, line.Start.Position + err.Column), length);

-          // http://msdn.microsoft.com/en-us/library/dd885244.aspx says one can use the error types below, but they

-          // all show as purple squiggles for me.  And just "error" (which is not mentioned on that page) shows up

-          // as red.

-          string ty;

+          string ty;  // the COLORs below indicate what I see on my machine

           switch (err.Category) {

             default:  // unexpected category

             case ErrorCategory.ParseError:

-              // ty = "syntax error";

-              ty = "error"; break;

+            case ErrorCategory.ParseWarning:

+              ty = "syntax error"; break;  // COLOR: red

             case ErrorCategory.ResolveError:

-              ty = "compiler error"; break;

+              ty = "compiler error"; break;  // COLOR: blue

             case ErrorCategory.VerificationError:

-              ty = "other error"; break;

-            case ErrorCategory.ParseWarning:

-              ty = "warning"; break;

+              ty = "error"; break;  // COLOR: red

+            case ErrorCategory.AuxInformation:

+              ty = "other error"; break;  // COLOR: purple red

+            case ErrorCategory.InternalError:

+              ty = "error"; break;  // COLOR: red

           }

           yield return new TagSpan<DafnyResolverTag>(span, new DafnyErrorResolverTag(ty, err.Message));

         }

@@ -143,66 +155,149 @@ namespace DafnyLanguage
       NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length));

 

       var driver = new DafnyDriver(_buffer.CurrentSnapshot.GetText(), _document != null ? _document.FilePath : "<program>");

-      Dafny.Program program = driver.Process();

-      var newErrors = driver.Errors;

+      List<DafnyError> newErrors;

+      Dafny.Program program;

+      try {

+        program = driver.Process();

+        newErrors = driver.Errors;

+      } catch (Exception e) {

+        newErrors = new List<DafnyError>();

+        newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message));

+        program = null;

+      }

 

-      _errorProvider.Tasks.Clear();

+      _snapshot = snapshot;

+      _program = program;

+      PopulateErrorList(newErrors, false, snapshot);

+    }

+

+    public void PopulateErrorList(List<DafnyError> newErrors, bool verificationErrors, ITextSnapshot snapshot) {

+      Contract.Requires(newErrors != null);

       foreach (var err in newErrors) {

-        ErrorTask task = new ErrorTask();

-        task.CanDelete = true;

-        task.Category = TaskCategory.BuildCompile;

-        if (_document != null)

+        err.FillInSnapshot(snapshot);

+      }

+      if (verificationErrors) {

+        _verificationErrors = newErrors;

+      } else {

+        _resolutionErrors = newErrors;

+      }

+

+      _errorProvider.SuspendRefresh();  // reduce flickering

+      _errorProvider.Tasks.Clear();

+      foreach (var err in AllErrors()) {

+        ErrorTask task = new ErrorTask() {

+          // CanDelete = true,

+          Category = TaskCategory.BuildCompile,

+          ErrorCategory = CategoryConversion(err.Category),

+          Text = err.Message,

+          Line = err.Line,

+          Column = err.Column

+        };

+        if (_document != null) {

           task.Document = _document.FilePath;

-        task.ErrorCategory = TaskErrorCategory.Error;

-        task.Text = err.Message;

-        if (err.Category != ErrorCategory.ProcessError) {

-          task.Line = err.Line;

-          task.Column = err.Column;

-          task.Navigate += new EventHandler(task_Navigate);

+        }

+        if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError) {

+          task.Navigate += new EventHandler(NavigateHandler);

         }

         _errorProvider.Tasks.Add(task);

       }

-

-      _errors = newErrors;

-      _snapshot = snapshot;

-      _program = program;

+      _errorProvider.ResumeRefresh();

       var chng = TagsChanged;

       if (chng != null)

         chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

     }

 

-    /// <summary>

-    /// Callback method attached to each of our tasks in the Error List

-    /// </summary>

-    void task_Navigate(object sender, EventArgs e) {

-      ErrorTask error = sender as ErrorTask;

-      if (error != null) {

-        error.Line += 1;

-        error.Column += 1;

-        // TODO: how to move the cursor to the right column?

-        _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));

-        error.Column -= 1;

-        error.Line -= 1;

+    TaskErrorCategory CategoryConversion(ErrorCategory cat) {

+      switch (cat) {

+        case ErrorCategory.ParseError:

+        case ErrorCategory.ResolveError:

+        case ErrorCategory.VerificationError:

+        case ErrorCategory.InternalError:

+          return TaskErrorCategory.Error;

+        case ErrorCategory.ParseWarning:

+          return TaskErrorCategory.Warning;

+        case ErrorCategory.AuxInformation:

+          return TaskErrorCategory.Message;

+        default:

+          Contract.Assert(false);  // unexpected category

+          return TaskErrorCategory.Error;  // please compiler

       }

     }

+

+    void NavigateHandler(object sender, EventArgs arguments) {

+      var task = sender as ErrorTask;

+      if (task == null || task.Document == null)

+        return;

+

+      // This would have been the simple way of doing things:

+      //     _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));

+      // Unfortunately, it doesn't work--it seems to ignore the column position.  (Moreover, it wants 1-based

+      // line/column numbers, whereas the Error Task pane wants 0-based line/column numbers.)

+      // So, instead we do all the things that follow:

+

+      var openDoc = Package.GetGlobalService(typeof(IVsUIShellOpenDocument)) as IVsUIShellOpenDocument;

+      if (openDoc == null)

+        return;

+

+      IVsWindowFrame frame;

+      Microsoft.VisualStudio.OLE.Interop.IServiceProvider sp;

+      IVsUIHierarchy hier;

+      uint itemid;

+      Guid logicalView = VSConstants.LOGVIEWID_Code;

+      if (Microsoft.VisualStudio.ErrorHandler.Failed(openDoc.OpenDocumentViaProject(task.Document, ref logicalView, out sp, out hier, out itemid, out frame)) || frame == null)

+        return;

+

+      object docData;

+      Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(frame.GetProperty((int)__VSFPROPID.VSFPROPID_DocData, out docData));

+

+      // Get the VsTextBuffer

+      VsTextBuffer buffer = docData as VsTextBuffer;

+      if (buffer == null) {

+        IVsTextBufferProvider bufferProvider = docData as IVsTextBufferProvider;

+        if (bufferProvider != null) {

+          IVsTextLines lines;

+          Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(bufferProvider.GetTextBuffer(out lines));

+          buffer = lines as VsTextBuffer;

+          if (buffer == null)

+            return;

+        }

+      }

+

+      VsTextManager textManager = Package.GetGlobalService(typeof(VsTextManagerClass)) as VsTextManager;

+      if (textManager == null)

+        return;

+

+      // Finally, move the cursor

+      Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(textManager.NavigateToLineAndColumn(buffer, ref logicalView, task.Line, task.Column, task.Line, task.Column));

+    }

+

   }

 

   public enum ErrorCategory

   {

-    ProcessError, ParseWarning, ParseError, ResolveError, VerificationError

+    ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError

   }

 

   internal class DafnyError

   {

     public readonly int Line;  // 0 based

     public readonly int Column;  // 0 based

+    public ITextSnapshot Snapshot;  // filled in during the FillInSnapshot call

     public readonly ErrorCategory Category;

     public readonly string Message;

+    /// <summary>

+    /// "line" and "col" are expected to be 0-based

+    /// </summary>

     public DafnyError(int line, int col, ErrorCategory cat, string msg) {

       Line = line;

       Column = col;

       Category = cat;

       Message = msg;

     }

+

+    public void FillInSnapshot(ITextSnapshot snapshot) {

+      Contract.Requires(snapshot != null);

+      Snapshot = snapshot;

+    }

   }

 }