Upgrade gnatprove to version 15

- Remove no longer needed workaround

Author: mgrojo

alire.toml

@@ -23,7 +23,8 @@ website = "https://github.com/mgrojo/coap_spark"
 tags = ["spark", "coap", "iot", "protocol"]
 
 [[depends-on]]
-gnatprove = "^14.1.1"
+gnat_native = "^15"
+gnatprove = "^15"
 
 [build-switches]
 "*".Style_Checks = [
@@ -65,6 +66,3 @@ wolfssl = { path='libs/wolfssl/wrapper/Ada' }
 # This is needed only for compatibility with https://github.com/mgrojo/ikea-smartlight
 # You can set it to false, if you need to disable it.
 wolfssl.STATIC_PSK = true
-
-[[depends-on]]
-gnat_native = "^14.2"

client/src/coap_client.adb

@@ -24,8 +24,6 @@ with RFLX.RFLX_Types;
 -- explained in the package itself (related to the use of SPARK).
 with SPARK_Terminal;
 
-with Workarounds;
-
 procedure CoAP_Client is
    package FSM renames RFLX.CoAP_Client.Session.FSM;
    package Session_Environment renames RFLX.CoAP_Client.Session_Environment;
@@ -373,7 +371,4 @@ begin
 
    RFLX.RFLX_Types.Free (Payload);
 
-   -- This has no effect, but it is needed to avoid a linking error with
-   -- SPARKLib in the validation profile.
-   Workarounds.Check_Or_Fail;
 end CoAP_Client;

client/src/workarounds.adb

@@ -9,6 +9,7 @@ is
         Response_Codes   : out CoAP_SPARK.Messages.Response_Kind;
         Response_Content : out CoAP_SPARK.Messages.Content)
    is
+      pragma Unreferenced (Request_Content);
    begin
       -- Handle the request based on the method and content.
       case Method is

client/src/workarounds.ads

@@ -1,4 +1,4 @@
-project SPARKlib extends "sparklib_external" is
+project SPARKlib extends "sparklib_internal" is
 
    -- Based on the SPARKlib project file from the Alire gnatprove crate, which
    -- has this notice:
@@ -12,10 +12,10 @@ project SPARKlib extends "sparklib_external" is
 
    for Object_Dir use "obj/sparklib";
 
-   for Source_Dirs use SPARKlib_External'Source_Dirs;
+   for Source_Dirs use SPARKlib_Internal'Source_Dirs;
 
    Ada_Compiler_Switches := 
-      Sparklib_External.Compiler'Default_Switches ("Ada") & (
+      Sparklib_Internal.Compiler'Default_Switches ("Ada") & (
          "-ffunction-sections" -- Separate ELF section for each function
          ,"-fdata-sections" -- Separate ELF section for each variable
          );
@@ -24,7 +24,7 @@ project SPARKlib extends "sparklib_external" is
       for Default_Switches ("Ada") use Ada_Compiler_Switches;
    end Compiler;
 
-   for Excluded_Source_Files use SPARKlib_External'Excluded_Source_Files
+   for Excluded_Source_Files use SPARKlib_Internal'Excluded_Source_Files
       & (
       -- Uncomment the files you want to exclude from your project
       -- "spark-big_integers.ads",