From bcb834b4d3fb4926d7eabe0a9837396c84619ee6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 10 Aug 2012 11:30:30 -0700
Subject: DafnyExtension:  hide execution-trace output, show split-expr related
 error locations, set a 10-second timeout

---
 Source/Dafny/Translator.cs                              |  8 +++-----
 .../VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 17 ++++++++++++++---
 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) {
-- 
cgit v1.2.3