DafnyExtension: hide execution-trace output, show split-expr related error locations, set a 10-second timeout

2 files changed, 17 insertions, 8 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2e322029..b476e7b4 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4804,12 +4804,10 @@ namespace Microsoft.Dafny {
     }

 

     static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)

-     {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-

-

       Contract.Requires(e0.Type is IntType && e1.Type is IntType);

       Contract.Ensures(Contract.Result<Expression>() != null);

       BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);

@@ -4819,7 +4817,7 @@ namespace Microsoft.Dafny {
     }

 

     static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)

-     {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(test != null);

       Contract.Requires(e0 != null);

@@ -4833,7 +4831,7 @@ namespace Microsoft.Dafny {
     }

 

     public IEnumerable<Expression> Conjuncts(Expression expr)

-     {

+    {

       Contract.Requires(expr != null);

       Contract.Requires(expr.Type is BoolType);

       Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 3298be4b..b7b2cd6d 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -39,9 +39,11 @@ 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();

+        var options = new Dafny.DafnyOptions();

+        options.ProverKillTime = 10;

+        options.ErrorTrace = 0;

+        options.ApplyDefaultOptions();

+        Dafny.DafnyOptions.Install(options);

       }

     }

 

@@ -388,12 +390,21 @@ namespace DafnyLanguage
         Contract.Requires(msg != null);

         Tok = tok;

         Msg = CleanUp(msg);

+        AddNestingsAsAux(tok);

       }

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

+        AddNestingsAsAux(tok);

+      }

+      void AddNestingsAsAux(Bpl.IToken tok) {

+        while (tok is Dafny.NestedToken) {

+          var nt = (Dafny.NestedToken)tok;

+          tok = nt.Inner;

+          Aux.Add(new DafnyErrorAuxInfo(tok, "Related location"));

+        }

       }

       public void AddAuxInfo(Bpl.QKeyValue attr) {

         while (attr != null) {