From bcb834b4d3fb4926d7eabe0a9837396c84619ee6 Mon Sep 17 00:00:00 2001 From: Rustan Leino 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 --- .../VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'Util') 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