summaryrefslogtreecommitdiff
path: root/Util/VS2010
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-08-10 11:30:30 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-08-10 11:30:30 -0700
commitbcb834b4d3fb4926d7eabe0a9837396c84619ee6 (patch)
treefbbf8857f0db2f388fe774917bdc90450383410b /Util/VS2010
parent33137f76bac9c2c0e3b26237bcd0e37c092e0c98 (diff)
DafnyExtension: hide execution-trace output, show split-expr related error locations, set a 10-second timeout
Diffstat (limited to 'Util/VS2010')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs17
1 files changed, 14 insertions, 3 deletions
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) {