Add suggested solution to flow errors in R803-008

src/jwx-crypto.ads

@@ -21,7 +21,8 @@ is
    with
       Pre => Key'First >= 0 and
              Key'Last < Natural'Last and
-             Key'First <= Key'Last;
+             Key'First <= Key'Last,
+      Global => (Payload, Auth, Key);
    --  Validate authenticator
    --
    --  @param Alg            Algorithm to use

src/jwx-jose.adb

@@ -14,6 +14,7 @@ with JWX.Base64;
 with JWX.Util;
 
 package body JWX.JOSE
+  with Refined_State => (State => (JOSE_Valid, Alg))
 is
    JOSE_Valid  : Boolean      := False;
    Alg         : JWX.Alg_Type := JWX.Alg_Invalid;

src/jwx-jose.ads

@@ -14,6 +14,7 @@ with JWX;
 generic
    Data : String;
 package JWX.JOSE
+  with Abstract_State => State
 is
    --  Valid JOSE header
    function Valid return Boolean;
@@ -21,6 +22,7 @@ is
    --  Algorithm defined in JOSE header
    function Algorithm return JWX.Alg_Type
    with
-      Pre => Valid;
+      Pre => Valid,
+      Global => State;
 
 end JWX.JOSE;

src/jwx-json.adb

@@ -10,6 +10,7 @@
 --
 
 package body JWX.JSON
+  with Refined_State => (State => (Context, Context_Index, Offset))
 is
 
    type Context_Element_Type (Kind : Kind_Type := Kind_Invalid) is
@@ -39,7 +40,9 @@ is
                              Depth : Natural)
    with
       Pre => Data'First >= 0 and
-             Data'Last < Natural'Last;
+             Data'Last < Natural'Last,
+      Global => (Input  => (Data, Context_Size, End_Index),
+                 In_Out => (Context, Context_Index, Offset));
 
    ---------------------
    -- Invalid_Element --

src/jwx-json.ads

@@ -11,19 +11,14 @@
 --  @summary JSON decoding (RFC 7159)
 generic
 
-   Input_Data   : String;
-   Context_Size : Natural := Input_Data'Length / 3 + 2;
+   Data         : String;
+   Context_Size : Natural := Data'Length / 3 + 2;
    Depth_Max    : Natural := 100;
 
 package JWX.JSON
+  with Abstract_State => State
 is
 
-   --  @private
-   --  This is a workaround for a bug in GNAT prior to Community 2018, where a
-   --  generic formal parameter is not considered a legal component of refined
-   --  state.
-   Data : constant String := Input_Data;
-
    type Kind_Type is (Kind_Invalid,
                       Kind_Null,
                       Kind_Boolean,
@@ -66,7 +61,9 @@ is
    with
       Pre => Data'First >= 0 and
              Data'Last < Natural'Last and
-             Data'First <= Data'Last;
+             Data'First <= Data'Last,
+      Global => (Input  => (Data, Context_Size, End_Index),
+                 In_Out => State);
    --  Parse a JSON file
    --
    --  @param Match  Result of parsing
@@ -138,7 +135,8 @@ is
    function Query_Object (Name  : String;
                           Index : Index_Type := Null_Index) return Index_Type
    with
-      Pre => Get_Kind (Index) = Kind_Object;
+       Pre => Get_Kind (Index) = Kind_Object,
+       Global => (State, Data, End_Index);
    --  Query object element
    --
    --  @param Name   Name of object element to query

src/jwx-jwk.ads

@@ -157,7 +157,8 @@ is
                 Length : out Natural)
    with
       Pre  => Kind (Key) = Kind_OCT,
-      Post => Length <= Value'Length;
+      Post => Length <= Value'Length,
+      Global => Data;
    --  Return K value of a plain secret key
    --
    --  @param Key     Key

src/jwx-jwscs.adb

@@ -10,9 +10,10 @@
 --
 
 package body JWX.JWSCS
+  with Refined_State => (State => (First, Second))
 is
-   First       : Natural := 0;
-   Second      : Natural := 0;
+   First  : Natural := 0;
+   Second : Natural := 0;
 
    -----------
    -- Split --

src/jwx-jwscs.ads

@@ -12,6 +12,7 @@
 generic
    Data : String;
 package JWX.JWSCS
+  with Abstract_State => State
 is
    function Valid return Boolean
    with
@@ -21,7 +22,9 @@ is
    procedure Split (Token_Valid : out Boolean)
    with
       Pre  => Data'Length >= 5,
-      Post => (if Token_Valid then Valid);
+      Post => (if Token_Valid then Valid),
+      Global => (Input  => Data,
+                 In_Out => State);
    --  Split the JOSE header
    --
    --  @param Token_Valid Head was valid