summaryrefslogtreecommitdiff
path: root/Source/DafnyDriver
diff options
context:
space:
mode:
Diffstat (limited to 'Source/DafnyDriver')
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs7
1 files changed, 4 insertions, 3 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 43aa6971..81662b5d 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -163,7 +163,8 @@ namespace Microsoft.Dafny
Contract.Ensures(0 <= Contract.ValueAtReturn(out stats).InconclusiveCount && 0 <= Contract.ValueAtReturn(out stats).TimeoutCount);
stats = new PipelineStatistics();
- PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName);
+ LinearTypechecker ltc;
+ PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc);
switch (oc) {
case PipelineOutcome.Done:
return oc;
@@ -180,7 +181,7 @@ namespace Microsoft.Dafny
fileNames.Add(bplFileName);
Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true);
if (reparsedProgram != null) {
- ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName);
+ ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc);
}
}
return oc;
@@ -190,7 +191,7 @@ namespace Microsoft.Dafny
return ExecutionEngine.InferAndVerify(program, stats);
default:
- Contract.Assert(false);throw new cce.UnreachableException(); // unexpected outcome
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome
}
}