45 lines
1.9 KiB
XML
45 lines
1.9 KiB
XML
|
<!--
|
||
|
|
##############################################################################
|
||
|
|
|
||
|
|
Microsoft Research Singularity
|
||
|
|
|
||
|
|
Copyright (c) Microsoft Corporation. All rights reserved.
|
||
|
|
|
||
|
|
Note:
|
||
|
|
|
||
|
|
##############################################################################
|
||
|
|
-->
|
||
|
|
<Project xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||
|
|
|
||
|
|
<Import Project="..\..\..\Paths.targets"/>
|
||
|
|
|
||
|
|
<PropertyGroup>
|
||
|
|
<AssemblyName>SpecTest</AssemblyName>
|
||
|
|
<OutputType>Exe</OutputType>
|
||
|
|
<BoogieSucceeded>"Spec#\ Program\ Verifier\ finished\ with\ [0-9]*\ verified,\ 0\ errors"</BoogieSucceeded>
|
||
|
|
</PropertyGroup>
|
||
|
|
|
||
|
|
<ItemGroup>
|
||
|
|
<Compile Include="SpecTest.sg"/>
|
||
|
|
</ItemGroup>
|
||
|
|
|
||
|
|
<Import Project="$(SINGULARITY_ROOT)\Targets\ConsoleCategory.targets"/>
|
||
|
|
|
||
|
|
<!--
|
||
|
|
For now, we invoke boogie explicitly here.
|
||
|
|
In the future, if many projects use boogie, we could change the .target
|
||
|
|
files so that boogie is invoked implicitly, conditional on some property.
|
||
|
|
Alternately, we could use the "/verify" flag to sgc.
|
||
|
|
-->
|
||
|
|
<Target Name="AfterBuild" DependsOnTargets="Boogie">
|
||
|
|
</Target>
|
||
|
|
|
||
|
|
<Target Name="Boogie" Inputs="$(OutputPath)\$(AssemblyName)$(AssemblyExt)" Outputs="$(OutputPath)\$(AssemblyName).boogiesuccess">
|
||
|
|
<Exec Command="boogie /platform:"$(CompilerPlatformVersion),$(CompilerPlatformDir)" /stdlib:"$(Stdlib)" "$(OutputPath)\$(AssemblyName)$(AssemblyExt)" > "$(OutputPath)\$(AssemblyName).boogieout""/>
|
||
|
|
<Exec Command="type "$(OutputPath)\$(AssemblyName).boogieout""/>
|
||
|
|
<Exec Command="findstr $(BoogieSucceeded) "$(OutputPath)\$(AssemblyName).boogieout" > "$(OutputPath)\$(AssemblyName).boogiefindstr""/>
|
||
|
|
<Copy SourceFiles="$(OutputPath)\$(AssemblyName).boogiefindstr" DestinationFiles="$(OutputPath)\$(AssemblyName).boogiesuccess"/>
|
||
|
|
</Target>
|
||
|
|
|
||
|
|
</Project>
|