diff options
| -rw-r--r-- | Binaries/PrepareDafnyZip.bat | 1 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 5 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.csproj | 3 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 5 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyExtension.csproj | 6 |
5 files changed, 9 insertions, 11 deletions
diff --git a/Binaries/PrepareDafnyZip.bat b/Binaries/PrepareDafnyZip.bat index 29330621..e2521112 100644 --- a/Binaries/PrepareDafnyZip.bat +++ b/Binaries/PrepareDafnyZip.bat @@ -22,7 +22,6 @@ for %%f in ( Model.dll Model.pdb ParserHelper.dll ParserHelper.pdb Provers.SMTLib.dll Provers.SMTLib.pdb - UnivBackPred2.smt2 VCExpr.dll VCExpr.pdb VCGeneration.dll VCGeneration.pdb DafnyLanguageService.vsix diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a2b5aa0b..b5414ba3 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -187,7 +187,10 @@ namespace Microsoft.Dafny return oc;
case PipelineOutcome.ResolvedAndTypeChecked:
- ExecutionEngine.EliminateDeadVariablesAndInline(program);
+ ExecutionEngine.EliminateDeadVariables(program);
+ ExecutionEngine.CollectModSets(program);
+ ExecutionEngine.CoalesceBlocks(program);
+ ExecutionEngine.Inline(program);
return ExecutionEngine.InferAndVerify(program, stats);
default:
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 912fd38e..631b0194 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -178,9 +178,6 @@ <None Include="app.config" />
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <PropertyGroup>
- <PreBuildEvent>copy /y "$(SolutionDir)"..\..\boogie\Binaries\UnivBackPred2.smt2 "$(TargetDir)"</PreBuildEvent>
- </PropertyGroup>
<!-- 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.
<Target Name="BeforeBuild">
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 168e69b5..c92caf4e 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -251,7 +251,10 @@ namespace DafnyLanguage PipelineOutcome oc = BoogieResolveAndTypecheck(program);
if (oc == PipelineOutcome.ResolvedAndTypeChecked) {
- ExecutionEngine.EliminateDeadVariablesAndInline(program);
+ ExecutionEngine.EliminateDeadVariables(program);
+ ExecutionEngine.CollectModSets(program);
+ ExecutionEngine.CoalesceBlocks(program);
+ ExecutionEngine.Inline(program);
return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId);
}
return oc;
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj index 47a3516c..d29da5d2 100644 --- a/Source/DafnyExtension/DafnyExtension.csproj +++ b/Source/DafnyExtension/DafnyExtension.csproj @@ -163,9 +163,6 @@ <Content Include="DafnyPrelude.bpl">
<IncludeInVSIX>true</IncludeInVSIX>
</Content>
- <Content Include="UnivBackPred2.smt2">
- <IncludeInVSIX>true</IncludeInVSIX>
- </Content>
<Content Include="DafnyRuntime.cs">
<IncludeInVSIX>true</IncludeInVSIX>
</Content>
@@ -189,8 +186,7 @@ <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
<Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />
<PropertyGroup>
- <PreBuildEvent>copy /y "..\..\boogie\Binaries\UnivBackPred2.smt2" "$(ProjectDir)"
-copy /y "..\Binaries\DafnyPrelude.bpl" "$(ProjectDir)"
+ <PreBuildEvent>copy /y "..\Binaries\DafnyPrelude.bpl" "$(ProjectDir)"
copy /y "..\Binaries\DafnyRuntime.cs" "$(ProjectDir)"</PreBuildEvent>
</PropertyGroup>
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
|