Skip to content

Commit

Permalink
Mostly build with .NET 8.0
Browse files Browse the repository at this point in the history 
A few small pieces of code are commented out until we can get them to
build correctly.
  • Loading branch information
@atomb
atomb committed May 20, 2024
1 parent 20e05ce commit 362713b
Show file tree
Hide file tree
Showing 27 changed files with 206 additions and 806 deletions.
132 changes: 16 additions & 116 deletions Sources/BoogieWrapper/BoogieWrapper.csproj
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,8 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="12.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<TargetFramework>net8.0</TargetFramework>
<Platform Condition=" '$(Platform)' == '' ">x86</Platform>
<ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{1E16DB2A-17E4-4E2B-BDE0-C6994B236152}</ProjectGuid>
<OutputType>Exe</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>BoogieWrapper</RootNamespace>
<AssemblyName>BoogieWrapper</AssemblyName>
<TargetFrameworkVersion>v4.6.1</TargetFrameworkVersion>
<TargetFrameworkProfile>
</TargetFrameworkProfile>
<FileAlignment>512</FileAlignment>
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
Expand All @@ -29,30 +18,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
<PlatformTarget>x86</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>bin\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<Prefer32Bit>false</Prefer32Bit>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<PlatformTarget>x86</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin\Release\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<Prefer32Bit>false</Prefer32Bit>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>false</SignAssembly>
<GenerateAssemblyInfo>false</GenerateAssemblyInfo>
</PropertyGroup>
<PropertyGroup>
<AssemblyOriginatorKeyFile>
Expand All @@ -62,96 +28,30 @@
<DelaySign>false</DelaySign>
</PropertyGroup>
<ItemGroup>
<Reference Include="AbsInt">
<HintPath>..\references\AbsInt.dll</HintPath>
</Reference>
<Reference Include="Basetypes">
<HintPath>..\references\Basetypes.dll</HintPath>
</Reference>
<Reference Include="CodeContractsExtender">
<HintPath>..\references\CodeContractsExtender.dll</HintPath>
</Reference>
<Reference Include="Core">
<HintPath>..\references\Core.dll</HintPath>
</Reference>
<Reference Include="Model">
<HintPath>..\references\Model.dll</HintPath>
</Reference>
<Reference Include="ParserHelper">
<HintPath>..\references\ParserHelper.dll</HintPath>
</Reference>
<Reference Include="Provers.SMTLib">
<HintPath>..\references\Provers.SMTLib.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core" />
<Reference Include="System.Xml.Linq" />
<Reference Include="System.Data.DataSetExtensions" />
<Reference Include="System.Data" />
<Reference Include="System.Xml" />
<Reference Include="VCExpr">
<HintPath>..\references\VCExpr.dll</HintPath>
</Reference>
<Reference Include="VCGeneration">
<HintPath>..\references\VCGeneration.dll</HintPath>
</Reference>
<PackageReference Include="Boogie.AbsInt" Version="2.7.39" />
<PackageReference Include="Boogie.BaseTypes" Version="2.7.39" />
<PackageReference Include="Boogie.CodeContractsExtender" Version="2.7.39" />
<PackageReference Include="Boogie.Core" Version="2.7.39" />
<PackageReference Include="Boogie.Model" Version="2.7.39" />
<PackageReference Include="Boogie.Provers.SMTLib" Version="2.7.39" />
<PackageReference Include="Boogie.VCExpr" Version="2.7.39" />
<PackageReference Include="Boogie.VCGeneration" Version="2.7.39" />
</ItemGroup>
<ItemGroup>
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="Properties\Resources.Designer.cs">
<Compile Update="Properties\Resources.Designer.cs">
<AutoGen>True</AutoGen>
<DesignTime>True</DesignTime>
<DependentUpon>Resources.resx</DependentUpon>
</Compile>
<Compile Include="source\Wrapper.cs" />
</ItemGroup>
<ItemGroup>
<BootstrapperPackage Include=".NETFramework,Version=v4.0,Profile=Client">
<Visible>False</Visible>
<ProductName>Microsoft .NET Framework 4 Client Profile %28x86 and x64%29</ProductName>
<Install>true</Install>
</BootstrapperPackage>
<BootstrapperPackage Include="Microsoft.Net.Client.3.5">
<Visible>False</Visible>
<ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
<Install>false</Install>
</BootstrapperPackage>
<BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
<Visible>False</Visible>
<ProductName>.NET Framework 3.5 SP1</ProductName>
<Install>false</Install>
</BootstrapperPackage>
<BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
<Visible>False</Visible>
<ProductName>Windows Installer 3.1</ProductName>
<Install>true</Install>
</BootstrapperPackage>
</ItemGroup>
<ItemGroup>
<EmbeddedResource Include="Properties\Resources.resx">
<EmbeddedResource Update="Properties\Resources.resx">
<Generator>ResXFileCodeGenerator</Generator>
<LastGenOutput>Resources.Designer.cs</LastGenOutput>
</EmbeddedResource>
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\SymDiffUtils\SymDiffUtils.csproj">
<Project>{699f0912-d902-4854-9e1e-9892b46bcdbd}</Project>
<Name>SymDiffUtils</Name>
</ProjectReference>
<ProjectReference Include="..\SymDiff\SymDiff.csproj">
<Project>{4a428490-cd6f-4fbf-aa15-5f579be6c4b9}</Project>
<Name>SymDiff</Name>
</ProjectReference>
</ItemGroup>
<ItemGroup>
<None Include="app.config" />
<ProjectReference Include="..\SymDiffUtils\SymDiffUtils.csproj" />
<ProjectReference Include="..\SymDiff\SymDiff.csproj" />
</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.
<Target Name="BeforeBuild">
</Target>
<Target Name="AfterBuild">
</Target>
-->
</Project>
</Project>
2 changes: 1 addition & 1 deletion Sources/BoogieWrapper/source/Wrapper.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Basetypes; //For BigNum
using Microsoft.BaseTypes; //For BigNum
using SDiff.Boogie;
using System.IO;
using System.Text.RegularExpressions;
Expand Down
102 changes: 16 additions & 86 deletions Sources/Dependency/Dependency.csproj
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,7 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="12.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')" />
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<ProjectGuid>{A699DBCF-BDC2-4EB1-B53E-0CEC2C0C8CDB}</ProjectGuid>
<TargetFramework>net8.0</TargetFramework>
<OutputType>Exe</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Dependency</RootNamespace>
<AssemblyName>Dependency</AssemblyName>
<TargetFrameworkVersion>v4.6.1</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
Expand All @@ -26,71 +17,11 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
<TargetFrameworkProfile />
<GenerateAssemblyInfo>false</GenerateAssemblyInfo>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<PlatformTarget>x64</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>bin\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<PlatformTarget>AnyCPU</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin\Release\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
</PropertyGroup>
<ItemGroup>
<Reference Include="Basetypes">
<HintPath>..\references\Basetypes.dll</HintPath>
</Reference>
<Reference Include="Core">
<HintPath>..\references\Core.dll</HintPath>
</Reference>
<Reference Include="Graph">
<HintPath>..\references\Graph.dll</HintPath>
</Reference>
<Reference Include="ParserHelper">
<HintPath>..\references\ParserHelper.dll</HintPath>
</Reference>
<Reference Include="Provers.SMTLib">
<HintPath>..\references\Provers.SMTLib.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core" />
<Reference Include="Microsoft.CSharp" />
<Reference Include="System.Data" />
<Reference Include="VCExpr">
<HintPath>..\references\VCExpr.dll</HintPath>
</Reference>
<Reference Include="VCGeneration">
<HintPath>..\references\VCGeneration.dll</HintPath>
</Reference>
</ItemGroup>
<ItemGroup>
<Compile Include="source\AbstractedTaint.cs" />
<Compile Include="source\AbstractState.cs" />
<Compile Include="source\Analysis.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="source\CallGraphBasedPruning.cs" />
<Compile Include="source\DacBasedSimplification.cs" />
<Compile Include="source\DependencyVisitor.cs" />
<Compile Include="source\Inliner.cs" />
<Compile Include="source\ProcessStubs.cs" />
<Compile Include="source\ReadSetVisitor.cs" />
<Compile Include="source\RefineDependency.cs" />
<Compile Include="source\RefineStmtTaint.cs" />
<Compile Include="source\SplitHeap.cs" />
<Compile Include="source\Utils.cs" />
<Compile Include="source\Worklist.cs" />
</ItemGroup>
<ItemGroup>
<BootstrapperPackage Include=".NETFramework,Version=v4.5">
<Visible>False</Visible>
Expand All @@ -109,20 +40,19 @@
</BootstrapperPackage>
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\SymDiffUtils\SymDiffUtils.csproj">
<Project>{699f0912-d902-4854-9e1e-9892b46bcdbd}</Project>
<Name>SymDiffUtils</Name>
</ProjectReference>
<ProjectReference Include="..\SymDiffUtils\SymDiffUtils.csproj" />
</ItemGroup>
<ItemGroup>
<PackageReference Include="Microsoft.CSharp" Version="4.7.0" />
<PackageReference Include="Boogie.Core" Version="2.7.39" />
<PackageReference Include="Boogie.Houdini" Version="2.7.39" />
<PackageReference Include="Boogie.Graph" Version="2.7.39" />
<PackageReference Include="Boogie.Model" Version="2.7.39" />
<PackageReference Include="Boogie.Provers.SMTLib" Version="2.7.39" />
<PackageReference Include="Boogie.VCExpr" Version="2.7.39" />
<PackageReference Include="Boogie.VCGeneration" Version="2.7.39" />
</ItemGroup>
<ItemGroup>
<None Include="app.config" />
<Compile Remove="source\TaintVisitor.cs" />
</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.
<Target Name="BeforeBuild">
</Target>
<Target Name="AfterBuild">
</Target>
-->
</Project>
</Project>
2 changes: 1 addition & 1 deletion Sources/Dependency/source/RefineDependency.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
using System.Diagnostics;
using Microsoft.Boogie.VCExprAST;
using VC;
using Microsoft.Basetypes;
using Microsoft.BaseTypes;
using BType = Microsoft.Boogie.Type;
using SymDiffUtils;

Expand Down
2 changes: 1 addition & 1 deletion Sources/Dependency/source/RefineStmtTaint.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
using System.Diagnostics;
using Microsoft.Boogie.VCExprAST;
using VC;
using Microsoft.Basetypes;
using Microsoft.BaseTypes;
using BType = Microsoft.Boogie.Type;

namespace Dependency
Expand Down
18 changes: 10 additions & 8 deletions Sources/Dependency/source/Utils.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
using System.Diagnostics;
using Microsoft.Boogie.VCExprAST;
using VC;
using Microsoft.Basetypes;
using Microsoft.BaseTypes;
using BType = Microsoft.Boogie.Type;
using Dependency;

Expand Down Expand Up @@ -1014,8 +1014,8 @@ static class VC
public static void InitializeVCGen(Program prog)
{
//create VC.vcgen/VC.proverInterface
VC.vcgen = new VCGen(prog, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, null);
VC.proverInterface = ProverInterface.CreateProver(prog, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
VC.vcgen = new VCGen(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, null);
VC.proverInterface = ProverInterface.CreateProver(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit);
VC.translator = VC.proverInterface.Context.BoogieExprTranslator;
VC.exprGen = VC.proverInterface.Context.ExprGen;
VC.collector = new ConditionGeneration.CounterexampleCollector();
Expand Down Expand Up @@ -1054,18 +1054,19 @@ public static VCExpr GenerateVC(Program prog, Implementation impl)

var exprGen = VC.proverInterface.Context.ExprGen;
//VCExpr controlFlowVariableExpr = null;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : VC.exprGen.Integer(BigNum.ZERO);
VCExpr controlFlowVariableExpr = /*CommandLineOptions.Clo.UseLabels ? null :*/ VC.exprGen.Integer(BigNum.ZERO);


Dictionary<int, Absy> label2absy;
var vc = VC.vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, VC.proverInterface.Context);
if (!CommandLineOptions.Clo.UseLabels)
{
//if (!CommandLineOptions.Clo.UseLabels)
//{
VCExpr controlFlowFunctionAppl = VC.exprGen.ControlFlowFunctionApplication(VC.exprGen.Integer(BigNum.ZERO), VC.exprGen.Integer(BigNum.ZERO));
VCExpr eqExpr = VC.exprGen.Eq(controlFlowFunctionAppl, VC.exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
vc = VC.exprGen.Implies(eqExpr, vc);
}
//}

/*
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
{
VC.handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, VC.vcgen.incarnationOriginMap, VC.collector, mvInfo, VC.proverInterface.Context, prog);
Expand All @@ -1074,10 +1075,11 @@ public static VCExpr GenerateVC(Program prog, Implementation impl)
{
VC.handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, VC.vcgen.incarnationOriginMap, VC.collector, mvInfo, VC.proverInterface.Context, prog);
}
*/
return vc;
}
#endregion

}

}
}
Loading

0 comments on commit 362713b

Please sign in to comment.