DafnyExtension: Enabled model extraction for verification failures.

3 files changed, 7 insertions, 2 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 479816a6..ade7c332 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -36,6 +36,7 @@ namespace DafnyLanguage
         options.ProverKillTime = 10;

         options.ErrorTrace = 0;

         options.VcsCores = System.Environment.ProcessorCount;

+        options.ModelViewFile = "-";

         Dafny.DafnyOptions.Install(options);

         options.ApplyDefaultOptions();

 

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index c2db66c0..6ee12d95 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -324,7 +324,7 @@ namespace DafnyLanguage
           if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))

           {

             var s = RequestIdToSnapshot[errorInfo.RequestId];

-            errorListHolder.AddError(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s), errorInfo.ImplementationName, requestId);

+            errorListHolder.AddError(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, errorInfo.Model.ToString()), errorInfo.ImplementationName, requestId);

             foreach (var aux in errorInfo.Aux)

             {

               errorListHolder.AddError(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s), errorInfo.ImplementationName, requestId);

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 578b9ce2..4f5f70fb 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -10,6 +10,7 @@ using System.Collections.Concurrent;
 using System.Collections.Generic;

 using System.ComponentModel.Composition;

 using System.Diagnostics.Contracts;

+using System.IO;

 using System.Linq;

 using EnvDTE;

 using Microsoft.VisualStudio;

@@ -431,10 +432,12 @@ namespace DafnyLanguage
     public readonly ErrorCategory Category;

     public readonly string Message;

     public readonly ITrackingSpan Span;

+    public readonly string Model;

+

     /// <summary>

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

     /// </summary>

-    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot)

+    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot, string model = null)

     {

       Line = Math.Max(0, line);

       Column = Math.Max(0, col);

@@ -444,6 +447,7 @@ namespace DafnyLanguage
       Contract.Assert(Column <= sLine.Length);

       var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));

       Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

+      Model = model;

     }

   }