Switch to GNAT Community 2021

Ref. #494
AdaCore · Jun 8, 2021 · fdedff5 · fdedff5
1 parent d1c1742
commit fdedff5
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 14 deletions.
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -51,7 +51,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_general.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -144,7 +144,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_python.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -195,7 +195,7 @@ jobs:
           ~/.local/bin
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -241,7 +241,7 @@ jobs:
         submodules: true
     - name: Install toolchain
       if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Test
@@ -259,7 +259,7 @@ jobs:
       with:
         submodules: true
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Build runtime
@@ -316,7 +316,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -362,7 +362,7 @@ jobs:
           ~/.local/bin
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -424,7 +424,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_apps.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -471,7 +471,7 @@ jobs:
           ~/.local/bin
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies

diff --git a/README.md b/README.md
@@ -268,7 +268,7 @@ if parse_message(b"\x01\x00\x04\x01\x02\x03\x04") != create_message():
 
 As a prerequisite, the following dependencies need to be installed:
 
-- [GNAT Community](https://www.adacore.com/download) >= 2020
+- [GNAT Community](https://www.adacore.com/download) >= 2021
 - [GMP](https://gmplib.org/) This is provided as a package for various distributions, e.g., libgmp-dev (Debian/Ubuntu), gmp-devel (Fedora) or gmp (Arch Linux).
 
 RecordFlux can be installed from PyPI:

diff --git a/defaults.gpr b/defaults.gpr
@@ -10,7 +10,7 @@ abstract project Defaults is
       "--warnings=error",
       "--proof-warnings",
       "--no-axiom-guard",
-      "--no-counterexample",
+      "--counterexamples=off",
       "-j0"
    );
 

diff --git a/examples/apps/ping/src/icmpv4.ads b/examples/apps/ping/src/icmpv4.ads
@@ -1,4 +1,3 @@
-with SPARK.Heap;
 with RFLX.IPv4;
 with RFLX.RFLX_Builtin_Types;
 with Ada.Text_IO;
@@ -22,8 +21,7 @@ is
 
    procedure Ping (Addr : String) with
       Global => (In_Out => (Ping_State,
-                            Ada.Text_IO.File_System,
-                            SPARK.Heap.Dynamic_Memory),
+                            Ada.Text_IO.File_System),
                  Input  => Ada.Real_Time.Clock_Time);
 
    procedure Generate (Buf  : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;