Merge remote-tracking branch 'origin/master' into issue-1996

dafny-lang · Sep 16, 2022 · f3427f6 · f3427f6
2 parents 33ee242 + 62a6d58
commit f3427f6
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 13 deletions.
diff --git a/.github/workflows/xunit-tests.yml b/.github/workflows/xunit-tests.yml
@@ -66,6 +66,8 @@ jobs:
  run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyTestGeneration.Test
  - name: Run AutoExtern Tests
  run: dotnet test --no-restore --verbosity normal --logger trx Source/AutoExtern.Test
+ - name: Run DafnyRuntime Tests
+ run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyRuntime.Tests
  - uses: actions/upload-artifact@v2
  if: always()
  with:

diff --git a/Source/Dafny.sln b/Source/Dafny.sln
@@ -8,6 +8,7 @@ EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore", "DafnyCore\DafnyCore.csproj", "{ACBF62FD-19AC-4243-9019-056D30A130D6}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyRuntime", "DafnyRuntime\DafnyRuntime.csproj", "{09E25A18-19EA-42C4-B33F-69E3E6FD5698}"
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyRuntime.Tests", "DafnyRuntime.Tests\DafnyRuntime.Tests.csproj", "{86D16941-75D5-4D75-ADF3-955C7950F770}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyPipeline", "DafnyPipeline\DafnyPipeline.csproj", "{45FFD363-CFE0-4ABC-984F-7EB58C8BEDE5}"
 EndProject
@@ -40,6 +41,7 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern", "AutoExtern\Au
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExtern.Test\AutoExtern.Test.csproj", "{A47E2F45-DEA3-4700-A82F-9506FEEB199A}"
 EndProject
+EndProject
 Global
  GlobalSection(SolutionConfigurationPlatforms) = preSolution
  Debug|Any CPU = Debug|Any CPU
@@ -98,14 +100,18 @@ Global
  {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.ActiveCfg = Release|Any CPU
  {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.Build.0 = Release|Any CPU
- {FBE70430-9890-405C-A282-61D33259CE30}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {FBE70430-9890-405C-A282-61D33259CE30}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {FBE70430-9890-405C-A282-61D33259CE30}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {FBE70430-9890-405C-A282-61D33259CE30}.Release|Any CPU.Build.0 = Release|Any CPU
+ {FBE70430-9890-405C-A282-61D33259CE30}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {FBE70430-9890-405C-A282-61D33259CE30}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {FBE70430-9890-405C-A282-61D33259CE30}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {FBE70430-9890-405C-A282-61D33259CE30}.Release|Any CPU.Build.0 = Release|Any CPU
  {F185BDC2-1327-47A4-A293-D3FCDC419867}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
  {F185BDC2-1327-47A4-A293-D3FCDC419867}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {F185BDC2-1327-47A4-A293-D3FCDC419867}.Release|Any CPU.ActiveCfg = Release|Any CPU
  {F185BDC2-1327-47A4-A293-D3FCDC419867}.Release|Any CPU.Build.0 = Release|Any CPU
+ {86D16941-75D5-4D75-ADF3-955C7950F770}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {86D16941-75D5-4D75-ADF3-955C7950F770}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {86D16941-75D5-4D75-ADF3-955C7950F770}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {86D16941-75D5-4D75-ADF3-955C7950F770}.Release|Any CPU.Build.0 = Release|Any CPU
  {A47E2F45-DEA3-4700-A82F-9506FEEB199A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
  {A47E2F45-DEA3-4700-A82F-9506FEEB199A}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {A47E2F45-DEA3-4700-A82F-9506FEEB199A}.Release|Any CPU.ActiveCfg = Release|Any CPU

diff --git a/customBoogie.patch b/customBoogie.patch
@@ -1,8 +1,8 @@
 diff --git a/Source/Dafny.sln b/Source/Dafny.sln
-index 88200dcc4..3a75b0cc5 100644
+index ddfd6d91f..06e9bb1a2 100644
 --- a/Source/Dafny.sln
 +++ b/Source/Dafny.sln
-@@ -35,6 +35,34 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern", "AutoExtern\Au
+@@ -41,6 +41,33 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern", "AutoExtern\Au
  EndProject
  Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExtern.Test\AutoExtern.Test.csproj", "{A47E2F45-DEA3-4700-A82F-9506FEEB199A}"
  EndProject
@@ -33,11 +33,10 @@ index 88200dcc4..3a75b0cc5 100644
 +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
 +EndProject
 +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
-+EndProject
+ EndProject
  Global
  GlobalSection(SolutionConfigurationPlatforms) = preSolution
- Debug|Any CPU = Debug|Any CPU
-@@ -106,6 +134,72 @@ Global
+@@ -116,6 +143,72 @@ Global
  {A47E2F45-DEA3-4700-A82F-9506FEEB199A}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {A47E2F45-DEA3-4700-A82F-9506FEEB199A}.Release|Any CPU.ActiveCfg = Release|Any CPU
  {A47E2F45-DEA3-4700-A82F-9506FEEB199A}.Release|Any CPU.Build.0 = Release|Any CPU
@@ -110,7 +109,7 @@ index 88200dcc4..3a75b0cc5 100644
  EndGlobalSection
  GlobalSection(SolutionProperties) = preSolution
  HideSolutionNode = FALSE
-@@ -100,5 +194,18 @@ Global
+@@ -124,5 +217,18 @@ Global
  SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
  EndGlobalSection
  GlobalSection(NestedProjects) = preSolution
@@ -129,11 +128,11 @@ index 88200dcc4..3a75b0cc5 100644
 + {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
  EndGlobalSection
  EndGlobal
-diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
-index 6ea0de067..ca1e0e527 100644
+diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
+index a9e188817..f4f593de9 100644
 --- a/Source/DafnyCore/DafnyCore.csproj
 +++ b/Source/DafnyCore/DafnyCore.csproj
-@@ -25,7 +25,7 @@
+@@ -27,7 +27,7 @@
  <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
  <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
  <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />