diff options
| author |  leino <unknown> | 2015-09-29 19:46:29 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-29 19:46:29 -0700 |
| commit | c8c9531139972c0bb0ade064a357e007e0faa4c0 (patch) | |
| tree | 025186bd17a7841014f15c304242e2c51959184f | |
| parent | b77e1539b2290f8661a86cf461493ce76d60254c (diff) | |
| parent | 13dcb53b7dde21f887d87c47608f81082e7efbb3 (diff) | |
Merge
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 6 | ||||
| -rw-r--r-- | Source/DafnyServer/DafnyServer.csproj | 13 | ||||
| -rw-r--r-- | Test/server/minimal.transcript | 2 | ||||
| -rw-r--r-- | Test/server/simple-session.transcript | 2 |
4 files changed, 13 insertions, 10 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index c45d66fc..8282edc7 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -226,8 +226,8 @@ namespace Microsoft.Dafny stats = new PipelineStatistics();
LinearTypeChecker ltc;
- MoverTypeChecker mtc;
- PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc, out mtc);
+ CivlTypeChecker ctc;
+ PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc, out ctc);
switch (oc) {
case PipelineOutcome.Done:
return oc;
@@ -244,7 +244,7 @@ namespace Microsoft.Dafny fileNames.Add(bplFileName);
Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true);
if (reparsedProgram != null) {
- ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc, out mtc);
+ ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc, out ctc);
}
}
return oc;
diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 1a256f5f..af262fc3 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
<PropertyGroup>
@@ -84,9 +84,6 @@ <Reference Include="System.Runtime.Serialization" />
<Reference Include="System.Xml.Linq" />
<Reference Include="Microsoft.CSharp" />
- <Reference Include="DafnyPipeline">
- <HintPath>..\..\Binaries\DafnyPipeline.dll</HintPath>
- </Reference>
<Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
@@ -99,6 +96,12 @@ <ItemGroup>
<None Include="App.config" />
</ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Dafny\DafnyPipeline.csproj">
+ <Project>{fe44674a-1633-4917-99f4-57635e6fa740}</Project>
+ <Name>DafnyPipeline</Name>
+ </ProjectReference>
+ </ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
@@ -107,4 +110,4 @@ <Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project>
\ No newline at end of file diff --git a/Test/server/minimal.transcript b/Test/server/minimal.transcript index 9625fb00..394fd921 100644 --- a/Test/server/minimal.transcript +++ b/Test/server/minimal.transcript @@ -1,4 +1,4 @@ -# RUN: %server "%s" > "%t"
+# RUN: "%server" "%s" > "%t"
# RUN: %diff "%s.expect" "%t"
verify
eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
diff --git a/Test/server/simple-session.transcript b/Test/server/simple-session.transcript index 26539267..d095f6dd 100644 --- a/Test/server/simple-session.transcript +++ b/Test/server/simple-session.transcript @@ -1,4 +1,4 @@ -# RUN: %server "%s" > "%t"
+# RUN: "%server" "%s" > "%t"
# RUN: %diff "%s.expect" "%t"
verify
eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
|